From 7a50680794a59c045c2c6e5dcc959c5a3823490c Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 29 Oct 2024 10:45:43 +0000
Subject: [PATCH] feat: add coBispinorDown_eq_pauliContrDown_contr

---
 .../ComplexLorentz/Bispinors/Basic.lean       | 44 ++++++++++++++++-
 .../ComplexLorentz/PauliMatrices/Basic.lean   | 49 +++++++++++++++++++
 2 files changed, 91 insertions(+), 2 deletions(-)

diff --git a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
index 83e1fd5..d0267f5 100644
--- a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
@@ -99,6 +99,12 @@ lemma contrBispinorDown_expand (p : complexContr) :
   rw [tensorNode_contrBispinorDown p]
   rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_contrBispinorUp p]
 
+lemma coBispinorDown_expand (p : complexCo) :
+    {coBispinorDown p | α β}ᵀ.tensor = {Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
+    (pauliContr | μ α β ⊗ p | μ)}ᵀ.tensor := by
+  rw [tensorNode_coBispinorDown p]
+  rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_coBispinorUp p]
+
 set_option maxRecDepth 5000 in
 lemma contrBispinorDown_eq_pauliCoDown_contr (p : complexContr) :
     {contrBispinorDown p | α β = pauliCoDown | μ α β ⊗ p | μ}ᵀ  := by
@@ -136,8 +142,42 @@ lemma contrBispinorDown_eq_pauliCoDown_contr (p : complexContr) :
   apply perm_congr _ rfl
   decide
 
-
-
+set_option maxRecDepth 5000 in
+lemma coBispinorDown_eq_pauliContrDown_contr (p : complexCo) :
+    {coBispinorDown p | α β = pauliContrDown | μ α β ⊗ p | μ}ᵀ  := by
+  conv =>
+    rhs
+    rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <| pauliContrDown_eq_metric_mul_pauliContr]
+    rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_left _ _ _ _]
+    rw [perm_tensor_eq <| perm_contr_congr 2 2]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
+    rw [perm_tensor_eq <| perm_contr_congr 2 2]
+    rw [perm_perm]
+    apply (perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_eq_id _ rfl _).trans
+    rw [perm_tensor_eq <| contr_tensor_eq <|  contr_tensor_eq <| contr_prod _ _ _]
+    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr_congr 1 3]
+    rw [perm_tensor_eq <| perm_contr_congr 2 2]
+    rw [perm_perm]
+    erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_eq_id _ rfl _]
+    rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_assoc' _ _ _ _ _ _]
+    rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_contr_congr 0 4]
+    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr_congr 1 3]
+    rw [perm_tensor_eq <| perm_contr_congr 2 2]
+    rw [perm_perm]
+  conv =>
+    lhs
+    rw [coBispinorDown_expand p]
+    rw [contr_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
+    rw [contr_tensor_eq <| perm_contr_congr 0 3]
+    rw [perm_contr_congr 1 2]
+    apply (perm_tensor_eq <| contr_tensor_eq <| contr_contr _ _ _).trans
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_contr _ _ _]
+    rw [perm_perm]
+  apply perm_congr _ rfl
+  decide
 
 end complexLorentzTensor
 end
diff --git a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
index fdc35eb..18e2e3f 100644
--- a/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/PauliMatrices/Basic.lean
@@ -135,5 +135,54 @@ lemma pauliCoDown_eq_metric_mul_pauliCo :
   apply perm_congr _ rfl
   decide
 
+set_option maxRecDepth 5000 in
+/-- A rearanging of `pauliContrDown` to place the pauli matrices on the right. -/
+lemma pauliContrDown_eq_metric_mul_pauliContr :
+   {pauliContrDown | μ α' β' = Fermion.altLeftMetric | α α' ⊗
+    Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ := by
+  conv =>
+    lhs
+    rw [tensorNode_pauliContrDown]
+    rw [contr_tensor_eq <| contr_prod _ _ _]
+    rw [perm_contr]
+    erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_eq_id _ rfl _]
+    rw [perm_tensor_eq <| contr_congr 1 2]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_tensor_eq <| contr_congr 1 2]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_congr 1 2]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_assoc' _ _ _ _ _ _]
+    rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
+    rw [perm_tensor_eq <| contr_tensor_eq <| perm_tensor_eq <| contr_congr 1 2]
+    rw [perm_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_congr 1 2]
+    rw [perm_perm]
+    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 <| contr_tensor_eq <| perm_tensor_eq <| contr_congr 5 0]
+    rw [perm_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_congr 4 1]
+    rw [perm_perm]
+  conv =>
+    rhs
+    rw [perm_tensor_eq <| contr_swap _ _]
+    rw [perm_perm]
+    erw [perm_tensor_eq <| contr_congr 4 1]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_tensor_eq <| contr_swap _ _]
+    erw [perm_tensor_eq <| contr_tensor_eq <| perm_tensor_eq <| contr_congr 5 0]
+    rw [perm_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _]
+    rw [perm_tensor_eq <| perm_contr _ _]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_congr 4 1]
+    rw [perm_perm]
+  apply perm_congr _ rfl
+  decide
 
 end complexLorentzTensor