awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
inr : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (π * swap a b) : ℤˣ) (1 : ℤˣ)
inr₁ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) =
    1
⊢ π * swap a b ∈ alternatingGroup α
have inr₂ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) = 1
Tactic: rw [mem_alternatingGroup, map_mul, h, sign_swap ab, Int.units_mul_self]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
inr : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (π * swap a b) : ℤˣ) (1 : ℤˣ)
inr₁ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) =
    1
inr₂ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) = 1
⊢ π * swap a b ∈ alternatingGroup α
have inr₃ : HMul.hMul (α := ℤˣ) (-1) (-1) = 1
Tactic: rw [mem_alternatingGroup, map_mul, h, sign_swap ab, Int.units_mul_self]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
inr : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (π * swap a b) : ℤˣ) (1 : ℤˣ)
inr₁ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) =
    1
inr₂ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) = 1
inr₃ : HMul.hMul (α := ℤˣ) (-1) (-1) = 1
⊢ π * swap a b ∈ alternatingGroup α
have inr₄ : Eq (α := ℤˣ) 1 1
Tactic: rw [mem_alternatingGroup, map_mul, h, sign_swap ab, Int.units_mul_self]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (π * swap a b) ⋯ *
            Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1 *
          (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (π * swap a b) ⋯)⁻¹) :
      Perm α) =
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
have inr : π * swap a b * σ * (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (π * swap a b) sorry)⁻¹ : Perm α) =
  π * σ * π⁻¹
Tactic: simp only [← hπ, Subgroup.coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ (swap a b).Disjoint σ
have rw : a ∉ σ.support ∧ b ∉ σ.support
Tactic: rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left,
          Finset.disjoint_singleton_left]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ_1 : σ ∈ alternatingGroup α
hσ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc :
  IsConj (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1) : Perm α)
    (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ) : Perm α)
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) π : ℤˣ) (-1 : ℤˣ)
h2 : 2 ≤ σ.supportᶜ.card
a : α
ha : a ∈ σ.supportᶜ
b : α
hb : b ∈ σ.supportᶜ
ab : a ≠ b
⊢ π * swap a b * σ * (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (π * swap a b) ⋯)⁻¹ : Perm α) =
    π * σ * π⁻¹
have hd : (swap a b).Disjoint σ
Tactic: have hd : Disjoint (swap a b) σ := by
        rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left,
          Finset.disjoint_singleton_left]
        exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
σ τ : ↥(alternatingGroup α)
hσ : (↑σ : Perm α).IsThreeCycle
hτ : (↑τ : Perm α).IsThreeCycle
⊢ IsConj σ τ
have h5₁ : 5 ≤ card α
Tactic: simp only [Nat.card_eq_fintype_card] at h5
Cleared hypotheses: h5
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ closure {σ : Perm α | σ.IsThreeCycle} = alternatingGroup α
have refine : ∀ (σ : Perm α) (hσ : σ ∈ alternatingGroup α),
  Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) σ
Tactic: refine closure_eq_of_le _ (fun _ ↦ IsThreeCycle.mem_alternatingGroup) fun σ hσ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) σ
have mk : ∀ (l : List (Perm α)) (hl : ∀ g ∈ l, g.IsSwap) (hσ : l.prod ∈ alternatingGroup α)
  (x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ ∀ g ∈ l_1, g.IsSwap }),
  Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
Tactic: obtain ⟨l, rfl, hl⟩ := truncSwapFactors σ
Cleared hypotheses: σ, hσ
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hσ : l.prod ∈ alternatingGroup α
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ ∀ g ∈ l_1, g.IsSwap }
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
have mk : ∀ (n : ℕ) (hn : l.length = n + n),
  Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
Tactic: obtain ⟨n, hn⟩ := (prod_list_swap_mem_alternatingGroup_iff_even_length hl).1 hσ
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hind :
  ∀ (n : ℕ) (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hσ : l.prod ∈ alternatingGroup α
x : Trunc { l_1 : List (Perm α) // l_1.prod = l.prod ∧ ∀ g ∈ l_1, g.IsSwap }
n : ℕ
hn : l.length = n + n
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
have hn₁ : l.length = 2 * n
Tactic: rw [← two_mul] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) σ
have suffices : ∀ (n : ℕ) (l : List (Perm α)),
  (∀ g ∈ l, g.IsSwap) →
    l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
Tactic: suffices hind :
    ∀ (n : ℕ) (l : List (Perm α)) (_ : ∀ g, g ∈ l → IsSwap g) (_ : l.length = 2 * n),
      l.prod ∈ closure { σ : Perm α | IsThreeCycle σ } by
    obtain ⟨l, rfl, hl⟩ := truncSwapFactors σ
    obtain ⟨n, hn⟩ := (prod_list_swap_mem_alternatingGroup_iff_even_length hl).1 hσ
    rw [← two_mul] at hn
    exact hind n l hl hn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hn : l.length = 2 * (n + 1)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
have hn₁ : l.length = 2 * n + 2
Tactic: rw [Nat.mul_succ] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hn : l.length = 2 * n + 2
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
have succ : ∀ (a : Perm α) (l : List (Perm α)) (hl : ∀ g ∈ a :: l, g.IsSwap) (hn : (a :: l).length = 2 * n + 2),
  Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a :: l).prod
Tactic: obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn
Cleared hypotheses: l, hl, hn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
a : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: l, g.IsSwap
hn : (a :: l).length = 2 * n + 2
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a :: l).prod
have hn₁ : l.length = 2 * n + 1
Tactic: rw [List.length_cons, Nat.succ_inj] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
a : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: l, g.IsSwap
hn : l.length = 2 * n + 1
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a :: l).prod
have succ : ∀ (b : Perm α) (l : List (Perm α)) (hl : ∀ g ∈ a :: b :: l, g.IsSwap) (hn : (b :: l).length = 2 * n + 1),
  Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a :: b :: l).prod
Tactic: obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn
Cleared hypotheses: l, hl, hn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a :: b :: l).prod
have succ : Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a * b * l.prod)
Tactic: rw [List.prod_cons, List.prod_cons, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a * b * l.prod)
have succ : Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a * b)
Tactic: apply mul_mem
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih :
  ∀ (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
succ : Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a * b)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a * b * l.prod)
have succ₁ : Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
Tactic: apply mul_mem
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
⊢ ∀ (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
have zero : ∀ (l : List (Perm α)),
  (∀ g ∈ l, g.IsSwap) →
    l.length = HMul.hMul (α := ℕ) 2 0 →
      Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
Tactic: induction n with intro l hl hn
  | zero => simp [List.length_eq_zero_iff.1 hn, one_mem]
  | succ n ih =>
    rw [Nat.mul_succ] at hn
    obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn
    rw [List.length_cons, Nat.succ_inj] at hn
    obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn
    rw [List.prod_cons, List.prod_cons, ← mul_assoc]
    apply mul_mem <;> grind [IsSwap.mul_mem_closure_three_cycles]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
zero zero₁ :
  ∀ (l : List (Perm α)) (hl : ∀ g ∈ l, g.IsSwap) (hn : l.length = HMul.hMul (α := ℕ) 2 0),
    Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
⊢ ∀ (l : List (Perm α)),
    (∀ g ∈ l, g.IsSwap) →
      l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (l : List (Perm α)),
      (∀ g ∈ l, g.IsSwap) →
        l.length = 2 * n → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod)
  (l : List (Perm α)),
  (∀ g ∈ l, g.IsSwap) →
    l.length = 2 * (n + 1) → Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
Tactic: induction n with intro l hl hn
  | zero => simp [List.length_eq_zero_iff.1 hn, one_mem]
  | succ n ih =>
    rw [Nat.mul_succ] at hn
    obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn
    rw [List.length_cons, Nat.succ_inj] at hn
    obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn
    rw [List.prod_cons, List.prod_cons, ← mul_assoc]
    apply mul_mem <;> grind [IsSwap.mul_mem_closure_three_cycles]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle})
    ⊤
have rw : closure
    (_root_.Set.image (α := ↥(alternatingGroup α))
      (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle}) =
  map (alternatingGroup α).subtype ⊤
Tactic: rw [← map_subtype_inj, MonoidHom.map_closure]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ closure
      (_root_.Set.image (α := ↥(alternatingGroup α))
        (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle}) =
    map (alternatingGroup α).subtype ⊤
have this : Eq (α := Set (Perm α))
  (_root_.Set.image (α := ↥(alternatingGroup α)) (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
    {x : (↑(↑(alternatingGroup α) : Set (Perm α)) : Type u_1) |
      Membership.mem (γ := Set (Perm α)) {g : Perm α | g.IsThreeCycle} (↑x : Perm α)})
  {g : Perm α | g.IsThreeCycle}
Tactic: have : (alternatingGroup α).subtype '' _ = {g : Perm α | IsThreeCycle g} :=
    Subtype.coe_image_of_subset isThreeCycle_subset_alternatingGroup
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ closure {g : Perm α | g.cycleType = {2, 2}} = alternatingGroup α
have a : closure {g : Perm α | g.cycleType = {2, 2}} ≤ alternatingGroup α
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
a : closure {g : Perm α | g.cycleType = {2, 2}} ≤ alternatingGroup α
⊢ closure {g : Perm α | g.cycleType = {2, 2}} = alternatingGroup α
have a₁ : alternatingGroup α ≤ closure {g : Perm α | g.cycleType = {2, 2}}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ closure {g : Perm α | g.cycleType = {2, 2}} ≤ alternatingGroup α
have a : {g : Perm α | g.cycleType = {2, 2}} ⊆ (↑(alternatingGroup α) : Set (Perm α))
Tactic: rw [Subgroup.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ alternatingGroup α ≤ closure {g : Perm α | g.cycleType = {2, 2}}
have a : {σ : Perm α | σ.IsThreeCycle} ⊆ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
Tactic: rw [← Equiv.Perm.closure_three_cycles_eq_alternating, Subgroup.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : Membership.mem (γ := Set (Perm α)) {σ : Perm α | σ.IsThreeCycle} g
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
have a : ∀ (a : α) (ha : a ∈ g.support), g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
Tactic: obtain ⟨a, ha⟩ := hg3.isCycle.nonempty_support
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : Membership.mem (γ := Set (Perm α)) {σ : Perm α | σ.IsThreeCycle} g
a : α
ha : a ∈ g.support
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
have h_support : g.support =
  insert a
    (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
Tactic: have h_support := hg3.support_eq_iff_mem_support.mpr ha
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : Membership.mem (γ := Set (Perm α)) {σ : Perm α | σ.IsThreeCycle} g
a : α
ha : a ∈ g.support
h_support :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
have h_nodup : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
Tactic: have h_nodup := hg3.nodup_iff_mem_support.mpr ha
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : Membership.mem (γ := Set (Perm α)) {σ : Perm α | σ.IsThreeCycle} g
a : α
ha : a ∈ g.support
h_support :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
h_nodup : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
have this : 1 < g.supportᶜ.card
Tactic: have : 1 < g.supportᶜ.card := by grind [Finset.card_compl, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : Membership.mem (γ := Set (Perm α)) {σ : Perm α | σ.IsThreeCycle} g
a : α
ha : a ∈ g.support
h_support :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
h_nodup : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
this : 1 < g.supportᶜ.card
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
have a₁ : ∀ (b c : α) (hb : b ∈ g.supportᶜ) (hc : c ∈ g.supportᶜ) (hbc : b ≠ c),
  g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
Tactic: obtain ⟨b, c, hb, hc, hbc⟩ := Finset.one_lt_card_iff.mp this