Theorem: Fin.perm_fin_two_of_fix_zero (Controlbits/PermFintwo.lean)

State before:
π : Equiv.Perm (Fin 2)
h : π 0 = 0
⊢ π = 1
Tactic:
rw [perm_fin_two π]
State after:
π : Equiv.Perm (Fin 2)
h : π 0 = 0
⊢ (if π 0 = 1 then Equiv.swap 0 1 else 1) = 1

State before:
π : Equiv.Perm (Fin 2)
h : π 0 = 0
⊢ (if π 0 = 1 then Equiv.swap 0 1 else 1) = 1
Tactic:
simp_rw [h, zero_eq_one_iff, OfNat.ofNat_ne_one, ite_false]
State after:
no goals