feat: Add example for complex lorentz

HepLean/Tensors/ComplexLorentz/Lemmas.lean

@@ -9,6 +9,8 @@ import Mathlib.LinearAlgebra.TensorProduct.Basis
 import HepLean.Tensors.Tree.NodeIdentities.Basic
 import HepLean.Tensors.Tree.NodeIdentities.PermProd
 import HepLean.Tensors.Tree.NodeIdentities.PermContr
+import HepLean.Tensors.Tree.NodeIdentities.ProdComm
+import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
 import HepLean.Tensors.Tree.NodeIdentities.ContrContr
 /-!
 
@@ -72,6 +74,39 @@ lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ :
     | (0 : Fin 2) => rfl
     | (1 : Fin 2) => rfl
 
+
+set_option maxRecDepth 20000 in
+lemma contr_rank_2_symm {T1 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
+    {T2 : (Lorentz.complexCo ⊗ Lorentz.complexCo).V} :
+    {(T1 | μ ν ⊗ T2 | μ ν) = (T2 | μ ν ⊗ T1 | μ ν)}ᵀ := by
+  rw [perm_tensor_eq (contr_tensor_eq (contr_tensor_eq (prod_comm _ _ _ _)))]
+  rw [perm_tensor_eq (contr_tensor_eq (perm_contr _ _))]
+  rw [perm_tensor_eq (perm_contr _ _)]
+  rw [perm_perm]
+  rw [perm_eq_id]
+  · rw [(contr_tensor_eq (contr_swap _ _))]
+    rw [perm_contr]
+    rw [perm_tensor_eq (contr_swap _ _)]
+    rw [perm_perm]
+    rw [perm_eq_id]
+    · rfl
+    · apply OverColor.Hom.ext
+      rfl
+  · apply OverColor.Hom.ext
+    ext x
+    exact Fin.elim0 x
+
+lemma contr_rank_2_symm' {T1 : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
+    {T2 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V} :
+    {(T1 | μ ν ⊗ T2 | μ ν) = (T2 | μ ν ⊗ T1 | μ ν)}ᵀ := by
+  rw [perm_tensor_eq contr_rank_2_symm]
+  rw [perm_perm]
+  rw [perm_eq_id]
+  apply OverColor.Hom.ext
+  ext x
+  exact Fin.elim0 x
+
+
 set_option maxRecDepth 20000 in
 /-- Contracting a rank-2 anti-symmetric tensor with a rank-2 symmetric tensor gives zero. -/
 lemma antiSymm_contr_symm {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
@@ -105,6 +140,15 @@ lemma antiSymm_contr_symm {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V
   · apply OverColor.Hom.ext
     rfl
 
+lemma symm_contr_antiSymm {S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
+    {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
+    (hA : {A | μ ν = - (A | ν μ)}ᵀ) (hs : {S | μ ν = S | ν μ}ᵀ) :
+    {S | μ ν ⊗ A | μ ν}ᵀ.tensor = 0 := by
+  rw [contr_rank_2_symm']
+  rw [perm_tensor]
+  rw [antiSymm_contr_symm hA hs]
+  rfl
+
 end Fermion
 
 end

HepLean/Tensors/Tree/NodeIdentities/ContrSwap.lean

@@ -113,7 +113,8 @@ lemma contrMap_swap : q.contrMap = q.swap.contrMap ≫ S.F.map q.contrSwapHom :=
     · change _ = ((S.FDiscrete.map (Discrete.eqToHom _)) ≫ S.FDiscrete.map (Discrete.eqToHom _)).hom
         ( (x (q.swap.i.succAbove q.swap.j)))
       rw [← S.FDiscrete.map_comp]
-      simp
+      simp only [Nat.succ_eq_add_one, mk_hom, Discrete.functor_obj_eq_as, Function.comp_apply,
+        eqToHom_trans]
       have h1nn' {a b d: Fin n.succ.succ} (hbd : b = d) (h : c d = S.τ (S.τ (c a))):
           (S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
           (S.FDiscrete.map (eqToHom (by