diff --git a/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean b/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
index 6e63defe..a7e1f22a 100644
--- a/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
+++ b/PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean
@@ -143,10 +143,29 @@ 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 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 (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
 
 /-- The map `toComplex` commutes with evalT. -/
 informal_lemma evalT_toComplex where