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

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

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