Contr T eval T

lemma contrT_evalT {n : ℕ} {c : Fin (n + 1 + 1 + 1) → C}    (k : Fin (n + 1 + 1 + 1)) (i j : Fin (n + 1 + 1)) (φ : basisIdx (c k))    (hij : i ≠ j ∧ S.τ ((c ∘ k.succAbove) i) = (c ∘ k.succAbove) j) (t : Tensor S c) :    contrT n i j hij (evalT k φ t) =    permT id (.succAbove_succSuccAbove_comm k i j hij.1)      (evalT (Fin.predPredAbove (k.succAbove i) (k.succAbove j) (by simp [hij.1]) k (by simp))        (basisIdxCongr (by simp) φ)        (contrT (n + 1) (k.succAbove i) (k.succAbove j) ⟨by simp [hij.1], hij.2⟩ t)) := by  induction' t using Tensor.induction_on_basis with b a t hb t1 t2 hb1 hb2  · have hs : Pure.contrPCoeff i j hij          (Pure.basisVector (c ∘ k.succAbove) (fun m => b (k.succAbove m))) =        Pure.contrPCoeff (k.succAbove i) (k.succAbove j) ⟨by simp [hij.1], hij.2⟩          (Pure.basisVector c b) := rfl    conv_lhs => rw [evalT_basis]    conv_rhs => rw [contrT_basis, map_smul, evalT_basis]    rw [apply_ite (contrT n i j hij), map_zero, contrT_basis, hs, map_smul,      apply_ite (permT id (IsReindexing.succAbove_succSuccAbove_comm k i j hij.1)), map_zero,      permT_basis, smul_ite, smul_zero]    have hidx : ∀ m, (k.succAbove i).succSuccAbove (k.succAbove j)        (((k.succAbove i).predPredAbove (k.succAbove j) (by simp [hij.1]) k (by simp)).succAbove m)        = k.succAbove (i.succSuccAbove j m) := by      intro m      apply Fin.val_injective      simp only [Fin.succSuccAbove, Fin.succAbove, Fin.predPredAbove, Fin.lt_def,        Fin.val_castSucc, Fin.val_succ, apply_ite Fin.val, apply_dite Fin.val]      grind (splits := 60)    have hk : (k.succAbove i).succSuccAbove (k.succAbove j)        ((k.succAbove i).predPredAbove (k.succAbove j) (by simp [hij.1]) k (by simp)) = k := by simp    have hcond : (ComponentIdx.dropPair (k.succAbove i) (k.succAbove j) b          ((k.succAbove i).predPredAbove (k.succAbove j) (by simp [hij.1]) k (by simp)) =          basisIdxCongr (by simp) φ) = (b k = φ) := by      simp only [ComponentIdx.dropPair]      rw [ComponentIdx.congr_right b _ k hk, eq_iff_iff]      exact (basisIdxCongr _).apply_eq_iff_eq    simp only [hcond]    split_ifs with hbk    · congr 1      congr 1      funext m      simp only [ComponentIdx.dropPair, id_eq]      exact ComponentIdx.congr_right b _ _ (hidx m).symm    · rfl  · simp  · simp only [map_smul, hb]  · simp only [map_add, hb1, hb2]