From baf5169171aa1062d7210a2e4c842f925a11fda1 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 21 Oct 2024 14:28:02 +0000
Subject: [PATCH] fix: Correct tensor evaluation

---
 HepLean/Tensors/ComplexLorentz/Lemmas.lean | 19 +++++++++++++++++--
 HepLean/Tensors/Tree/Basic.lean            |  1 +
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/HepLean/Tensors/ComplexLorentz/Lemmas.lean b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
index 009a5fa0..6d9b1134 100644
--- a/HepLean/Tensors/ComplexLorentz/Lemmas.lean
+++ b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
@@ -89,7 +89,8 @@ lemma contr_rank_2_symm {T1 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
     rw [perm_perm]
     rw [perm_eq_id]
     · rfl
-    · rfl
+    · apply OverColor.Hom.ext
+      rfl
   · apply OverColor.Hom.ext
     ext x
     exact Fin.elim0 x
@@ -104,6 +105,7 @@ lemma contr_rank_2_symm' {T1 : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
   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}
     {S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
@@ -120,7 +122,20 @@ lemma antiSymm_contr_symm {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V
   rw [contr_tensor_eq (contr_tensor_eq (neg_fst_prod _ _))]
   rw [contr_tensor_eq (neg_contr _)]
   rw [neg_contr]
-  rfl
+  rw [neg_tensor]
+  apply congrArg
+  rw [contr_tensor_eq (contr_tensor_eq (prod_perm_left _ _ _ _))]
+  rw [contr_tensor_eq (perm_contr _ _)]
+  rw [perm_contr]
+  rw [perm_tensor_eq (contr_tensor_eq (contr_tensor_eq (prod_perm_right _ _ _ _)))]
+  rw [perm_tensor_eq (contr_tensor_eq (perm_contr _ _))]
+  rw [perm_tensor_eq (perm_contr _ _)]
+  rw [perm_perm]
+  nth_rewrite 1 [perm_tensor_eq (contr_contr _ _ _)]
+  rw [perm_perm]
+  rw [perm_eq_id]
+  · rfl
+  · rfl
 
 lemma symm_contr_antiSymm {S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
     {A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean
index ff0e385b..f048315c 100644
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@@ -448,6 +448,7 @@ noncomputable section
   Note: This function is not fully defined yet. -/
 def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (OverColor.mk c) := fun
   | tensorNode t => t
+  | twoNode t => (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom t
   | constTwoNode t => (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom (t.hom (1 : S.k))
   | add t1 t2 => t1.tensor + t2.tensor
   | perm σ t => (S.F.map σ).hom t.tensor