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

State before:
m : ℕ
i : Fin (m + 1)
⊢ i.rev = 0 ↔ i = last m
Tactic:
convert rev_inj
State after:
case h.e'_1.h.e'_3.h
m : ℕ
i : Fin (m + 1)
⊢ 0 = (last m).rev

State before:
case h.e'_1.h.e'_3.h
m : ℕ
i : Fin (m + 1)
⊢ 0 = (last m).rev
Tactic:
exact (rev_last m).symm
State after:
no goals