Contr T to Complex

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 ∘ Fin.succSuccAbove i j) (contrT (S := realLorentzTensor) n i j h t)      =    contrT (S := complexLorentzTensor) n i j (by        simpa [Function.comp_apply] using          And.intro h.1 (by            simpa [tau_colorToComplex] using congrArg colorToComplex h.2))      (toComplex (c := c) t) := by  induction t using induction_on_basis with  | h b =>    rw [Tensor.basis_apply (S := realLorentzTensor) c b,      contrT_pure (S := realLorentzTensor) (p := Pure.basisVector c b),      toComplex_pure_basisVector (c := c) b,      contrT_pure (S := complexLorentzTensor)        (p := Pure.basisVector (colorToComplex ∘ c) (ComponentIdx.complexify b))]    exact toComplex_contrP_basisVector h b  | hzero => simp  | hsmul r t ht => simp [map_smul, ht]  | hadd t1 t2 h1 h2 => simp [map_add, h1, h2]