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

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

State before:
π : Equiv.Perm (Fin 2)
⊢ π 0 = (if π 0 = 1 then Equiv.swap 0 1 else 1) 0 ∧ π 1 = (if π 0 = 1 then Equiv.swap 0 1 else 1) 1
Tactic:
rcases (exists_fin_two.mp ⟨π 0, rfl⟩) with (h0 | h0) <;>
rcases (exists_fin_two.mp ⟨π 1, rfl⟩) with (h1 | h1) <;>
simp only [h0, ite_true, Equiv.swap_apply_left, h1, Equiv.swap_apply_right, one_eq_zero_iff, id_eq,
  OfNat.ofNat_ne_one, and_false, zero_eq_one_iff, ite_false, Equiv.Perm.coe_one,  and_self] <;>
exact (zero_ne_one ((EmbeddingLike.apply_eq_iff_eq _).mp (h0.trans (h1.symm)))).elim
State after:
no goals