Theorem: piFinSuccCastSucc_apply_snd (Controlbits/Equivs.lean)

State before:
n : ℕ
α : Type u_1
v : Fin (n + 2) → α
⊢ (piFinSuccCastSucc v).2 = v ∘ fun i => i.castSucc.succ
Tactic:
simp only [piFinSuccCastSucc_apply]
State after:
no goals