Theorem: Fin.rev_castSucc_succ (Controlbits/Fin.lean)

State before:
m : ℕ
i : Fin m
⊢ i.castSucc.succ.rev = i.rev.castSucc.succ
Tactic:
simp_rw [rev_succ, rev_castSucc, succ_castSucc]
State after:
no goals