Conj T contr T

lemma conjT_contrT {n : ℕ} {c : Fin (n + 1 + 1) → C} (i j : Fin (n + 1 + 1))    (h : i ≠ j ∧ S.τ (c i) = c j) (t : S.Tensor c) :    S.conjT (contrT n i j h t)      = contrT n i j (S.contrCond_bar h) (S.conjT t) := by  apply componentMap_ext  intro φ  rw [componentMap_conjT, componentMap_eq_repr, Tensor.contrT_basis_repr_apply]  have hrhs := Tensor.contrT_basis_repr_apply (S := S.toTensorSpecies) (c := fun i => S.bar (c i))    (i := i) (j := j) (S.contrCond_bar h) (S.conjT t) φ  rw [componentMap_eq_repr]  refine Eq.trans ?_ hrhs.symm  rw [star_sum]  -- `componentReindex` carries the `bar`-side contraction section onto the `c`-side one: it  -- commutes with `dropPair` definitionally, so the section bijection is just `subtypeEquiv`.  have hmem : ∀ a : ComponentIdx (S := S.toTensorSpecies) (S.bar ∘ c),      a ∈ ComponentIdx.DropPairSection φ ↔        S.componentReindex c a ∈          ComponentIdx.DropPairSection (S.componentReindex (c ∘ i.succSuccAbove j) φ) := by    intro a    simp only [ComponentIdx.DropPairSection, Finset.mem_filter, Finset.mem_univ, true_and]    exact (Equiv.apply_eq_iff_eq (S.componentReindex (c ∘ i.succSuccAbove j))).symm  refine (Finset.sum_equiv (Equiv.subtypeEquiv (S.componentReindex c) hmem)    ?_ ?_).symm  · exact fun _ => iff_of_true (Finset.mem_attach _ _) (Finset.mem_attach _ _)  intro b'' _  simp only [Equiv.subtypeEquiv_apply]  erw [← componentMap_eq_repr (S.bar ∘ c), componentMap_conjT, componentMap_eq_repr c t,    star_mul']  congr 1  rw [S.conj_contrComm (c i) ((S.componentReindex c b''.1) i)        (basisIdxCongr (by rw [h.2]) ((S.componentReindex c b''.1) j)),    show (S.componentReindex c b''.1) i = Equiv.cast (S.barIdx_eq (c i)) (b''.1 i) from rfl,    show (S.componentReindex c b''.1) j = Equiv.cast (S.barIdx_eq (c j)) (b''.1 j) from rfl,    Equiv.symm_apply_apply]  congr 2  exact congrArg (b (S.τ (S.bar (c i)))) (basisIdxCongr_heq_arg _ _    (HEq.symm ((cast_heq _ _).trans ((cast_heq _ _).trans (cast_heq _ _)))))