Theorem: piFinSuccCastSucc_symm_apply_castSucc_succ (Controlbits/Equivs.lean)

State before:
α : Type u_1
n : ℕ
a b : α
v : Fin n → α
i : Fin n
⊢ piFinSuccCastSucc.symm ((a, b), v) i.castSucc.succ = v i
Tactic:
simp only [piFinSuccCastSucc, Equiv.instTrans_trans, Equiv.symm_trans_apply, Equiv.symm_symm,
  Equiv.prodAssoc_apply, Equiv.prodCongr_symm, Equiv.refl_symm, Equiv.prodCongr_apply,
  Equiv.coe_refl, Equiv.piFinSuccAbove_symm_apply, insertNth_last', Prod_map, id_eq,
  Equiv.piFinSucc_symm_apply, cons_succ, snoc_castSucc]
State after:
no goals