chore: Remove mk_hom and mk_left from simp

PhysLean/Relativity/Lorentz/RealTensor/Vector/Basic.lean

@@ -287,10 +287,16 @@ lemma action_apply_eq_sum (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : Vecto
     simp [mul_add, Finset.sum_add_distrib]
     ring)
   intro r p
-  simp only [C_eq_color, TensorSpecies.F_def, Nat.reduceAdd, OverColor.mk_left,
+  simp only [TensorSpecies.F_def, Nat.reduceAdd, OverColor.mk_left,
     Functor.id_obj, OverColor.mk_hom, PiTensorProduct.tprodCoeff_eq_smul_tprod, _root_.map_smul,
     Pi.smul_apply, smul_eq_mul]
-  erw [OverColor.lift.objObj'_ρ_tprod]
+  conv_lhs =>
+    enter [2, 2]
+    simp only [C_eq_color, OverColor.lift, OverColor.lift.obj', LaxBraidedFunctor.of_toFunctor,
+      Nat.succ_eq_add_one, Nat.reduceAdd]
+    /- I beleive this erw is needed becuase of (realLorentzTensor d).G and
+      LorentzGroup d are different. -/
+    erw [OverColor.lift.objObj'_ρ_tprod]
   conv_rhs =>
     enter [2, x]
     rw [← mul_assoc, mul_comm _ r, mul_assoc]

PhysLean/Relativity/Tensors/OverColor/Basic.lean

@@ -267,11 +267,9 @@ end monoidal
 /-- Make an object of `OverColor C` from a map `X → C`. -/
 def mk (f : X → C) : OverColor C := Over.mk f
 
-@[simp]
 lemma mk_hom (f : X → C) : (mk f).hom = f := rfl
 open MonoidalCategory
 
-@[simp]
 lemma mk_left (f : X → C) : (mk f).left = X := rfl
 
 lemma Hom.fin_ext {n : ℕ} {f g : Fin n → C} (σ σ' : OverColor.mk f ⟶ OverColor.mk g)

PhysLean/Relativity/Tensors/OverColor/Iso.lean

@@ -278,7 +278,7 @@ lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fi
   simp only [Nat.succ_eq_add_one, Equiv.apply_symm_apply]
   match k with
   | Sum.inl (Sum.inl 0) =>
-    simp [-OverColor.mk_left]
+    simp
   | Sum.inl (Sum.inr 0) =>
     simp only [Fin.isValue, finExtractTwo_symm_inl_inr_apply, Sum.map_inl, id_eq]
     have h1 : ((Hom.toEquiv σ) (Fin.succAbove

PhysLean/Relativity/Tensors/TensorSpecies/Contractions/Categorical.lean

@@ -192,7 +192,8 @@ lemma contr_one_two_left_eq_contrOneTwoLeft {c1 c2 : S.C} (x : S.F.obj (OverColo
   rw [contrOneTwoLeft_smul_left]
   simp only [smul_tmul, tmul_smul, LinearMapClass.map_smul]
   apply congrArg
-  simpa using contr_one_two_left_eq_contrOneTwoLeft_tprod (PiTensorProduct.tprod k fx)
+  simpa [OverColor.mk_hom] using
+    contr_one_two_left_eq_contrOneTwoLeft_tprod (PiTensorProduct.tprod k fx)
     (PiTensorProduct.tprod k fy) fx fy
 
 /-- Expanding `contrOneTwoLeft` as a tensor tree. -/

PhysLean/Relativity/Tensors/TensorSpecies/Contractions/ContrMap.lean

@@ -54,7 +54,7 @@ lemma contrFin1Fin1_inv_tmul {n : ℕ} (c : Fin n.succ.succ → S.C)
     (S.contrFin1Fin1 c i j h).inv.hom (x ⊗ₜ[k] y) =
     PiTensorProduct.tprod k (fun k =>
     match k with | Sum.inl 0 => x | Sum.inr 0 => (S.FD.map
-    (eqToHom (by simp [h]))).hom y) := by
+    (eqToHom (by simp [h, mk_hom]))).hom y) := by
   simp only [Nat.succ_eq_add_one, contrFin1Fin1, Functor.comp_obj, Discrete.functor_obj_eq_as,
     Function.comp_apply, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_inv, tensorIso_inv,
     Iso.symm_inv, Functor.mapIso_hom, tensor_comp, Functor.Monoidal.μIso_hom,
@@ -116,7 +116,7 @@ lemma contrFin1Fin1_hom_hom_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
     (x : (k : Fin 1 ⊕ Fin 1) → (S.FD.obj
       { as := (OverColor.mk ((c ∘ ⇑(PhysLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).hom k })) :
     (S.contrFin1Fin1 c i j h).hom.hom (PiTensorProduct.tprod k x) =
-    x (Sum.inl 0) ⊗ₜ[k] ((S.FD.map (eqToHom (by simp [h]))).hom (x (Sum.inr 0))) := by
+    x (Sum.inl 0) ⊗ₜ[k] ((S.FD.map (eqToHom (by simp [h, mk_hom]))).hom (x (Sum.inr 0))) := by
   change ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).hom _ = _
   trans ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).toLinearEquiv
     (PiTensorProduct.tprod k x)

PhysLean/Relativity/Tensors/TensorSpecies/DualRepIso.lean

@@ -107,7 +107,7 @@ lemma toDualRep_fromDualRep_tensorTree_metrics (c : S.C) (x : S.FD.obj (Discrete
   conv_lhs =>
     rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <| tensorNode_of_tree _]
     rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_left _ _ _ _]
-    rw [perm_tensor_eq <| perm_contr_congr 0 0 (by simp) (by
+    rw [perm_tensor_eq <| perm_contr_congr 0 0 (by simp [OverColor.mk_left]) (by
       simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero,
         OverColor.mk_left, Functor.id_obj, OverColor.mk_hom, Equiv.refl_symm, Equiv.coe_refl,
         Function.comp_apply, id_eq, Fin.zero_eta, List.pmap.eq_1, Matrix.cons_val_zero,

PhysLean/Relativity/Tensors/TensorSpecies/UnitTensor.lean

@@ -141,10 +141,12 @@ lemma unitTensor_contr_vec_eq_self {c1 : S.C} (x : S.F.obj (OverColor.mk ![S.τ
     perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl))).tensor := by
   conv_lhs =>
     rw [contr_tensor_eq <| prod_comm _ _ _ _]
-    rw [perm_contr_congr 2 0 (by simp; decide) (by simp; decide)]
+    rw [perm_contr_congr 2 0 (by simp [mk_hom, mk_left]; decide)
+      (by simp [mk_hom, mk_left]; decide)]
     rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| unitTensor_eq_dual_perm _]
     rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_right _ _ _ _]
-    rw [perm_tensor_eq <| perm_contr_congr 1 0 (by simp; decide) (by simp; decide)]
+    rw [perm_tensor_eq <| perm_contr_congr 1 0 (by simp [mk_hom, mk_left]; decide)
+      (by simp [mk_hom, mk_left]; decide)]
     rw [perm_perm]
     rw [perm_tensor_eq <| contr_swap _ _]
     rw [perm_perm]

PhysLean/Relativity/Tensors/Tree/Basic.lean

@@ -344,7 +344,7 @@ lemma prod_tensorBasis_repr_apply {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m
         (TensorBasis.prodEquiv.symm (b1, b2))) b
       · congr 2
         rw [TensorBasis.tensorBasis_prod]
-        simp
+        simp [OverColor.mk_hom]
       simp only [Function.comp_apply, Basis.repr_self, Pt, P]
       rw [MonoidAlgebra.single_apply, MonoidAlgebra.single_apply, MonoidAlgebra.single_apply]
       obtain ⟨b, rfl⟩ := TensorBasis.prodEquiv.symm.surjective b
@@ -546,7 +546,7 @@ lemma field_eq_repr {c : Fin 0 → S.C} (t : TensorTree S c) :
         LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single, LinearEquiv.coe_coe]
         change (PiTensorProduct.isEmptyEquiv (Fin 0)) (S.fromCoordinates c
           (Pi.single _ 1)) = _
-        simp [fromCoordinates, basisVector]
+        simp [fromCoordinates, basisVector, OverColor.mk_hom, OverColor.mk_left]
     · simp only [Fin.default_eq_zero, mul_one]
       congr
       funext j

PhysLean/Relativity/Tensors/Tree/NodeIdentities/Basic.lean

@@ -172,9 +172,9 @@ lemma perm_eq_iff_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
       apply Hom.ext
       ext x
       change (Hom.toEquiv σ) ((Hom.toEquiv σ).symm x) = x
-      simp [-OverColor.mk_left]
+      simp
     rw [h1]
-    simp
+    simp [OverColor.mk_hom]
 
 /-!
 

PhysLean/Relativity/Tensors/Tree/NodeIdentities/ContrSwap.lean

@@ -76,7 +76,7 @@ def contrSwapHom : (OverColor.mk (c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbov
 
 @[simp]
 lemma contrSwapHom_toEquiv : Hom.toEquiv q.contrSwapHom = Equiv.refl (Fin n) := by
-  simp [contrSwapHom]
+  simp [contrSwapHom, OverColor.mk_left]
 
 @[simp]
 lemma contrSwapHom_hom_left_apply (x : Fin n) : q.contrSwapHom.hom.left x = x := by