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

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

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