To Complex eval P basis Vector

lemma toComplex_evalP_basisVector {n : ℕ} {c : Fin (n + 1) → realLorentzTensor.Color}    (i : Fin (n + 1)) (b : Fin 1 ⊕ Fin 3)    (b' : ComponentIdx (S := realLorentzTensor) c) :    toComplex (c := c ∘ i.succAbove)      (Pure.evalP (S := realLorentzTensor) i b (Pure.basisVector c b'))      =    permT (S := complexLorentzTensor) (σ := (id : Fin n → Fin n))      (by simp [Function.comp_apply])      (Pure.evalP (S := complexLorentzTensor) i (evalIdxToComplex (c := c) i b)        (Pure.basisVector (colorToComplex ∘ c) (ComponentIdx.complexify b'))) := by  simp only [Pure.evalP]  have hdrop : (Pure.basisVector c b').drop i =    Pure.basisVector (c ∘ i.succAbove) (fun k => b' (i.succAbove k)) := by    ext j; simp only [Pure.drop, Pure.basisVector, Function.comp_apply]  rw [hdrop, toComplex_map_smul (c ∘ i.succAbove) (Pure.evalPCoeff i b (Pure.basisVector c b'))    ((Pure.basisVector (c ∘ i.succAbove)) (fun k => b' (i.succAbove k)) |>.toTensor)]  · -- evalPCoeff: real and complex match; then tensor equality    simp only [Pure.evalPCoeff, Pure.basisVector, Basis.repr_self, Finsupp.single_apply,      ComponentIdx.complexify_apply, evalIdxToComplex]    · by_cases h : b' i = b      · simp [h]        have hdrop' : (Pure.basisVector (colorToComplex ∘ c) (ComponentIdx.complexify b')).drop i =          Pure.basisVector (colorToComplex ∘ (c ∘ i.succAbove))            (ComponentIdx.complexify (c := c ∘ i.succAbove) (fun k => b' (i.succAbove k))) := by          ext j; simp only [Pure.drop, Pure.basisVector, ComponentIdx.complexify_apply,            Function.comp_apply]        rw [hdrop']        exact (permT_id_self _).symm      · simp [h]