awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
succ 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 α)) (hl : ∀ g ∈ l, g.IsSwap) (hn : l.length = 2 * (n + 1)),
    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

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]

Premises used: Nat.succ_inj, Nat.mul_succ, List.length_cons, mul_assoc, Equiv.Perm.IsSwap.mul_mem_closure_three_cycles, OneMemClass.one_mem, List.prod_cons, rfl, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ {g : Perm α | g.IsThreeCycle} ⊆ (↑(alternatingGroup α) : Set (Perm α))

Tactic:
fun _ ↦ IsThreeCycle.mem_alternatingGroup

Premises used: Set.Mem, setOf, Set.Subset, Equiv.Perm.IsThreeCycle, Equiv.Perm.IsThreeCycle.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
rw :
  closure
      (_root_.Set.image (α := ↥(alternatingGroup α))
        (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle}) =
    map (alternatingGroup α).subtype ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle})
    ⊤

Tactic:
rw [← map_subtype_inj, MonoidHom.map_closure]

Premises used: Subgroup.map_subtype_inj, MonoidHom.map_closure
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ 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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
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}
⊢ closure
      (_root_.Set.image (α := ↥(alternatingGroup α))
        (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).IsThreeCycle}) =
    map (alternatingGroup α).subtype ⊤

Tactic:
aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
a : closure {g : Perm α | g.cycleType = {2, 2}} ≤ alternatingGroup α
a₁ : alternatingGroup α ≤ closure {g : Perm α | g.cycleType = {2, 2}}
⊢ closure {g : Perm α | g.cycleType = {2, 2}} = alternatingGroup α

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
a : {g : Perm α | g.cycleType = {2, 2}} ⊆ (↑(alternatingGroup α) : Set (Perm α))
⊢ closure {g : Perm α | g.cycleType = {2, 2}} ≤ alternatingGroup α

Tactic:
rw [Subgroup.closure_le]

Premises used: Subgroup.closure_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg : g.cycleType = {2, 2}
⊢ g ∈ (↑(alternatingGroup α) : Set (Perm α))

Tactic:
simp [mem_alternatingGroup, sign_of_cycleType, hg, ← Units.val_inj]

Premises used: Equiv.Perm.sign_of_cycleType, Equiv.Perm.mem_alternatingGroup, Units.val_inj
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
a : {σ : Perm α | σ.IsThreeCycle} ⊆ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
⊢ alternatingGroup α ≤ closure {g : Perm α | g.cycleType = {2, 2}}

Tactic:
rw [← Equiv.Perm.closure_three_cycles_eq_alternating, Subgroup.closure_le]

Premises used: Subgroup.closure_le, Equiv.Perm.closure_three_cycles_eq_alternating
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : Membership.mem (γ := Set (Perm α)) {σ : Perm α | σ.IsThreeCycle} g
a : ∀ (a : α) (ha : a ∈ g.support), g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))

Tactic:
obtain ⟨a, ha⟩ := hg3.isCycle.nonempty_support

Premises used: Equiv.Perm.IsCycle.nonempty_support, Equiv.Perm.IsThreeCycle.isCycle
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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.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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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 : α) : α)))
⊢ [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup

Tactic:
have h_nodup := hg3.nodup_iff_mem_support.mpr ha
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
⊢ 1 < g.supportᶜ.card

Tactic:
grind [Finset.card_compl, Nat.card_eq_fintype_card]

Premises used: Finset.card_compl, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
⊢ 1 < g.supportᶜ.card

Tactic:
have : 1 < g.supportᶜ.card := by grind [Finset.card_compl, Nat.card_eq_fintype_card]
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
a₁ :
  ∀ (b c : α) (hb : b ∈ g.supportᶜ) (hc : c ∈ g.supportᶜ) (hbc : b ≠ c),
    g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))

Tactic:
obtain ⟨b, c, hb, hc, hbc⟩ := Finset.one_lt_card_iff.mp this

Premises used: Finset.one_lt_card_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
⊢ g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)

Tactic:
simp [mul_assoc, ← hg3.eq_swap_mul_swap_iff_mem_support.mpr ha]

Premises used: Iff.mpr, mul_assoc, Equiv.Perm.IsThreeCycle.eq_swap_mul_swap_iff_mem_support
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
⊢ g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)

Tactic:
have H : g = (swap a (g a) * (swap b c)) * (swap b c * (swap (g a) (g (g a)))) := by
      simp [mul_assoc, ← hg3.eq_swap_mul_swap_iff_mem_support.mpr ha]
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H :
  g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
a₁ :
  swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) ∈
    (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))

Tactic:
rw [H]
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H :
  g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
a₁ :
  Membership.mem (γ := Subgroup (Perm α)) (closure {g : Perm α | g.cycleType = {2, 2}})
    (swap a ((g : (a : α) → α) a) * swap b c)
a₂ :
  Membership.mem (γ := Subgroup (Perm α)) (closure {g : Perm α | g.cycleType = {2, 2}})
    (HMul.hMul (β := Perm α) (swap b c)
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α))
⊢ swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) ∈
    (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))

Tactic:
apply mul_mem

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H :
  g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
a₁ : Membership.mem (γ := Set (Perm α)) {g : Perm α | g.cycleType = {2, 2}} (swap a ((g : (a : α) → α) a) * swap b c)
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {g : Perm α | g.cycleType = {2, 2}})
    (swap a ((g : (a : α) → α) a) * swap b c)

Tactic:
apply Subgroup.subset_closure

Premises used: Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H :
  g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
⊢ [a, (g : (a : α) → α) a, b, c].Nodup

Tactic:
grind [Finset.mem_compl]

Premises used: Finset.mem_compl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H :
  g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
⊢ Membership.mem (γ := Set (Perm α)) {g : Perm α | g.cycleType = {2, 2}} (swap a ((g : (a : α) → α) a) * swap b c)

Tactic:
exact cycleType_swap_mul_swap_of_nodup (by grind [Finset.mem_compl])

Premises used: Equiv.Perm.cycleType_swap_mul_swap_of_nodup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H :
  g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
a₁ :
  Membership.mem (γ := Set (Perm α)) {g : Perm α | g.cycleType = {2, 2}}
    (HMul.hMul (β := Perm α) (swap b c)
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α))
⊢ Membership.mem (γ := Subgroup (Perm α)) (closure {g : Perm α | g.cycleType = {2, 2}})
    (HMul.hMul (β := Perm α) (swap b c)
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α))

Tactic:
apply Subgroup.subset_closure

Premises used: Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H :
  g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
⊢ [b, c, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup

Tactic:
grind [Finset.mem_compl]

Premises used: Finset.mem_compl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
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
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H :
  g =
    swap a ((g : (a : α) → α) a) * swap b c *
      HMul.hMul (β := Perm α) (swap b c)
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
⊢ Membership.mem (γ := Set (Perm α)) {g : Perm α | g.cycleType = {2, 2}}
    (HMul.hMul (β := Perm α) (swap b c)
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α))

Tactic:
exact cycleType_swap_mul_swap_of_nodup (by grind [Finset.mem_compl])

Premises used: Equiv.Perm.cycleType_swap_mul_swap_of_nodup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : Membership.mem (γ := Set (Perm α)) {g : Perm α | g.cycleType = {2, 2}} g
⊢ g.cycleType = {2, 2}

Tactic:
rw [Set.mem_setOf_eq] at hg

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g.cycleType = {2, 2}
⊢ g ∈ (↑(alternatingGroup α) : Set (Perm α))

Tactic:
simp [sign_of_cycleType, hg, ← Units.val_inj]

Premises used: Equiv.Perm.sign_of_cycleType, Units.val_inj
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
rw :
  closure
      (_root_.Set.image (α := ↥(alternatingGroup α))
        (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) =
    map (alternatingGroup α).subtype ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α))
    (closure {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) ⊤

Tactic:
rw [← map_subtype_inj, MonoidHom.map_closure]

Premises used: Subgroup.map_subtype_inj, MonoidHom.map_closure
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ 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.cycleType = {2, 2}} (↑x : Perm α)})
    {g : Perm α | g.cycleType = {2, 2}}

Tactic:
have : (alternatingGroup α).subtype '' _ = {g : Perm α | g.cycleType = {2, 2}} :=
    Subtype.coe_image_of_subset cycleType_eq_two_two_subset_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
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.cycleType = {2, 2}} (↑x : Perm α)})
    {g : Perm α | g.cycleType = {2, 2}}
⊢ closure {g : Perm α | g.cycleType = {2, 2}} = alternatingGroup α

Tactic:
have := closure_cycleType_eq_two_two_eq_alternatingGroup h5
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
this_1 :
  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.cycleType = {2, 2}} (↑x : Perm α)})
    {g : Perm α | g.cycleType = {2, 2}}
this : closure {g : Perm α | g.cycleType = {2, 2}} = alternatingGroup α
⊢ closure
      (_root_.Set.image (α := ↥(alternatingGroup α))
        (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) =
    map (alternatingGroup α).subtype ⊤

Tactic:
aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
g : Perm (Fin 5)
h : 3 ∈ g.cycleType
obtain :
  ∀ (c g' : Perm (Fin 5)) (h : 3 ∈ (c * g').cycleType) (hd : c.Disjoint g'),
    c.IsCycle → ∀ (h3 : c.support.card = 3), (c * g' * (c * g')).IsThreeCycle
⊢ (g * g).IsThreeCycle

Tactic:
obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h

Premises used: Equiv.Perm.mem_cycleType_iff, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
simp : (c * (g' * (c * g'))).IsThreeCycle
⊢ (c * g' * (c * g')).IsThreeCycle

Tactic:
simp only [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
rw : (c * (g' * g' * c)).IsThreeCycle
⊢ (c * (g' * (c * g'))).IsThreeCycle

Tactic:
rw [hd.commute.eq, ← mul_assoc g']

Premises used: Equiv.Perm.Disjoint.commute, mul_assoc, Commute.eq