Theorem: piFinSuccCastSucc_apply_fst_fst (Controlbits/Equivs.lean)

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