From aff9c88f99c745a80b60a02defb8e0e614751269 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 31 Oct 2024 19:52:07 +0000
Subject: [PATCH] feat: Add informal lemma

---
 HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
index e693f34..b795431 100644
--- a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
@@ -88,6 +88,16 @@ lemma tensorNode_coBispinorDown (p : complexCo) :
 
 -/
 
+informal_lemma contrBispinorUp_eq_metric_contr_contrBispinorDown where
+  math :≈ "{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ"
+  proof :≈ "Expand `contrBispinorDown` and use fact that metrics contract to the identity."
+  deps :≈ [``contrBispinorUp, ``contrBispinorDown, ``leftMetric, ``rightMetric]
+
+informal_lemma coBispinorUp_eq_metric_contr_coBispinorDown where
+  math :≈ "{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ"
+  proof :≈ "Expand `coBispinorDown` and use fact that metrics contract to the identity."
+  deps :≈ [``coBispinorUp, ``coBispinorDown, ``leftMetric, ``rightMetric]
+
 lemma contrBispinorDown_expand (p : complexContr) :
     {contrBispinorDown p | α β}ᵀ.tensor =
     {εL' | α α' ⊗ εR' | β β' ⊗