case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
hτ : IsSwap τ
a b : α
ab : a ≠ b
⊢ swap a b * τ ∈ closure {σ | IsThreeCycle σ}
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : IsSwap σ
hτ : IsSwap τ
⊢ σ * τ ∈ closure {σ | IsThreeCycle σ}
obtain ⟨a, b, ab, rfl⟩ := hσ
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
hτ : IsSwap τ
a b : α
ab : a ≠ b
⊢ swap a b * τ ∈ closure {σ | IsThreeCycle σ}
obtain ⟨c, d, cd, rfl⟩ := hτ
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : a = c
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
by_cases ac : a = c
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
have h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d) := by
  simp [swap_comm c a, mul_assoc]
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ swap a b * swap a c * (swap c a * swap c d) ∈ closure {σ | IsThreeCycle σ}
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
rw [h']
no goals
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ swap a b * swap a c * (swap c a * swap c d) ∈ closure {σ | IsThreeCycle σ}
exact
  mul_mem (swap_mul_swap_same_mem_closure_three_cycles ab ac)
    (swap_mul_swap_same_mem_closure_three_cycles (Ne.symm ac) cd)
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
d : α
cd : a ≠ d
⊢ swap a b * swap a d ∈ closure {σ | IsThreeCycle σ}
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : a = c
⊢ swap a b * swap c d ∈ closure {σ | IsThreeCycle σ}
subst ac
no goals
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
d : α
cd : a ≠ d
⊢ swap a b * swap a d ∈ closure {σ | IsThreeCycle σ}
exact swap_mul_swap_same_mem_closure_three_cycles ab cd
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
⊢ swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
simp [swap_comm c a, mul_assoc]