α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
⊢ σ ∈ closure {σ | IsThreeCycle σ}

case hind
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ σ ∈ closure {σ | IsThreeCycle σ}
suffices hind :
  ∀ (n : ℕ) (l : List (Perm α)) (_ : ∀ g, g ∈ l → IsSwap g) (_ : l.length = 2 * n),
    l.prod ∈ closure { σ : Perm α | IsThreeCycle σ }
case hind
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
⊢ ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
case hind
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
intro n
case hind.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * Nat.zero
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}

case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * Nat.succ n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
case hind
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
⊢ ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
induction' n with n ih <;> intro l hl hn
case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * n + 2
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * Nat.succ n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
rw [Nat.mul_succ] at hn
case hind.succ.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: l → IsSwap g
hn : List.length (a :: l) = 2 * n + 2
⊢ List.prod (a :: l) ∈ closure {σ | IsThreeCycle σ}
case hind.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * n + 2
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn
case hind.succ.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: l → IsSwap g
hn : List.length l = 2 * n + 1
⊢ List.prod (a :: l) ∈ closure {σ | IsThreeCycle σ}
case hind.succ.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: l → IsSwap g
hn : List.length (a :: l) = 2 * n + 2
⊢ List.prod (a :: l) ∈ closure {σ | IsThreeCycle σ}
rw [List.length_cons, Nat.succ_inj'] at hn
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length (b :: l) = 2 * n + 1
⊢ List.prod (a :: b :: l) ∈ closure {σ | IsThreeCycle σ}
case hind.succ.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: l → IsSwap g
hn : List.length l = 2 * n + 1
⊢ List.prod (a :: l) ∈ closure {σ | IsThreeCycle σ}
obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length (b :: l) = 2 * n + 1
⊢ a * b * List.prod l ∈ closure {σ | IsThreeCycle σ}
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length (b :: l) = 2 * n + 1
⊢ List.prod (a :: b :: l) ∈ closure {σ | IsThreeCycle σ}
rw [List.prod_cons, List.prod_cons, ← mul_assoc]
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length l = 2 * n
⊢ a * b * List.prod l ∈ closure {σ | IsThreeCycle σ}
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length (b :: l) = 2 * n + 1
⊢ a * b * List.prod l ∈ closure {σ | IsThreeCycle σ}
rw [List.length_cons, Nat.succ_inj'] at hn
no goals
case hind.succ.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
a b : Perm α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ a :: b :: l → IsSwap g
hn : List.length l = 2 * n
⊢ a * b * List.prod l ∈ closure {σ | IsThreeCycle σ}
exact
  mul_mem
    (IsSwap.mul_mem_closure_three_cycles (hl a (List.mem_cons_self a _))
      (hl b (List.mem_cons_of_mem a (l.mem_cons_self b))))
    (ih _ (fun g hg => hl g (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ hg))) hn)
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
⊢ σ ∈ closure {σ | IsThreeCycle σ}
obtain ⟨l, rfl, hl⟩ := truncSwapFactors σ
case mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
n : ℕ
hn : List.length l = n + n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
case mk.mk.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
obtain ⟨n, hn⟩ := (prod_list_swap_mem_alternatingGroup_iff_even_length hl).1 hσ
case mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
n : ℕ
hn : List.length l = 2 * n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
case mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
n : ℕ
hn : List.length l = n + n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
rw [← two_mul] at hn
no goals
case mk.mk.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ (g : Perm α), g ∈ l → IsSwap g) → List.length l = 2 * n → List.prod l ∈ closure {σ | IsThreeCycle σ}
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hσ : List.prod l ∈ alternatingGroup α
x✝ : Trunc { l_1 // List.prod l_1 = List.prod l ∧ ∀ (g : Perm α), g ∈ l_1 → IsSwap g }
n : ℕ
hn : List.length l = 2 * n
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
exact hind n l hl hn
no goals
case hind.zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
hn : List.length l = 2 * Nat.zero
⊢ List.prod l ∈ closure {σ | IsThreeCycle σ}
simp [List.length_eq_zero.1 hn, one_mem]