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

State before:
n : ℕ
i : Fin2 n
⊢ toFin2 (ofFin2 i) = i
Tactic:
induction i <;> simp [ofFin2, toFin2, *]
State after:
no goals