Merge pull request #272 from HEPLean/WickContract

Relation between Wick contractions and involutions, and the cardinality of full Wick contractions.

HepLean.lean

@@ -100,6 +100,7 @@ import HepLean.Lorentz.Weyl.Modules
 import HepLean.Lorentz.Weyl.Two
 import HepLean.Lorentz.Weyl.Unit
 import HepLean.Mathematics.Fin
+import HepLean.Mathematics.Fin.Involutions
 import HepLean.Mathematics.LinearMaps
 import HepLean.Mathematics.List
 import HepLean.Mathematics.PiTensorProduct
@@ -114,6 +115,7 @@ import HepLean.Meta.Notes.NoteFile
 import HepLean.Meta.Notes.ToHTML
 import HepLean.Meta.TransverseTactics
 import HepLean.PerturbationTheory.Contractions.Basic
+import HepLean.PerturbationTheory.Contractions.Card
 import HepLean.PerturbationTheory.Contractions.Involutions
 import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
 import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar

HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean

@@ -485,7 +485,7 @@ lemma pauliMatrix_contr_down_3 :
     rw [contrBasisVectorMul_pos _]
   conv =>
     lhs; rhs; rhs; lhs;
-    rw [contrBasisVectorMul_pos  _]
+    rw [contrBasisVectorMul_pos _]
   conv =>
     lhs
     simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]

HepLean/Mathematics/Fin.lean

@@ -101,7 +101,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
         · rw [Fin.succAbove_of_castSucc_lt _ _]
           exact hx1
         · rw [Fin.lt_def] at h1 hx1 ⊢
-          simp_all
+          simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc]
           omega
       · exact Nat.lt_trans hx1 h1
     · simp only [not_lt] at hx1
@@ -115,7 +115,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
           · rfl
           · exact hx1
         · rw [Fin.lt_def] at hx2 ⊢
-          simp_all
+          simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc, Fin.val_succ]
           omega
       · simp only [Nat.succ_eq_add_one, not_lt] at hx2
         rw [Fin.succAbove_of_le_castSucc _ _ hx2]
@@ -135,12 +135,12 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
       · nth_rewrite 2 [Fin.succAbove_of_le_castSucc _ _]
         · rw [Fin.succAbove_of_le_castSucc _ _]
           rw [Fin.le_def] at hx1 ⊢
-          simp_all
+          simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc, Fin.val_succ, add_le_add_iff_right]
         · rw [Fin.le_def] at h1 hx1 ⊢
-          simp_all
+          simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc]
           omega
       · rw [Fin.le_def] at hx1 h1 ⊢
-        simp_all
+        simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc, Fin.val_succ]
         omega
     · simp only [Nat.succ_eq_add_one, not_le] at hx1
       rw [Fin.lt_def] at hx1
@@ -151,7 +151,7 @@ lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x :
         nth_rewrite 2 [Fin.succAbove_of_castSucc_lt _ _]
         · rw [Fin.succAbove_of_castSucc_lt _ _]
           rw [Fin.lt_def] at hx2 ⊢
-          simp_all
+          simp_all only [Nat.succ_eq_add_one, Fin.coe_castSucc, Fin.val_succ]
           omega
         · rw [Fin.lt_def] at hx2 ⊢
           simp_all