Theorem: piFinSuccCastSucc_apply_fst_snd (Controlbits/Equivs.lean)

State before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ (piFinSuccCastSucc v).1.2 = v (last (n + 1))
Tactic:
simp_rw [piFinSuccCastSucc_apply]
State after:
no goals