awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
have 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 α)
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]
-- 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
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 α)
⊢ g ∈ (↑(closure {g : Perm α | g.cycleType = {2, 2}}) : Set (Perm α))
have 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 α))
Tactic: rw [H]
-- 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
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 α)
⊢ 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 α))
have a₁ : Membership.mem (γ := Subgroup (Perm α)) (closure {g : Perm α | g.cycleType = {2, 2}})
  (swap a ((g : (a : α) → α) a) * swap b c)
Tactic: apply mul_mem
-- 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
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)
⊢ 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 α))
have 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 α))
Tactic: apply mul_mem
-- 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
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 (γ := Subgroup (Perm α)) (closure {g : Perm α | g.cycleType = {2, 2}})
    (swap a ((g : (a : α) → α) a) * swap b c)
have a₁ : Membership.mem (γ := Set (Perm α)) {g : Perm α | g.cycleType = {2, 2}} (swap a ((g : (a : α) → α) a) * swap b c)
Tactic: apply Subgroup.subset_closure
-- 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
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 (γ := 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 α))
have 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 α))
Tactic: apply Subgroup.subset_closure
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : Membership.mem (γ := Set (Perm α)) {g : Perm α | g.cycleType = {2, 2}} g
⊢ g ∈ (↑(alternatingGroup α) : Set (Perm α))
have hg₁ : g.cycleType = {2, 2}
Tactic: rw [Set.mem_setOf_eq] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α))
    (closure {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) ⊤
have rw : closure
    (_root_.Set.image (α := ↥(alternatingGroup α))
      (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) =
  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 α
h5 : 5 ≤ Nat.card α
⊢ closure
      (_root_.Set.image (α := ↥(alternatingGroup α))
        (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) =
    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.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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
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
      (_root_.Set.image (α := ↥(alternatingGroup α))
        (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) =
    map (alternatingGroup α).subtype ⊤
have this₁ : closure {g : Perm α | g.cycleType = {2, 2}} = alternatingGroup α
Tactic: have := closure_cycleType_eq_two_two_eq_alternatingGroup h5
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
g : Perm (Fin 5)
h : 3 ∈ g.cycleType
⊢ (g * g).IsThreeCycle
have 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
Tactic: obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
⊢ (c * g' * (c * g')).IsThreeCycle
have simp : (c * (g' * (c * g'))).IsThreeCycle
Tactic: simp only [mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
⊢ (c * (g' * (c * g'))).IsThreeCycle
have rw : (c * (g' * g' * c)).IsThreeCycle
Tactic: rw [hd.commute.eq, ← mul_assoc g']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
hg' : orderOf g' ∣ 2
⊢ (c * (g' * g' * c)).IsThreeCycle
have rw : (c * c).IsThreeCycle
Tactic: rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
⊢ (c * (g' * g' * c)).IsThreeCycle
have suffices : orderOf g' ∣ 2
Tactic: suffices hg' : orderOf g' ∣ 2 by
    rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
    exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
⊢ orderOf g' ∣ 2
have rw : ∀ b ∈ g'.cycleType, b ∣ 2
Tactic: rw [← lcm_cycleType, Multiset.lcm_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ n ∣ 2
have rw : g'.support.card ≤ 2
Tactic: rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left : c.IsCycle
h3 : c.support.card = 3
n : ℕ
hn : n ∈ g'.cycleType
⊢ g'.support.card ≤ 2
have bc : c.support.card + g'.support.card ≤ c.support.card + 2
Tactic: apply le_of_add_le_add_left
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
⊢ alternatingGroup α = ⊥
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
hα' : Nat.card α = 2
⊢ alternatingGroup α = ⊥
have rw : Nat.card.{u_1} ↥(alternatingGroup α) = 1
Tactic: rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
hα' : Nat.card α = 2
rw : Nat.card.{u_1} ↥(alternatingGroup α) = 1
⊢ alternatingGroup α = ⊥
have rw₁ : 2 * Nat.card.{u_1} ↥(alternatingGroup α) = HMul.hMul (α := ℕ) 2 1
Tactic: rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
hα' : Nat.card α = 2
rw : Nat.card.{u_1} ↥(alternatingGroup α) = 1
rw₁ : 2 * Nat.card.{u_1} ↥(alternatingGroup α) = HMul.hMul (α := ℕ) 2 1
⊢ alternatingGroup α = ⊥
have rw₂ : Nat.card.{u_1} (Perm α) = HMul.hMul (α := ℕ) 2 1
Tactic: rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
hα' : Nat.card α = 2
rw : Nat.card.{u_1} ↥(alternatingGroup α) = 1
rw₁ : 2 * Nat.card.{u_1} ↥(alternatingGroup α) = HMul.hMul (α := ℕ) 2 1
rw₂ : Nat.card.{u_1} (Perm α) = HMul.hMul (α := ℕ) 2 1
rw₃ : Nat.card.{u_1} (Perm α) = 2
⊢ alternatingGroup α = ⊥
have rw₄ : (Nat.card α).factorial = 2
Tactic: rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
hα' : Nat.card α = 2
rw : Nat.card.{u_1} ↥(alternatingGroup α) = 1
rw₁ : 2 * Nat.card.{u_1} ↥(alternatingGroup α) = HMul.hMul (α := ℕ) 2 1
rw₂ : Nat.card.{u_1} (Perm α) = HMul.hMul (α := ℕ) 2 1
rw₃ : Nat.card.{u_1} (Perm α) = 2
rw₄ : (Nat.card α).factorial = 2
⊢ alternatingGroup α = ⊥
have rw₅ : Nat.factorial 2 = 2
Tactic: rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
hα' : Nat.card α = 2
rw : Nat.card.{u_1} ↥(alternatingGroup α) = 1
rw₁ : 2 * Nat.card.{u_1} ↥(alternatingGroup α) = HMul.hMul (α := ℕ) 2 1
rw₂ : Nat.card.{u_1} (Perm α) = HMul.hMul (α := ℕ) 2 1
rw₃ : Nat.card.{u_1} (Perm α) = 2
rw₄ : (Nat.card α).factorial = 2
rw₅ : Nat.factorial 2 = 2
⊢ alternatingGroup α = ⊥
have rw₆ : Eq (α := ℕ) 2 2
Tactic: rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
⊢ alternatingGroup α = ⊥
have suffices : Nat.card α = 2
Tactic: suffices hα' : Nat.card α = 2 by
    rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h2 : Nat.card α ≤ 2
h : Nontrivial α
⊢ Nat.card α = 2
have refine : 2 ≤ Nat.card α
Tactic: refine h2.antisymm ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
⊢ Nontrivial α
have rw : 1 < Nat.card α
Tactic: rw [← Fintype.one_lt_card_iff_nontrivial, ← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
⊢ Nontrivial.{u_1} ↥(alternatingGroup α)
have this : Nontrivial α
Tactic: have : Nontrivial α := by
    rw [← Fintype.one_lt_card_iff_nontrivial, ← Nat.card_eq_fintype_card]
    refine lt_of_lt_of_le (by decide) h3
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ Nontrivial.{u_1} ↥(alternatingGroup α)
have rw : 1 < Nat.card.{u_1} ↥(alternatingGroup α)
Tactic: rw [← Fintype.one_lt_card_iff_nontrivial, ← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ 1 < Nat.card.{u_1} ↥(alternatingGroup α)
have refine : HMul.hMul (α := ℕ) 2 1 < 2 * Nat.card.{u_1} ↥(alternatingGroup α)
Tactic: refine lt_of_mul_lt_mul_left ?_ (le_of_lt Nat.prime_two.pos)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ HMul.hMul (α := ℕ) 2 1 < 2 * Nat.card.{u_1} ↥(alternatingGroup α)
have rw : (HMul.hMul (α := ℕ) 2 1).succ ≤ (Nat.card α).factorial
Tactic: rw [two_mul_nat_card_alternatingGroup, Nat.card_perm, ← Nat.succ_le_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : ∀ n ∈ g.cycleType, n = 2
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
have h : g.support.card ≤ card (Fin 5)
Tactic: have h := g.support.card_le_univ
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : ∀ n ∈ g.cycleType, n = 2
h : g.support.card ≤ card (Fin 5)
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
have h2₁ : g.cycleType = Multiset.replicate g.cycleType.card 2
Tactic: rw [← Multiset.eq_replicate_card] at h2
Cleared hypotheses: h2, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.support.card ≤ card (Fin 5)
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
have h₁ : g.cycleType.card * 2 ≤ card (Fin 5)
Tactic: rw [← sum_cycleType, h2, Multiset.sum_replicate, smul_eq_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h : g.cycleType.card * 2 ≤ card (Fin 5)
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
have h₁ : g.cycleType.card ≤ 3
Tactic: have h : Multiset.card g.cycleType ≤ 3 :=
    le_of_mul_le_mul_right (le_trans h (by norm_num only [card_fin])) (by simp)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
g : Perm (Fin 5)
ha : Membership.mem (γ := Subgroup (Perm (Fin 5))) (alternatingGroup (Fin 5)) g
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
have ha₁ : HPow.hPow (α := ℤˣ) (-1)
    (Multiset.sum (Multiset.replicate g.cycleType.card 2) +
      Multiset.card (α := ℕ) (Multiset.replicate g.cycleType.card 2)) =
  1
Tactic: rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha
Cleared hypotheses: ha, h1, h2, h_1, h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
g : Perm (Fin 5)
ha :
  HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate g.cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate g.cycleType.card 2)) =
    1
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
have ha₁ : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.card * 2 + g.cycleType.card) = 1
Tactic: simp at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.card * 2 + g.cycleType.card) = 1
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
have rw : ∀ (ha : Even g.cycleType.card), IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
Tactic: rw [pow_add, pow_mul, Int.units_pow_two, one_mul, neg_one_pow_eq_one_iff_even] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.card * 2 + g.cycleType.card) = 1
rw : ∀ (ha : Even g.cycleType.card), IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
have rw₁ : ∀ (ha : HPow.hPow (α := ℤˣ) (-1) g.cycleType.card = 1), Ne (α := ℤˣ) (-1) 1
Tactic: rw [pow_add, pow_mul, Int.units_pow_two, one_mul, neg_one_pow_eq_one_iff_even] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
h_1 : g.cycleType.card * 2 ≤ card (Fin 5)
h : g.cycleType.card ≤ 3
ha : Even g.cycleType.card
⊢ IsConj (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)) g
have rw : (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate g.cycleType.card 2
Tactic: rw [isConj_iff_cycleType_eq, h2]