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

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

State before:
π : Equiv.Perm (Fin 2)
⊢ ((if π 0 = 1 then Equiv.swap 0 1 else 1) * if π 0 = 1 then Equiv.swap 0 1 else 1) = 1
Tactic:
split_ifs
State after:
case pos
π : Equiv.Perm (Fin 2)
h✝ : π 0 = 1
⊢ Equiv.swap 0 1 * Equiv.swap 0 1 = 1

case neg
π : Equiv.Perm (Fin 2)
h✝ : ¬π 0 = 1
⊢ 1 * 1 = 1

State before:
case pos
π : Equiv.Perm (Fin 2)
h✝ : π 0 = 1
⊢ Equiv.swap 0 1 * Equiv.swap 0 1 = 1
Tactic:
rw [Equiv.swap_mul_self]
State after:
no goals

State before:
case neg
π : Equiv.Perm (Fin 2)
h✝ : ¬π 0 = 1
⊢ 1 * 1 = 1
Tactic:
rw [mul_one]
State after:
no goals