From 58a31d76a81aff76681493abf05b4f2c99b39753 Mon Sep 17 00:00:00 2001
From: kastch <kastch>
Date: Fri, 23 Jan 2026 11:36:06 -0300
Subject: [PATCH 1/2] 7RKFR: Replaced informal with sorryful

---
 .../Tensors/RealTensor/ToComplex.lean         | 37 +++++++++++++++++--
 1 file changed, 34 insertions(+), 3 deletions(-)

diff --git a/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean b/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
index 6e63defe..8b7d2995 100644
--- a/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
+++ b/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
@@ -143,10 +143,41 @@ informal_lemma prodT_toComplex where
   deps := [``prodT]
   tag := "7RKFF"
 
+/-- `τ` commutes with `colorToComplex` on the Lorentz `up/down` colors. -/
+@[simp]
+lemma tau_colorToComplex (x : realLorentzTensor.Color) :
+    (complexLorentzTensor).τ (colorToComplex x) = colorToComplex ((realLorentzTensor).τ x) := by
+  cases x <;> rfl
+
+/-- The contraction condition is preserved under `colorToComplex`. -/
+@[simp]
+lemma contrCond_colorToComplex {n : ℕ}
+    {c : Fin (n + 1 + 1) → realLorentzTensor.Color} {i j : Fin (n + 1 + 1)}
+    (h : i ≠ j ∧ (realLorentzTensor).τ (c i) = c j) :
+    i ≠ j ∧ (complexLorentzTensor).τ ((colorToComplex ∘ c) i) = (colorToComplex ∘ c) j := by
+  refine And.intro h.1 ?_
+  have h2 : colorToComplex ((realLorentzTensor).τ (c i)) = colorToComplex (c j) :=
+    congrArg colorToComplex h.2
+  calc
+    (complexLorentzTensor).τ ((colorToComplex ∘ c) i)
+        = (complexLorentzTensor).τ (colorToComplex (c i)) := rfl
+    _ = colorToComplex ((realLorentzTensor).τ (c i)) := by
+          simp [tau_colorToComplex]
+    _ = (colorToComplex ∘ c) j := by
+          change colorToComplex ((realLorentzTensor).τ (c i)) = colorToComplex (c j)
+          exact h2
+
 /-- The map `toComplex` commutes with contrT. -/
-informal_lemma contrT_toComplex where
-  deps := [``contrT]
-  tag := "7RKFR"
+@[sorryful]
+lemma contrT_toComplex {n : ℕ}
+    {c : Fin (n + 1 + 1) → realLorentzTensor.Color} {i j : Fin (n + 1 + 1)}
+    (h : i ≠ j ∧ (realLorentzTensor).τ (c i) = c j) (t : ℝT(3, c)) :
+    toComplex (c := c ∘ Pure.dropPairEmb i j) (contrT (S := realLorentzTensor) n i j h t)
+      =
+    contrT (S := complexLorentzTensor) n i j
+      (contrCond_colorToComplex (c := c) (i := i) (j := j) h)
+      (toComplex (c := c) t) := by
+  sorry
 
 /-- The map `toComplex` commutes with evalT. -/
 informal_lemma evalT_toComplex where

From 03518907d2d20d4d8fb539b2f4c9a25caa7e8563 Mon Sep 17 00:00:00 2001
From: kastch <kastch>
Date: Fri, 23 Jan 2026 12:55:35 -0300
Subject: [PATCH 2/2] 7RKFR: Removed redundant lemma

---
 .../Tensors/RealTensor/ToComplex.lean         | 28 ++++++-------------
 1 file changed, 8 insertions(+), 20 deletions(-)

diff --git a/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean b/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
index 8b7d2995..a7e1f22a 100644
--- a/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
+++ b/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
@@ -149,24 +149,6 @@ lemma tau_colorToComplex (x : realLorentzTensor.Color) :
     (complexLorentzTensor).τ (colorToComplex x) = colorToComplex ((realLorentzTensor).τ x) := by
   cases x <;> rfl
 
-/-- The contraction condition is preserved under `colorToComplex`. -/
-@[simp]
-lemma contrCond_colorToComplex {n : ℕ}
-    {c : Fin (n + 1 + 1) → realLorentzTensor.Color} {i j : Fin (n + 1 + 1)}
-    (h : i ≠ j ∧ (realLorentzTensor).τ (c i) = c j) :
-    i ≠ j ∧ (complexLorentzTensor).τ ((colorToComplex ∘ c) i) = (colorToComplex ∘ c) j := by
-  refine And.intro h.1 ?_
-  have h2 : colorToComplex ((realLorentzTensor).τ (c i)) = colorToComplex (c j) :=
-    congrArg colorToComplex h.2
-  calc
-    (complexLorentzTensor).τ ((colorToComplex ∘ c) i)
-        = (complexLorentzTensor).τ (colorToComplex (c i)) := rfl
-    _ = colorToComplex ((realLorentzTensor).τ (c i)) := by
-          simp [tau_colorToComplex]
-    _ = (colorToComplex ∘ c) j := by
-          change colorToComplex ((realLorentzTensor).τ (c i)) = colorToComplex (c j)
-          exact h2
-
 /-- The map `toComplex` commutes with contrT. -/
 @[sorryful]
 lemma contrT_toComplex {n : ℕ}
@@ -174,8 +156,14 @@ lemma contrT_toComplex {n : ℕ}
     (h : i ≠ j ∧ (realLorentzTensor).τ (c i) = c j) (t : ℝT(3, c)) :
     toComplex (c := c ∘ Pure.dropPairEmb i j) (contrT (S := realLorentzTensor) n i j h t)
       =
-    contrT (S := complexLorentzTensor) n i j
-      (contrCond_colorToComplex (c := c) (i := i) (j := j) h)
+    contrT (S := complexLorentzTensor) n i j (by
+        -- если у simp достаточно информации, то это закрывается:
+        simpa [Function.comp_apply] using
+          And.intro h.1 (by
+            -- τ-совместимость
+            simpa [tau_colorToComplex] using congrArg colorToComplex h.2
+          )
+      )
       (toComplex (c := c) t) := by
   sorry