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

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

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