Theorem: piFinSuccCastSucc_symm_apply_succ_castSucc (Controlbits/Equivs.lean)

State before:
α : Type u_1
n : ℕ
a b : α
v : Fin n → α
i : Fin n
⊢ piFinSuccCastSucc.symm ((a, b), v) i.succ.castSucc = v i
Tactic:
rw [<- succ_castSucc, piFinSuccCastSucc_symm_apply_castSucc_succ]
State after:
no goals