awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 : ℤˣ)
⊢ σ.support.card + 2 ≤ card α

Tactic:
exact hσ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 : ℤˣ)
⊢ 2 ≤ σ.supportᶜ.card

Tactic:
have h2 : 2 ≤ σ.supportᶜ.card := by
      rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]
      exact hσ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
inr :
  ∀ (a : α) (ha : a ∈ σ.supportᶜ) (b : α) (hb : b ∈ σ.supportᶜ) (ab : a ≠ b),
    IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)

Tactic:
obtain ⟨a, ha, b, hb, ab⟩ := Finset.one_lt_card.1 h2

Premises used: Iff.mp, Finset.one_lt_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)

Tactic:
isConj_iff.2 ⟨⟨π * swap a b, ?_⟩, Subtype.val_injective ?_⟩

Premises used: Iff.mpr, isConj_iff, HMul.hMul, Subtype.val_injective, Equiv.swap, Subtype.mk, Exists.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 : π * swap a b ∈ alternatingGroup α
inr₁ :
  (↑(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 α)
⊢ IsConj (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) σ hσ_1)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) τ hτ)

Tactic:
refine isConj_iff.2 ⟨⟨π * swap a b, ?_⟩, Subtype.val_injective ?_⟩

Premises used: Iff.mpr, isConj_iff, Subtype.val_injective, Exists.intro
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
inr₄ inr₅ : Eq (α := ℤˣ) 1 1
⊢ π * swap a b ∈ alternatingGroup α

Tactic:
rw [mem_alternatingGroup, map_mul, h, sign_swap ab, Int.units_mul_self]

Premises used: Equiv.Perm.mem_alternatingGroup, map_mul, Equiv.Perm.sign_swap, Int.units_mul_self
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 :
  π * swap a b * σ * (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (π * swap a b) ⋯)⁻¹ : Perm α) =
    π * σ * π⁻¹
⊢ (↑(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 α)

Tactic:
simp only [← hπ, Subgroup.coe_mul]

Premises used: Subgroup.coe_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
rw : a ∉ σ.support ∧ b ∉ σ.support
⊢ (swap a b).Disjoint σ

Tactic:
rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left,
          Finset.disjoint_singleton_left]

Premises used: Finset.disjoint_insert_left, Equiv.Perm.support_swap, Finset.disjoint_singleton_left, Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
⊢ a ∉ σ.support ∧ b ∉ σ.support

Tactic:
⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩

Premises used: Finset.mem_compl, And.intro, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
⊢ a ∉ σ.support ∧ b ∉ σ.support

Tactic:
exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 σ

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⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
hd : (swap a b).Disjoint σ
⊢ π * swap a b * σ * (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (π * swap a b) ⋯)⁻¹ : Perm α) =
    π * σ * π⁻¹

Tactic:
simp [mul_assoc, hd.commute.eq]

Premises used: Equiv.Perm.Disjoint.commute, mul_assoc, Commute.eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
σ τ : ↥(alternatingGroup α)
hσ : (↑σ : Perm α).IsThreeCycle
hτ : (↑τ : Perm α).IsThreeCycle
⊢ 5 ≤ card α

Tactic:
simp only [Nat.card_eq_fintype_card] at h5

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : ↥(alternatingGroup α)
hσ : (↑σ : Perm α).IsThreeCycle
hτ : (↑τ : Perm α).IsThreeCycle
h5 : 5 ≤ card α
rwa rwa₁ rwa₂ rwa₃ : HAdd.hAdd (α := ℕ) 3 2 ≤ card α
⊢ (↑σ : Perm α).support.card + 2 ≤ card α

Tactic:
rwa [hσ.card_support]

Premises used: Equiv.Perm.IsThreeCycle.card_support
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : ↥(alternatingGroup α)
hσ : (↑σ : Perm α).IsThreeCycle
hτ : (↑τ : Perm α).IsThreeCycle
h5 : 5 ≤ card α
⊢ IsConj σ τ

Tactic:
exact alternatingGroup.isConj_of (isConj_iff_cycleType_eq.2 (hσ.trans hτ.symm))
    (by rwa [hσ.card_support])

Premises used: Iff.mpr, alternatingGroup.isConj_of, Equiv.Perm.isConj_iff_cycleType_eq, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ closure {σ : Perm α | σ.IsThreeCycle} = alternatingGroup α

Tactic:
closure_eq_of_le _ (fun _ ↦ IsThreeCycle.mem_alternatingGroup) fun σ hσ ↦ ?_

Premises used: Subgroup.closure_eq_of_le, Equiv.Perm.IsThreeCycle.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
refine :
  ∀ (σ : Perm α) (hσ : σ ∈ alternatingGroup α),
    Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) σ
⊢ closure {σ : Perm α | σ.IsThreeCycle} = alternatingGroup α

Tactic:
refine closure_eq_of_le _ (fun _ ↦ IsThreeCycle.mem_alternatingGroup) fun σ hσ ↦ ?_

Premises used: Subgroup.closure_eq_of_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
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
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) σ

Tactic:
obtain ⟨l, rfl, hl⟩ := truncSwapFactors σ

Premises used: Equiv.Perm.truncSwapFactors, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 }
mk :
  ∀ (n : ℕ) (hn : l.length = n + n),
    Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod

Tactic:
obtain ⟨n, hn⟩ := (prod_list_swap_mem_alternatingGroup_iff_even_length hl).1 hσ

Premises used: Equiv.Perm.prod_list_swap_mem_alternatingGroup_iff_even_length, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
⊢ l.length = 2 * n

Tactic:
rw [← two_mul] at hn

Premises used: two_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 = 2 * n
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod

Tactic:
hind n l hl hn
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 = 2 * n
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod

Tactic:
exact hind n l hl hn
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
suffices :
  ∀ (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}) σ

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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hn : l.length = HMul.hMul (α := ℕ) 2 0
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod

Tactic:
simp [List.length_eq_zero_iff.1 hn, one_mem]

Premises used: Iff.mp, OneMemClass.one_mem, List.length_eq_zero_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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)
⊢ l.length = 2 * n + 2

Tactic:
rw [Nat.mul_succ] at hn

Premises used: Nat.mul_succ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
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
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod

Tactic:
obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn

Premises used: List.exists_of_length_succ, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
⊢ l.length = 2 * n + 1

Tactic:
rw [List.length_cons, Nat.succ_inj] at hn

Premises used: Nat.succ_inj, List.length_cons
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
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
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a :: l).prod

Tactic:
obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn

Premises used: List.exists_of_length_succ, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 * l.prod)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a :: b :: l).prod

Tactic:
rw [List.prod_cons, List.prod_cons, ← mul_assoc]

Premises used: mul_assoc, List.prod_cons
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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)
succ₁ : Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) l.prod
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {σ : Perm α | σ.IsThreeCycle}) (a * b * l.prod)

Tactic:
apply mul_mem

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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)

Tactic:
grind [IsSwap.mul_mem_closure_three_cycles]

Premises used: Equiv.Perm.IsSwap.mul_mem_closure_three_cycles
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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}) l.prod

Tactic:
grind [IsSwap.mul_mem_closure_three_cycles]

Premises used: Equiv.Perm.IsSwap.mul_mem_closure_three_cycles