fix: Slow builds with tensors

HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean

@@ -63,17 +63,18 @@ lemma tensorNode_pauliContr : {pauliContr | μ α β}ᵀ.tensor =
 
 /-- The definitional tensor node relation for `pauliCo`. -/
 lemma tensorNode_pauliCo : {pauliCo | μ α β}ᵀ.tensor =
-    {η' | μ ν ⊗ PauliMatrix.asConsTensor | ν α β}ᵀ.tensor := by
-  rfl
+    {η' | μ ν ⊗ pauliContr | ν α β}ᵀ.tensor := by
+  rw [pauliCo, tensorNode_tensor]
 
 /-- The definitional tensor node relation for `pauliCoDown`. -/
 lemma tensorNode_pauliCoDown : {pauliCoDown | μ α β}ᵀ.tensor =
     {pauliCo | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.tensor := by
-  rfl
+  rw [pauliCoDown, tensorNode_tensor]
 
 /-- The definitional tensor node relation for `pauliContrDown`. -/
 lemma tensorNode_pauliContrDown : {pauliContrDown | μ α β}ᵀ.tensor =
     {pauliContr | μ α β ⊗ εL' | α α' ⊗ εR' | β β'}ᵀ.tensor := by
+  rw [pauliContr, tensorNode_tensor]
   rfl
 
 /-!
@@ -200,10 +201,15 @@ lemma action_pauliCo (g : SL(2,ℂ)) : {g •ₐ pauliCo | μ α β}ᵀ.tensor =
   conv =>
     lhs
     rw [action_tensor_eq <| tensorNode_pauliCo]
+    rw [action_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_pauliContr]
     rw [(contr_action _ _).symm]
     rw [contr_tensor_eq <| (prod_action _ _ _).symm]
     rw [contr_tensor_eq <| prod_tensor_eq_fst <| action_constTwoNode _ _]
     rw [contr_tensor_eq <| prod_tensor_eq_snd <| action_constThreeNode _ _]
+  conv =>
+    rhs
+    rw [tensorNode_pauliCo]
+    rw [contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_pauliContr]
   rfl
 
 /-- The tensor `pauliCoDown` is invariant under the action of `SL(2,ℂ)`. -/
@@ -219,9 +225,11 @@ lemma action_pauliCoDown (g : SL(2,ℂ)) : {g •ₐ pauliCoDown | μ α β}ᵀ.
     rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_fst <|
       action_pauliCo _]
     rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_snd <|
-      action_constTwoNode _ _]
-    erw [contr_tensor_eq <| prod_tensor_eq_snd <| action_constTwoNode _ _]
-  rfl
+      action_altLeftMetric _]
+    rw [contr_tensor_eq <| prod_tensor_eq_snd <| action_altRightMetric _]
+  conv =>
+    rhs
+    rw [tensorNode_pauliCoDown]
 
 /-- The tensor `pauliContrDown` is invariant under the action of `SL(2,ℂ)`. -/
 lemma action_pauliContrDown (g : SL(2,ℂ)) : {g •ₐ pauliContrDown | μ α β}ᵀ.tensor =
@@ -236,8 +244,10 @@ lemma action_pauliContrDown (g : SL(2,ℂ)) : {g •ₐ pauliContrDown | μ α
     rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_fst <|
       action_pauliContr _]
     rw [contr_tensor_eq <| prod_tensor_eq_fst <| contr_tensor_eq <| prod_tensor_eq_snd <|
-      action_constTwoNode _ _]
-    erw [contr_tensor_eq <| prod_tensor_eq_snd <| action_constTwoNode _ _]
-  rfl
+      action_altLeftMetric _]
+    erw [contr_tensor_eq <| prod_tensor_eq_snd <| action_altRightMetric _]
+  conv =>
+    rhs
+    rw [tensorNode_pauliContrDown]
 
 end complexLorentzTensor

HepLean/Tensors/ComplexLorentz/PauliMatrices/Basis.lean

@@ -458,15 +458,10 @@ lemma pauliMatrix_contr_down_2 :
   conv =>
     lhs
     simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
-  congr 1
-  · rw [basisVectorContrPauli]
-    congr 2
-    funext k
-    fin_cases k <;> rfl
-  · rw [basisVectorContrPauli]
-    congr 2
-    funext k
-    fin_cases k <;> rfl
+  rw [basisVectorContrPauli, basisVectorContrPauli]
+  congr 3
+  · decide
+  · decide
 
 lemma pauliMatrix_contr_down_3 :
     {(basisVector ![Color.down, Color.down] fun x => 3) | μ ν ⊗
@@ -503,16 +498,10 @@ lemma pauliMatrix_contr_down_3 :
   conv =>
     lhs
     simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
-  congr 1
-  · rw [basisVectorContrPauli]
-    congr 1
-    funext k
-    fin_cases k <;> rfl
-  · rw [basisVectorContrPauli]
-    congr 1
-    congr 1
-    funext k
-    fin_cases k <;> rfl
+  rw [basisVectorContrPauli, basisVectorContrPauli]
+  congr 3
+  · decide
+  · decide
 
 /-- The expansion of `pauliCo` in terms of a basis. -/
 lemma pauliCo_basis_expand : pauliCo

HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean

@@ -139,6 +139,34 @@ lemma sum_inr_succAbove_leftContrI_leftContrJ (k : Fin n1) : finSumFinEquiv.symm
   erw [succAbove_leftContrJ_leftContrI_natAdd]
   simp
 
+/- An auxillary lemma to `contrMap_prod_tprod`. -/
+lemma contrMap_prod_tprod_aux
+    (l : (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)).left ⊕ (OverColor.mk c1).left)
+    (l' : Fin n.succ.succ ⊕ Fin n1)
+    (h : Sum.elim c c1 l' = Sum.elim (c ∘ q.i.succAbove ∘ q.j.succAbove) c1 l)
+    (h' : l' = (Sum.map (q.i.succAbove ∘ q.j.succAbove) id l))
+    (p : (i : (𝟭 Type).obj (OverColor.mk c).left) →
+      CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c).hom i }))
+    (q' : (i : (𝟭 Type).obj (OverColor.mk c1).left) →
+      CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c1).hom i })) :
+    (lift.discreteSumEquiv S.FDiscrete l)
+    (HepLean.PiTensorProduct.elimPureTensor
+    (fun k => p (q.i.succAbove (q.j.succAbove k))) q' l) =
+    (S.FDiscrete.map (eqToHom (by simp [h]))).hom
+    ((lift.discreteSumEquiv S.FDiscrete l')
+    (HepLean.PiTensorProduct.elimPureTensor p q' l')) := by
+  subst h'
+  match l with
+  | Sum.inl l =>
+    simp only [instMonoidalCategoryStruct_tensorObj_hom, mk_hom,
+      Sum.elim_inl, Function.comp_apply, Functor.id_obj, Sum.map_inl, eqToHom_refl,
+      Discrete.functor_map_id, Action.id_hom, ModuleCat.id_apply]
+    rfl
+  | Sum.inr l =>
+    simp only [instMonoidalCategoryStruct_tensorObj_hom, mk_hom, Sum.elim_inr, Functor.id_obj,
+      Function.comp_apply, Sum.map_inr, Discrete.functor_map_id, Action.id_hom]
+    rfl
+
 lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) →
     CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c).hom i }))
     (q' : (i : (𝟭 Type).obj (OverColor.mk c1).left) →
@@ -183,7 +211,6 @@ lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) →
           ModuleCat.id_apply]
         rfl
   congr 1
-  /- The contraction. -/
   · apply congrArg
     simp only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V,
       Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
@@ -234,28 +261,7 @@ lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) →
       Iso.refl_hom, Action.id_hom, Iso.refl_inv, instMonoidalCategoryStruct_tensorObj_hom,
       LinearEquiv.ofLinear_apply, Equiv.toFun_as_coe, equivToIso_mkIso_hom, Equiv.refl_symm,
       Functor.mapIso_hom, eqToIso.hom, Functor.mapIso_inv, eqToIso.inv]
-    have h1 (l : (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)).left ⊕ (OverColor.mk c1).left)
-        (l' : Fin n.succ.succ ⊕ Fin n1)
-        (h : Sum.elim c c1 l' = Sum.elim (c ∘ q.i.succAbove ∘ q.j.succAbove) c1 l)
-        (h' : l' = (Sum.map (q.i.succAbove ∘ q.j.succAbove) id l)) :
-        (lift.discreteSumEquiv S.FDiscrete l)
-        (HepLean.PiTensorProduct.elimPureTensor
-        (fun k => p (q.i.succAbove (q.j.succAbove k))) q' l) =
-        (S.FDiscrete.map (eqToHom (by simp [h]))).hom
-        ((lift.discreteSumEquiv S.FDiscrete l')
-        (HepLean.PiTensorProduct.elimPureTensor p q' l')) := by
-      subst h'
-      match l with
-      | Sum.inl l =>
-        simp only [instMonoidalCategoryStruct_tensorObj_hom, mk_hom,
-          Sum.elim_inl, Function.comp_apply, Functor.id_obj, Sum.map_inl, eqToHom_refl,
-          Discrete.functor_map_id, Action.id_hom, ModuleCat.id_apply]
-        rfl
-      | Sum.inr l =>
-        simp only [instMonoidalCategoryStruct_tensorObj_hom, mk_hom, Sum.elim_inr, Functor.id_obj,
-          Function.comp_apply, Sum.map_inr, Discrete.functor_map_id, Action.id_hom]
-        rfl
-    refine h1 _ _ ?_ ?_
+    refine contrMap_prod_tprod_aux _ _ _ ?_ ?_ _ _
     · simpa using Discrete.eqToIso.proof_1
         (Hom.toEquiv_comp_inv_apply (mkIso (leftContr_map_eq q)).hom k)
     · obtain ⟨k, hk⟩ := finSumFinEquiv.surjective k