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

State before:
x y : Equiv.Perm (Fin 2)
⊢ ⁅x, y⁆ = 1
Tactic:
rw [perm_fin_two x, perm_fin_two y]
State after:
x y : Equiv.Perm (Fin 2)
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1

State before:
x y : Equiv.Perm (Fin 2)
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
by_cases h : (x 0 = 1)
State after:
case pos
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1

case neg
x y : Equiv.Perm (Fin 2)
h : ¬x 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1

State before:
case pos
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
by_cases h₂ : (y 0 = 1)
State after:
case pos
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
h₂ : y 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1

case neg
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
h₂ : ¬y 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1

State before:
case pos
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
h₂ : y 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
rw [if_pos h, if_pos h₂, commutatorElement_self]
State after:
no goals

State before:
case neg
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
h₂ : ¬y 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
rw [if_neg h₂, commutatorElement_one_right]
State after:
no goals

State before:
case neg
x y : Equiv.Perm (Fin 2)
h : ¬x 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
rw [if_neg h, commutatorElement_one_left]
State after:
no goals