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

State before:
m : ℕ
i : Fin (m + 1)
⊢ i = 0 ↔ i.rev = last m
Tactic:
convert rev_rev i ▸ rev_eq_zero_iff_last
State after:
no goals