Merge pull request #424 from HEPLean/erw

removing some erw's

PhysLean/Mathematics/Fin.lean

@@ -158,7 +158,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
 
 /-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
   `i`th component. -/
-def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
+def finExtractOne {n : ℕ} (i : Fin (n + 1)) : Fin (n + 1) ≃ Fin 1 ⊕ Fin n :=
   (finCongr (by omega : n.succ = i + 1 + (n - i))).trans <|
   finSumFinEquiv.symm.trans <|
   (Equiv.sumCongr (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin i) (Fin 1)))
@@ -231,7 +231,7 @@ lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
     (finExtractOne i).symm (Sum.inl 0) = i := by
   rfl
 
-lemma finExtractOne_apply_neq {n : ℕ} (i j : Fin n.succ.succ) (hij : i ≠ j) :
+lemma finExtractOne_apply_neq {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) :
     finExtractOne i j = Sum.inr (predAboveI i j) := by
   symm
   apply (Equiv.symm_apply_eq _).mp ?_

PhysLean/Mathematics/List.lean

@@ -344,7 +344,7 @@ lemma orderedInsert_eraseIdx_orderedInsertPos_le {I : Type} (le1 : I → I → P
 /-- The equivalence between `Fin (r0 :: r).length` and `Fin (List.orderedInsert le1 r0 r).length`
   according to where the elements map, i.e. `0` is taken to `orderedInsertPos le1 r r0`. -/
 def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
-    Fin (r0 :: r).length ≃ Fin (List.orderedInsert le1 r0 r).length := by
+    Fin (r.length + 1) ≃ Fin (List.orderedInsert le1 r0 r).length := by
   let e2 : Fin (List.orderedInsert le1 r0 r).length ≃ Fin (r0 :: r).length :=
     (Fin.castOrderIso (List.orderedInsert_length le1 r r0)).toEquiv
   let e3 : Fin (r0 :: r).length ≃ Fin 1 ⊕ Fin (r).length := finExtractOne 0
@@ -352,8 +352,9 @@ def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r
     finExtractOne ⟨orderedInsertPos le1 r r0, orderedInsertPos_lt_length le1 r r0⟩
   exact e3.trans (e4.symm.trans e2.symm)
 
+@[simp]
 lemma orderedInsertEquiv_zero {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
-    (r0 : I) : orderedInsertEquiv le1 r r0 ⟨0, by simp⟩ = orderedInsertPos le1 r r0 := by
+    (r0 : I) : orderedInsertEquiv le1 r r0 0 = orderedInsertPos le1 r r0 := by
   simp [orderedInsertEquiv]
 
 lemma orderedInsertEquiv_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
@@ -368,7 +369,8 @@ lemma orderedInsertEquiv_succ {I : Type} (le1 : I → I → Prop) [DecidableRel
   | [] =>
     simp
   | r1 :: r =>
-    erw [finExtractOne_apply_neq]
+    simp only [List.orderedInsert.eq_2, List.length_cons, Fin.cast_inj]
+    rw [finExtractOne_apply_neq]
     simp only [List.orderedInsert.eq_2, List.length_cons, orderedInsertPos, decide_not,
       Nat.succ_eq_add_one, finExtractOne_symm_inr_apply]
     rfl
@@ -384,9 +386,12 @@ lemma orderedInsertEquiv_fin_succ {I : Type} (le1 : I → I → Prop) [Decidable
   | [] =>
     simp
   | r1 :: r =>
-    erw [finExtractOne_apply_neq]
-    simp only [List.orderedInsert.eq_2, List.length_cons, orderedInsertPos, decide_not,
-      Nat.succ_eq_add_one, finExtractOne_symm_inr_apply]
+    simp only [List.orderedInsert.eq_2, List.length_cons, OrderIso.toEquiv_symm,
+      Fin.symm_castOrderIso, Nat.succ_eq_add_one, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
+      Fin.eta, Fin.cast_inj]
+    rw [finExtractOne_apply_neq]
+    simp only [orderedInsertPos, List.orderedInsert.eq_2, decide_not, Nat.succ_eq_add_one,
+      finExtractOne_symm_inr_apply]
     rfl
     exact ne_of_beq_false rfl
 
@@ -413,14 +418,11 @@ lemma get_eq_orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRe
   funext x
   match x with
   | ⟨0, h⟩ =>
-    simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
-      List.getElem_cons_zero, Function.comp_apply]
-    erw [orderedInsertEquiv_zero]
     simp
   | ⟨Nat.succ n, h⟩ =>
     simp only [List.length_cons, Nat.succ_eq_add_one, List.get_eq_getElem, List.getElem_cons_succ,
       Function.comp_apply]
-    erw [orderedInsertEquiv_succ]
+    rw [orderedInsertEquiv_succ]
     simp only [Fin.succAbove, Fin.castSucc_mk, Fin.mk_lt_mk, Fin.succ_mk, Fin.coe_cast]
     by_cases hn : n < ↑(orderedInsertPos le1 r r0)
     · simp [hn, orderedInsert_get_lt]
@@ -501,7 +503,7 @@ lemma orderedInsertEquiv_sigma {I : Type} {f : I → Type}
   | ⟨0, h0⟩ =>
     simp only [List.length_cons, Fin.zero_eta, Equiv.trans_apply, RelIso.coe_fn_toEquiv,
       Fin.castOrderIso_apply, Fin.cast_zero, Fin.coe_cast]
-    erw [orderedInsertEquiv_zero, orderedInsertEquiv_zero]
+    rw [orderedInsertEquiv_zero, orderedInsertEquiv_zero]
     simp [orderedInsertPos_sigma]
   | ⟨Nat.succ n, h0⟩ =>
     simp only [List.length_cons, Nat.succ_eq_add_one, Equiv.trans_apply, RelIso.coe_fn_toEquiv,

PhysLean/QFT/AnomalyCancellation/MSSMNu/Basic.lean

@@ -138,7 +138,7 @@ def accGrav : MSSMCharges.Charges →ₗ[ℚ] ℚ where
     repeat rw [map_add]
     simp only [MSSMSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add,
       toSMSpecies_apply, reduceMul, Fin.isValue, mul_add, Hd_apply, Fin.reduceFinMk, Hu_apply]
-    repeat erw [Finset.sum_add_distrib]
+    repeat rw [Finset.sum_add_distrib]
     ring
   map_smul' a S := by
     simp only
@@ -146,9 +146,8 @@ def accGrav : MSSMCharges.Charges →ₗ[ℚ] ℚ where
     erw [Hd.map_smul, Hu.map_smul]
     simp only [MSSMSpecies_numberCharges, HSMul.hSMul, SMul.smul, Fin.isValue, toSMSpecies_apply,
       reduceMul, Hd_apply, Fin.reduceFinMk, Hu_apply, eq_ratCast, Rat.cast_eq_id, id_eq]
-    repeat erw [Finset.sum_add_distrib]
-    repeat erw [← Finset.mul_sum]
-    --rw [show Rat.cast a = a from rfl]
+    repeat rw [Finset.sum_add_distrib]
+    repeat rw [← Finset.mul_sum]
     ring
 
 /-- Extensionality lemma for `accGrav`. -/

PhysLean/QFT/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean

@@ -119,7 +119,10 @@ lemma cube_proj_proj_Y₃ (T : MSSMACC.LinSols) :
     (dot Y₃.val B₃.val)^2 * cubeTriLin T.val T.val Y₃.val := by
   rw [proj_val]
   rw [cubeTriLin.map_add₁, cubeTriLin.map_add₂]
-  erw [lineY₃B₃_doublePoint]
+  conv_lhs =>
+    enter [1, 1]
+    change ((cubeTriLin (lineY₃B₃ _ _).val) (lineY₃B₃ _ _).val) _
+    rw [lineY₃B₃_doublePoint]
   rw [cubeTriLin.map_add₂]
   rw [cubeTriLin.swap₂]
   rw [cubeTriLin.map_add₁, cubeTriLin.map_smul₁, cubeTriLin.map_smul₃]

PhysLean/QFT/AnomalyCancellation/PureU1/Basic.lean

@@ -104,7 +104,7 @@ open BigOperators
 
 /-- A solution to the pure U(1) accs satisfies the linear ACCs. -/
 lemma pureU1_linear {n : ℕ} (S : (PureU1 n).LinSols) :
-    ∑ i, S.val i = 0 := by
+    ∑ (i : Fin n), S.val i = 0 := by
   have hS := S.linearSol
   simp only [succ_eq_add_one, PureU1_numberLinear, PureU1_linearACCs] at hS
   exact hS 0

PhysLean/QFT/AnomalyCancellation/PureU1/ConstAbs.lean

@@ -176,7 +176,7 @@ lemma AFL_hasBoundary (h : A.val (0 : Fin n.succ) ≠ 0) : HasBoundary A.val :=
   by_contra hn
   have h0 := not_hasBoundary_grav hA hn
   simp only [succ_eq_add_one, accGrav, LinearMap.coe_mk, AddHom.coe_mk, cast_add, cast_one] at h0
-  erw [pureU1_linear A] at h0
+  rw [pureU1_linear A] at h0
   simp only [zero_eq_mul] at h0
   cases' h0
   · linarith
@@ -188,7 +188,7 @@ lemma AFL_odd_noBoundary {A : (PureU1 (2 * n + 1)).LinSols} (h : ConstAbsSorted
   obtain ⟨k, hk⟩ := hn
   have h0 := boundary_accGrav'' h k hk
   simp only [succ_eq_add_one, accGrav, LinearMap.coe_mk, AddHom.coe_mk, cast_mul, cast_ofNat] at h0
-  erw [pureU1_linear A] at h0
+  rw [pureU1_linear A] at h0
   simp only [zero_eq_mul, hA, or_false] at h0
   have h1 : 2 * n = 2 * k.val + 1 := by
     rw [← @Nat.cast_inj ℚ]
@@ -210,8 +210,10 @@ lemma AFL_even_Boundary {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted
     (hA : A.val (0 : Fin (2 * n.succ)) ≠ 0) {k : Fin (2 * n + 1)} (hk : Boundary A.val k) :
     k.val = n := by
   have h0 := boundary_accGrav'' h k hk
-  change ∑ i : Fin (succ (Nat.mul 2 n + 1)), A.val i = _ at h0
-  erw [pureU1_linear A] at h0
+  change ∑ i, A.val i = _ at h0
+  simp only [succ_eq_add_one, PureU1_numberCharges, mul_eq, cast_add, cast_mul, cast_ofNat,
+    cast_one, add_sub_add_right_eq_sub] at h0
+  rw [pureU1_linear A] at h0
   simp only [mul_eq, cast_add, cast_mul, cast_ofNat, cast_one, add_sub_add_right_eq_sub,
     succ_eq_add_one, zero_eq_mul, hA, or_false] at h0
   rw [← @Nat.cast_inj ℚ]

PhysLean/QFT/AnomalyCancellation/PureU1/Even/LineInCubic.lean

@@ -45,7 +45,14 @@ lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S)
   simp only [TriLinearSymm.toCubic_add] at h1
   simp only [HomogeneousCubic.map_smul,
     accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1
-  erw [P_accCube, P!_accCube] at h1
+  conv_lhs at h1 =>
+    enter [1, 1, 1, 2]
+    change accCube _ _
+    rw [P_accCube]
+  conv_lhs at h1 =>
+    enter [1, 1, 2, 2]
+    change accCube _ _
+    rw [P!_accCube]
   rw [← h1]
   ring
 

PhysLean/Relativity/Lorentz/ComplexTensor/OfRat.lean

@@ -145,7 +145,7 @@ lemma contr_ofRat {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.C} {i
   congr
   funext b
   rw [← (contrSectionEquiv b).symm.sum_comp]
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   congr
   funext x
   rw [Finset.sum_eq_single (Fin.cast (by simp [h]) x)]

PhysLean/Relativity/Lorentz/ComplexVector/Two.lean

@@ -33,7 +33,7 @@ lemma contrContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1
   simp only [Action.instMonoidalCategory_tensorObj_V, contrContrToMatrix, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply complexContrBasis complexContrBasis i j]
     rfl
@@ -52,7 +52,7 @@ lemma coCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin
   simp only [Action.instMonoidalCategory_tensorObj_V, coCoToMatrix, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply complexCoBasis complexCoBasis i j]
     rfl
@@ -71,7 +71,7 @@ lemma contrCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕
   simp only [Action.instMonoidalCategory_tensorObj_V, contrCoToMatrix, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply complexContrBasis complexCoBasis i j]
     rfl
@@ -90,7 +90,7 @@ lemma coContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕
   simp only [Action.instMonoidalCategory_tensorObj_V, coContrToMatrix, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply complexCoBasis complexContrBasis i j]
     rfl
@@ -126,7 +126,7 @@ lemma contrContrToMatrix_ρ (v : (complexContr ⊗ complexContr).V) (M : SL(2,
         ((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M))
         ((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M)) (i, j) k)
         * contrContrToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x, (∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
       contrContrToMatrix v x1 x) * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
@@ -168,7 +168,7 @@ lemma coCoToMatrix_ρ (v : (complexCo ⊗ complexCo).V) (M : SL(2,ℂ)) :
         ((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M))
         ((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M)) (i, j) k)
         * coCoToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x, (∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
       coCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
@@ -210,7 +210,7 @@ lemma contrCoToMatrix_ρ (v : (complexContr ⊗ complexCo).V) (M : SL(2,ℂ)) :
         ((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M))
         ((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M)) (i, j) k)
         * contrCoToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply]
   have h1 : ∑ x, (∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
       contrCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
@@ -253,7 +253,7 @@ lemma coContrToMatrix_ρ (v : (complexCo ⊗ complexContr).V) (M : SL(2,ℂ)) :
         ((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M))
         ((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M)) (i, j) k)
         * coContrToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x, (∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
       coContrToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) j x

PhysLean/Relativity/Lorentz/RealTensor/Basic.lean

@@ -242,7 +242,7 @@ lemma contr_tensorBasis_repr_apply_eq_fin {n d: ℕ} {c : Fin (n + 1 + 1) → (r
     (liftToContrSection b ⟨Fin.cast (by simp) x, Fin.cast (by simp) x⟩)) := by
   rw [contr_tensorBasis_repr_apply_eq_contrSection]
   rw [← (contrSectionEquiv b).symm.sum_comp]
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   let e : Fin ((realLorentzTensor d).repDim (c i)) ≃ Fin (1 + d) :=
     (Fin.castOrderIso (by simp)).toEquiv
   rw [← e.symm.sum_comp]

PhysLean/Relativity/Lorentz/RealTensor/Matrix/Pre.lean

@@ -32,7 +32,7 @@ lemma contrContrToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
   simp only [contrContrToMatrixRe, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply (contrBasis d) (contrBasis d) i j]
     rfl
@@ -51,7 +51,7 @@ lemma coCoToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ F
   simp only [Action.instMonoidalCategory_tensorObj_V, coCoToMatrixRe, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply (coBasis d) (coBasis d) i j]
     rfl
@@ -70,7 +70,7 @@ lemma contrCoToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
   simp only [contrCoToMatrixRe, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply _ _ i j]
     rfl
@@ -89,7 +89,7 @@ lemma coContrToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
   simp only [Action.instMonoidalCategory_tensorObj_V, coContrToMatrixRe, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply _ _ i j]
     rfl
@@ -124,7 +124,7 @@ lemma contrContrToMatrixRe_ρ {d : ℕ} (v : (Contr d ⊗ Contr d).V) (M : Loren
         ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M))
         ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M)) (i, j) k)
         * contrContrToMatrixRe v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   conv_rhs =>
     enter [2, x]
@@ -160,7 +160,7 @@ lemma coCoToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Co d)).V) (M : LorentzGroup
         ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M))
         ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M)) (i, j) k)
         * coCoToMatrixRe v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   conv_rhs =>
     enter [2, x]
@@ -197,7 +197,7 @@ lemma contrCoToMatrixRe_ρ {d : ℕ} (v : ((Contr d) ⊗ (Co d)).V) (M : Lorentz
         ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M))
         ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M)) (i, j) k)
         * contrCoToMatrixRe v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply]
   conv_rhs =>
     enter [2, x]
@@ -234,7 +234,7 @@ lemma coContrToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Contr d)).V) (M : Lorentz
         ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M))
         ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M)) (i, j) k)
         * coContrToMatrixRe v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   conv_rhs =>
     enter [2, x]

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.succ_eq_add_one, 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/Lorentz/Weyl/Two.lean

@@ -38,9 +38,11 @@ lemma leftLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
   simp only [Action.instMonoidalCategory_tensorObj_V, leftLeftToMatrix,
     LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    erw [Basis.tensorProduct_apply leftBasis leftBasis i j]
+    conv_lhs =>
+      enter [2]
+      erw [Basis.tensorProduct_apply leftBasis leftBasis i j]
     rfl
   · simp
 
@@ -56,7 +58,7 @@ lemma altLeftaltLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
   simp only [Action.instMonoidalCategory_tensorObj_V, altLeftaltLeftToMatrix,
     LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply altLeftBasis altLeftBasis i j]
     rfl
@@ -74,7 +76,7 @@ lemma leftAltLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
   simp only [Action.instMonoidalCategory_tensorObj_V, leftAltLeftToMatrix,
     LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply leftBasis altLeftBasis i j]
     rfl
@@ -92,7 +94,7 @@ lemma altLeftLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
   simp only [Action.instMonoidalCategory_tensorObj_V, altLeftLeftToMatrix,
     LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply altLeftBasis leftBasis i j]
     rfl
@@ -110,7 +112,7 @@ lemma rightRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
   simp only [Action.instMonoidalCategory_tensorObj_V, rightRightToMatrix,
     LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply rightBasis rightBasis i j]
     rfl
@@ -129,7 +131,7 @@ lemma altRightAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ)
   simp only [Action.instMonoidalCategory_tensorObj_V, altRightAltRightToMatrix,
     LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply altRightBasis altRightBasis i j]
     rfl
@@ -147,7 +149,7 @@ lemma rightAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
   simp only [Action.instMonoidalCategory_tensorObj_V, rightAltRightToMatrix, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply rightBasis altRightBasis i j]
     rfl
@@ -165,7 +167,7 @@ lemma altRightRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
   simp only [Action.instMonoidalCategory_tensorObj_V, altRightRightToMatrix, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply altRightBasis rightBasis i j]
     rfl
@@ -183,7 +185,7 @@ lemma altLeftAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ)
   simp only [Action.instMonoidalCategory_tensorObj_V, altLeftAltRightToMatrix,
     LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply altLeftBasis altRightBasis i j]
     rfl
@@ -201,7 +203,7 @@ lemma leftRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
   simp only [Action.instMonoidalCategory_tensorObj_V, leftRightToMatrix, LinearEquiv.trans_symm,
     LinearEquiv.trans_apply, Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
-  · erw [Finset.sum_product]
+  · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
     erw [Basis.tensorProduct_apply leftBasis rightBasis i j]
     rfl
@@ -236,7 +238,7 @@ lemma leftLeftToMatrix_ρ (v : (leftHanded ⊗ leftHanded).V) (M : SL(2,ℂ)) :
         ((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M))
         ((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M)) (i, j) k)
         * leftLeftToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x : Fin 2, (∑ j : Fin 2, M.1 i j * leftLeftToMatrix v j x) * M.1 j x
     = ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftLeftToMatrix v x1 x) * M.1 j x := by
@@ -279,7 +281,7 @@ lemma altLeftaltLeftToMatrix_ρ (v : (altLeftHanded ⊗ altLeftHanded).V) (M : S
         ((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M))
         ((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M)) (i, j) k)
         * altLeftaltLeftToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1)⁻¹ x1 i * altLeftaltLeftToMatrix v x1 x) * (M.1)⁻¹ x j
     = ∑ x : Fin 2, ∑ x1 : Fin 2, ((M.1)⁻¹ x1 i * altLeftaltLeftToMatrix v x1 x) * (M.1)⁻¹ x j := by
@@ -319,7 +321,7 @@ lemma leftAltLeftToMatrix_ρ (v : (leftHanded ⊗ altLeftHanded).V) (M : SL(2,
         ((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M))
         ((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M)) (i, j) k)
         * leftAltLeftToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply]
   have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, M.1 i x1 * leftAltLeftToMatrix v x1 x) * (M.1⁻¹) x j
     = ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftAltLeftToMatrix v x1 x) * (M.1⁻¹) x j := by
@@ -360,7 +362,7 @@ lemma altLeftLeftToMatrix_ρ (v : (altLeftHanded ⊗ leftHanded).V) (M : SL(2,
         ((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M))
         ((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M)) (i, j) k)
         * altLeftLeftToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1)⁻¹ x1 i * altLeftLeftToMatrix v x1 x) * M.1 j x
     = ∑ x : Fin 2, ∑ x1 : Fin 2, ((M.1)⁻¹ x1 i * altLeftLeftToMatrix v x1 x) * M.1 j x:= by
@@ -401,7 +403,7 @@ lemma rightRightToMatrix_ρ (v : (rightHanded ⊗ rightHanded).V) (M : SL(2,ℂ)
         ((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M))
         ((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M)) (i, j) k)
         * rightRightToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1.map star) i x1 * rightRightToMatrix v x1 x) *
       (M.1.map star) j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
@@ -443,7 +445,7 @@ lemma altRightAltRightToMatrix_ρ (v : (altRightHanded ⊗ altRightHanded).V) (M
         ((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M))
         ((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M)) (i, j) k)
         * altRightAltRightToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (↑M)⁻¹ᴴ i x1 * altRightAltRightToMatrix v x1 x) *
       (↑M)⁻¹ᴴ j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
@@ -484,7 +486,7 @@ lemma rightAltRightToMatrix_ρ (v : (rightHanded ⊗ altRightHanded).V) (M : SL(
         ((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M))
         ((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M)) (i, j) k)
         * rightAltRightToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1.map star) i x1 * rightAltRightToMatrix v x1 x)
       * (↑M)⁻¹ᴴ j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
@@ -526,7 +528,7 @@ lemma altRightRightToMatrix_ρ (v : (altRightHanded ⊗ rightHanded).V) (M : SL(
         ((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M))
         ((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M)) (i, j) k)
         * altRightRightToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2,
       (↑M)⁻¹ᴴ i x1 * altRightRightToMatrix v x1 x) * (M.1.map star) j x
@@ -567,7 +569,7 @@ lemma altLeftAltRightToMatrix_ρ (v : (altLeftHanded ⊗ altRightHanded).V) (M :
         ((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M))
         ((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M)) (i, j) k)
         * altLeftAltRightToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
   have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1)⁻¹ x1 i * altLeftAltRightToMatrix v x1 x) *
       (M.1)⁻¹ᴴ j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
@@ -607,7 +609,7 @@ lemma leftRightToMatrix_ρ (v : (leftHanded ⊗ rightHanded).V) (M : SL(2,ℂ))
         ((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M))
         ((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M)) (i, j) k)
         * leftRightToMatrix v k.1 k.2) = _
-  erw [Finset.sum_product]
+  rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply]
   have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, M.1 i x1 * leftRightToMatrix v x1 x) * (M.1)ᴴ x j
     = ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftRightToMatrix v x1 x) * (M.1)ᴴ x j := by

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/Discrete.lean

@@ -48,7 +48,7 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverCol
 /-- The isomorphism between `F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)` and
   `(lift.obj F).obj (OverColor.mk ![c1,c2])` formed by the tensor. -/
 def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ≅
-    (lift.obj F).obj (OverColor.mk ![c1,c2]) := by
+    (lift.obj F).obj (OverColor.mk (![c1 ,c2] : Fin 2 → C)) := by
   symm
   apply ((lift.obj F).mapIso fin2Iso).trans
   apply (Functor.Monoidal.μIso (lift.obj F).toFunctor _ _).symm.trans
@@ -67,8 +67,13 @@ def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)
     rfl
 
 lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discrete.mk c2)) :
-    (pairIsoSep F).hom.hom (x ⊗ₜ[k] y) =
+    ((pairIsoSep F).hom.hom :
+      (F.obj (Discrete.mk c1)).V ⊗ (F.obj (Discrete.mk c2)).V ⟶  _ ) (x ⊗ₜ[k] y) =
     PiTensorProduct.tprod k (Fin.cases x (Fin.cases y (fun i => Fin.elim0 i))) := by
+  conv_lhs =>
+    simp only [Action.instMonoidalCategory_tensorObj_V, Nat.succ_eq_add_one, Nat.reduceAdd,
+      Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+      Action.FunctorCategoryEquivalence.functor_obj_obj]
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Action.instMonoidalCategory_tensorObj_V,
     pairIsoSep, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
     forgetLiftApp, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom,

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/OverColor/Lift.lean

@@ -69,10 +69,10 @@ lemma discreteFunctorMapEqIso_comm_ρ {c1 c2 : Discrete C} (h : c1.as = c2.as) (
 
 /-- Given a object in `OverColor Color` the corresponding tensor product of representations. -/
 def objObj' (f : OverColor C) : Rep k G := Rep.of {
-  toFun := fun M => PiTensorProduct.map (fun x =>
+  toFun := fun M => PiTensorProduct.map (ι := f.left) (fun x =>
     (F.obj (Discrete.mk (f.hom x))).ρ M),
   map_one' := by
-    simp only [Functor.id_obj, map_one, PiTensorProduct.map_one]
+    simp only [map_one, PiTensorProduct.map_one]
   map_mul' := fun M N => by
     simp only [CategoryTheory.Functor.id_obj, _root_.map_mul]
     ext x : 2
@@ -118,7 +118,7 @@ lemma objObj'_ρ_from_fin0 (c : Fin 0 → C) (g : G) :
   exact Fin.elim0 i
 
 open TensorProduct in
-@[simp]
+
 lemma objObj'_V_carrier (f : OverColor C) :
     (objObj' F f).V = ⨂[k] (i : f.left), F.obj (Discrete.mk (f.hom i)) := rfl
 
@@ -159,7 +159,8 @@ def objMap' {f g : OverColor C} (m : f ⟶ g) : objObj' F f ⟶ objObj' F g wher
     change (mapToLinearEquiv' F m) (((objObj' F f).ρ M) ((PiTensorProduct.tprod k) x)) =
       ((objObj' F g).ρ M) ((mapToLinearEquiv' F m) ((PiTensorProduct.tprod k) x))
     rw [mapToLinearEquiv'_tprod, objObj'_ρ_tprod]
-    erw [mapToLinearEquiv'_tprod, objObj'_ρ_tprod]
+    simp only [Functor.id_obj]
+    rw [mapToLinearEquiv'_tprod, objObj'_ρ_tprod]
     apply congrArg
     funext i
     rw [discreteFunctorMapEqIso_comm_ρ]
@@ -218,7 +219,7 @@ def discreteSumEquiv' {X Y : Type} {cX : X → C} {cY : Y → C} (i : X ⊕ Y) :
 
 /-- The equivalence of modules corresponding to the tensor. -/
 def μModEquiv (X Y : OverColor C) :
-    (objObj' F X ⊗ objObj' F Y).V ≃ₗ[k] objObj' F (X ⊗ Y) :=
+    ((objObj' F X).V ⊗[k] (objObj' F Y).V) ≃ₗ[k] objObj' F (X ⊗ Y) :=
   PhysLean.PiTensorProduct.tmulEquiv ≪≫ₗ PiTensorProduct.congr (discreteSumEquiv' F)
 
 lemma μModEquiv_tmul_tprod {X Y : OverColor C}
@@ -233,7 +234,7 @@ lemma μModEquiv_tmul_tprod {X Y : OverColor C}
     Functor.id_obj, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
     Action.FunctorCategoryEquivalence.functor_obj_obj]
   rw [LinearEquiv.trans_apply]
-  erw [PhysLean.PiTensorProduct.tmulEquiv_tmul_tprod]
+  rw [PhysLean.PiTensorProduct.tmulEquiv_tmul_tprod]
   change PiTensorProduct.congr (discreteSumEquiv' F)
     (PiTensorProduct.tprod k (PhysLean.PiTensorProduct.elimPureTensor p q)) = _
   rw [PiTensorProduct.congr_tprod]
@@ -244,17 +245,15 @@ def μ (X Y : OverColor C) : objObj' F X ⊗ objObj' F Y ≅ objObj' F (X ⊗ Y)
   (fun M => by
     refine ModuleCat.hom_ext ?_
     refine PhysLean.PiTensorProduct.induction_tmul (fun p q => ?_)
-    simp only [objObj'_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
-      OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp,
-      Action.instMonoidalCategory_tensorObj_V, Action.tensor_ρ, LinearMap.coe_comp,
-      Function.comp_apply]
     change (μModEquiv F X Y)
       ((objObj' F X).ρ M (PiTensorProduct.tprod k p) ⊗ₜ[k]
       (objObj' F Y).ρ M (PiTensorProduct.tprod k q)) = (objObj' F (X ⊗ Y)).ρ M
       (μModEquiv F X Y (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q))
     rw [μModEquiv_tmul_tprod]
-    erw [objObj'_ρ_tprod, objObj'_ρ_tprod, objObj'_ρ_tprod]
+    rw [objObj'_ρ_tprod, objObj'_ρ_tprod]
+    simp only [Functor.id_obj]
     rw [μModEquiv_tmul_tprod]
+    erw [objObj'_ρ_tprod]
     apply congrArg
     funext i
     match i with
@@ -521,7 +520,8 @@ lemma objMap'_id (X : OverColor C) : objMap' F (𝟙 X) = 𝟙 _ := by
   simp only [CategoryTheory.Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
     _root_.map_smul, Action.id_hom, ModuleCat.id_apply]
   apply congrArg
-  erw [mapToLinearEquiv'_tprod]
+  simp only [objMap', ModuleCat.hom_ofHom, LinearEquiv.coe_coe]
+  rw [mapToLinearEquiv'_tprod]
   simp only [objObj'_V_carrier, discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
     Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
   exact congrArg _ (funext (fun i => rfl))
@@ -618,6 +618,7 @@ lemma mapApp'_tprod (X : OverColor C) (p : (i : X.left) → F.obj (Discrete.mk (
     PiTensorProduct.tprod k fun i => (η.app (Discrete.mk (X.hom i))).hom (p i) := by
   simp only [mapApp']
   erw [PiTensorProduct.map_tprod]
+  rfl
 
 lemma mapApp'_naturality {X Y : OverColor C} (f : X ⟶ Y) :
     (obj' F).map f ≫ mapApp' η Y = mapApp' η X ≫ (obj' F').map f := by
@@ -721,7 +722,7 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ LaxBraidedFunctor (OverCol
     intro r y
     simp only [Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod, map_smul]
     apply congrArg
-    erw [lift.mapApp'_tprod]
+    rw [lift.mapApp'_tprod]
     rfl
   map_comp {F G H} η θ := by
     refine LaxMonoidalFunctor.hom_ext ?_
@@ -852,6 +853,7 @@ def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c
     apply congrArg
     erw [PiTensorProduct.subsingletonEquiv_apply_tprod]
     simp only [lift, lift.obj', lift.objObj'_V_carrier, Fin.isValue]
+    simp
     erw [lift.objObj'_ρ_tprod]
     erw [PiTensorProduct.subsingletonEquiv_apply_tprod]
     rfl)

PhysLean/Relativity/Tensors/TensorSpecies/Basis.lean

@@ -80,13 +80,14 @@ def coordinateMultiLinear {n : ℕ} (c : Fin n → S.C) :
 /-- The linear map from tensors to coordinates. -/
 def coordinate {n : ℕ} (c : Fin n → S.C) :
     S.F.obj (OverColor.mk c) →ₗ[k] ((Π j, Fin (S.repDim (c j))) → k) :=
-  (S.liftTensor (c := c)).toFun (S.coordinateMultiLinear c)
+  PiTensorProduct.lift (S.coordinateMultiLinear c)
 
+@[simp]
 lemma coordinate_tprod {n : ℕ} (c : Fin n → S.C) (x : (i : Fin n) → S.FD.obj (Discrete.mk (c i))) :
     S.coordinate c (PiTensorProduct.tprod k x) = S.coordinateMultiLinear c x := by
-  simp only [coordinate, liftTensor, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
-    LinearEquiv.coe_coe, mk_left, Functor.id_obj, mk_hom]
+  rw [coordinate]
   erw [PiTensorProduct.lift.tprod]
+  rfl
 
 /-- The basis vector of tensors given a `b : Π j, Fin (S.repDim (c j))` . -/
 def basisVector {n : ℕ} (c : Fin n → S.C) (b : Π j, Fin (S.repDim (c j))) :

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

@@ -66,6 +66,7 @@ lemma contrOneTwoLeft_add_right {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
   simp only [contrOneTwoLeft]
   simp [map_add, add_tmul, tmul_add]
 
+@[simp]
 lemma contrOneTwoLeft_tprod_eq {c1 c2 : S.C}
     (fx : (i : (𝟭 Type).obj (OverColor.mk ![c1]).left) →
       (S.FD.obj { as := (OverColor.mk ![c1]).hom i }))
@@ -110,7 +111,7 @@ lemma contr_one_two_left_eq_contrOneTwoLeft_tprod {c1 c2 : S.C} (x : S.F.obj (Ov
   subst hx
   subst hy
   conv_rhs =>
-    rw [contrOneTwoLeft_tprod_eq]
+    erw [contrOneTwoLeft_tprod_eq]
     rw [tensorToVec_inv_apply_expand]
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, mk_left,
     Functor.id_obj, mk_hom, contr_tensor, prod_tensor, Action.instMonoidalCategory_tensorObj_V,
@@ -191,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. -/
@@ -230,7 +232,7 @@ lemma contr_two_two_inner_tprod (c : S.C) (x : S.F.obj (OverColor.mk ![c, c]))
     (OverColor.Discrete.pairIsoSep S.FD).inv.hom y))))))) := by
   subst hx
   subst hy
-  rw [Discrete.pairIsoSep_inv_tprod S.FD fx, Discrete.pairIsoSep_inv_tprod S.FD fy]
+  erw [Discrete.pairIsoSep_inv_tprod S.FD fx, Discrete.pairIsoSep_inv_tprod S.FD fy]
   change _ = (S.F.map (OverColor.mkIso _).hom).hom ((OverColor.Discrete.pairIsoSep S.FD).hom.hom
     ((fx (0 : Fin 2) ⊗ₜ[k] (λ_ (S.FD.obj { as := S.τ c }).V).hom
       ((S.contr.app { as := c }).hom (fx (1 : Fin 2)

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