Theorem: piFinSuccCastSucc_symm_apply_last (Controlbits/Equivs.lean)

State before:
α : Type u_1
n : ℕ
a b : α
v : Fin n → α
⊢ piFinSuccCastSucc.symm ((a, b), v) (last (n + 1)) = b
Tactic:
simp_rw [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_snoc_eq_snoc_cons, snoc_last]
State after:
no goals