Prod T to Complex

lemma prodT_toComplex {n m : ℕ}    {c : Fin n → realLorentzTensor.Color}    {c1 : Fin m → realLorentzTensor.Color}    (t : ℝT(3, c)) (t1 : ℝT(3, c1)) :    toComplex (c := Fin.append c c1) (prodT (S := realLorentzTensor) t t1)      =    prodTColorToComplex (c := c) (c1 := c1)      (toComplex (c := c) t) (toComplex (c := c1) t1) := by  -- Double induction on the tensor basis: first over `t`, then over `t1`. The zero, scalar and  -- additive cases follow from linearity of `prodT`, `toComplex` and `prodTColorToComplex`.  induction t using induction_on_basis with  | h b =>    induction t1 using induction_on_basis with    | h b1 =>      simp [prodTColorToComplex, prodT_pure, permT_pure, Pure.prodP_basisVector,        Pure.permP_basisVector, Tensor.basis_apply, toComplex_pure_basisVector,        colorToComplex_append, basisIdxCongr_eq_cast]    | hzero => simp [prodTColorToComplex]    | hsmul r ta hta => simp [map_smul, hta, prodTColorToComplex]    | hadd ta tb hta htb => simp [map_add, hta, htb, prodTColorToComplex]  | hzero => simp [prodTColorToComplex]  | hsmul r ta hta => simp [map_smul, hta, prodTColorToComplex]  | hadd ta tb hta htb => simp [map_add, hta, htb, prodTColorToComplex]