To Complex contr P basis Vector

lemma toComplex_contrP_basisVector {n : ℕ} {c : Fin (n + 1 + 1) → realLorentzTensor.Color}    {i j : Fin (n + 1 + 1)} (h : i ≠ j ∧ (realLorentzTensor).τ (c i) = c j)    (b : ComponentIdx (S := realLorentzTensor) c) :    toComplex (c := c ∘ Fin.succSuccAbove i j)      (Pure.contrP (S := realLorentzTensor) i j h (Pure.basisVector c b))      =    Pure.contrP (S := complexLorentzTensor) i j      (by        simpa [Function.comp_apply] using And.intro h.1          (by simpa [tau_colorToComplex] using congrArg colorToComplex h.2))      (Pure.basisVector (colorToComplex ∘ c) (ComponentIdx.complexify b)) := by  let c' := c ∘ Fin.succSuccAbove i j  simp only [Pure.contrP]  rw [toComplex_map_smul c' (Pure.contrPCoeff i j h (Pure.basisVector c b))    ((Pure.dropPair i j h.1 (Pure.basisVector c b)).toTensor),    Pure.dropPair_basisVector (c := c),    ← Tensor.basis_apply (S := realLorentzTensor) c' (fun k => b (Fin.succSuccAbove i j k)),    toComplex_basis (c := c') (i := fun k => b (Fin.succSuccAbove i j k))]  congr 1  · -- contrPCoeff: real and complex both equal 0 or 1 with same condition    rw [contrPCoeff_basis, complexLorentzTensor.contrPCoeff_basis]    simp only [Function.comp_apply, ComponentIdx.complexify_apply, Nat.reduceAdd, Fin.cast_cast,      Fin.cast_inj, EmbeddingLike.apply_eq_iff_eq]    split <;> simp_all  · -- complexify(fun k => b (succSuccAbove k)) = (complexify b) ∘ succSuccAbove    rw [Pure.dropPair_basisVector, ← Tensor.basis_apply]    exact congr_arg _ (funext fun m => ComponentIdx.complexify_comp_succSuccAbove b m)