Theorem: PFin2.inv_last_eq_fz (Qpf/MathlibPort/Fin2.lean)

State before:
n : ℕ
⊢ inv last = fz
Tactic:
induction n <;> simp [inv, last, weaken, *]
State after:
no goals