awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate g.cycleType.card 2
have 0 : ∀ (h_1 : g.cycleType.card = 0) (h2 : g.cycleType = Multiset.replicate 0 2) (h : HMul.hMul (α := ℕ) 0 2 ≤ card (Fin 5))
  (h : LE.le (α := ℕ) 0 3) (ha : Even (α := ℕ) 0),
  (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 0 2
Tactic: interval_cases h_1 : Multiset.card g.cycleType
Cleared hypotheses: h2, h_1, h, 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
0 :
  ∀ (h_1 : g.cycleType.card = 0) (h2 : g.cycleType = Multiset.replicate 0 2) (h : HMul.hMul (α := ℕ) 0 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 0 3) (ha : Even (α := ℕ) 0),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 0 2
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate g.cycleType.card 2
have 1 : ∀ (h_1 : g.cycleType.card = 1) (h2 : g.cycleType = Multiset.replicate 1 2) (h : HMul.hMul (α := ℕ) 1 2 ≤ card (Fin 5))
  (h : LE.le (α := ℕ) 1 3) (ha : Even (α := ℕ) 1),
  (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 1 2
Tactic: interval_cases h_1 : Multiset.card g.cycleType
Cleared hypotheses: h2, h_1, h, 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
0 :
  ∀ (h_1 : g.cycleType.card = 0) (h2 : g.cycleType = Multiset.replicate 0 2) (h : HMul.hMul (α := ℕ) 0 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 0 3) (ha : Even (α := ℕ) 0),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 0 2
1 :
  ∀ (h_1 : g.cycleType.card = 1) (h2 : g.cycleType = Multiset.replicate 1 2) (h : HMul.hMul (α := ℕ) 1 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 1 3) (ha : Even (α := ℕ) 1),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 1 2
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate g.cycleType.card 2
have 2 : ∀ (h_1 : g.cycleType.card = 2) (h2 : g.cycleType = Multiset.replicate 2 2) (h : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5))
  (h : LE.le (α := ℕ) 2 3) (ha : Even (α := ℕ) 2),
  (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 2 2
Tactic: interval_cases h_1 : Multiset.card g.cycleType
Cleared hypotheses: h2, h_1, h, 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
0 :
  ∀ (h_1 : g.cycleType.card = 0) (h2 : g.cycleType = Multiset.replicate 0 2) (h : HMul.hMul (α := ℕ) 0 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 0 3) (ha : Even (α := ℕ) 0),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 0 2
1 :
  ∀ (h_1 : g.cycleType.card = 1) (h2 : g.cycleType = Multiset.replicate 1 2) (h : HMul.hMul (α := ℕ) 1 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 1 3) (ha : Even (α := ℕ) 1),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 1 2
2 :
  ∀ (h_1 : g.cycleType.card = 2) (h2 : g.cycleType = Multiset.replicate 2 2) (h : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5))
    (h : LE.le (α := ℕ) 2 3) (ha : Even (α := ℕ) 2),
    (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 2 2
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate g.cycleType.card 2
have 3 : ∀ (h_1 : g.cycleType.card = 3) (h2 : g.cycleType = Multiset.replicate 3 2) (h : HMul.hMul (α := ℕ) 3 2 ≤ card (Fin 5))
  (h : LE.le (α := ℕ) 3 3) (ha : Even (α := ℕ) 3),
  (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 3 2
Tactic: interval_cases h_1 : Multiset.card g.cycleType
Cleared hypotheses: h2, h_1, h, ha
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 2 2
have h04 : Ne (α := Fin 5) 0 4
Tactic: have h04 : (0 : Fin 5) ≠ 4 := by decide
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 2 2
have h13 : Ne (α := Fin 5) 1 3
Tactic: have h13 : (1 : Fin 5) ≠ 3 := by decide
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
h13 : Ne (α := Fin 5) 1 3
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 2 2
have 2 : HAdd.hAdd (α := Multiset ℕ) {2} {2} = Multiset.replicate 2 2
Tactic: rw [Disjoint.cycleType_mul, (isCycle_swap h04).cycleType, (isCycle_swap h13).cycleType,
      card_support_swap h04, card_support_swap h13]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
h13 : Ne (α := Fin 5) 1 3
2 : HAdd.hAdd (α := Multiset ℕ) {2} {2} = Multiset.replicate 2 2
⊢ (HMul.hMul (α := Perm (Fin 5)) (swap 0 4) (swap 1 3)).cycleType = Multiset.replicate 2 2
have 2₁ : Perm.Disjoint (α := Fin 5) (swap 0 4) (swap 1 3)
Tactic: rw [Disjoint.cycleType_mul, (isCycle_swap h04).cycleType, (isCycle_swap h13).cycleType,
      card_support_swap h04, card_support_swap h13]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
h2 : g.cycleType = Multiset.replicate 2 2
h_2 : HMul.hMul (α := ℕ) 2 2 ≤ card (Fin 5)
h : LE.le (α := ℕ) 2 3
ha : Even (α := ℕ) 2
h04 : Ne (α := Fin 5) 0 4
h13 : Ne (α := Fin 5) 1 3
⊢ Perm.Disjoint (α := Fin 5) (swap 0 4) (swap 1 3)
have 2 : _root_.Disjoint (α := Finset (Fin 5)) {0, 4} {1, 3}
Tactic: rw [disjoint_iff_disjoint_support, support_swap h04, support_swap h13]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α)) ⊥
have rw : LE.le.{u_1} (α := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α)) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg = 1
have simp : ∀ (x : α), x ∉ g.support
Tactic: simp only [← Subtype.coe_inj, Subgroup.coe_one, ← support_eq_empty_iff,
    Finset.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
⊢ False
have hab : (g : (a : α) → α) a ≠ a
Tactic: have hab : g a ≠ a := by rw [← mem_support]; exact ha
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
⊢ 2 ≤ Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ
have rw : Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α))) + 2 ≤ card α
Tactic: rw [← Nat.add_le_add_iff_left, Finset.card_add_card_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
⊢ Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α))) + 2 ≤ card α
have rw : Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α))) + 2 ≤ Nat.card α
Tactic: rw [← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
⊢ False
have this : 2 ≤ Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ
Tactic: have : 2 ≤ (({a, g a} : Finset α)ᶜ).card := by
    rw [← Nat.add_le_add_iff_left, Finset.card_add_card_compl]
    rw [← Nat.card_eq_fintype_card]
    rw [Finset.card_pair hab.symm]
    exact hα4
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
this : 2 ≤ Finset.card (α := α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ
⊢ False
have this₁ : ∃ (a_1 : α) (b : α),
  Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ a_1 ∧
    Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ b ∧ a_1 ≠ b
Tactic: rw [← Nat.lt_iff_add_one_le, Finset.one_lt_card_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
this :
  ∃ (a_1 : α) (b : α),
    Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ a_1 ∧
      Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ b ∧ a_1 ≠ b
⊢ False
have obtain : ∀ (c d : α) (hc : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ c)
  (hd : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ d) (hcd : c ≠ d),
  False
Tactic: obtain ⟨c, d, hc, hd, hcd⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hc : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ c
hd : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ d
hcd : c ≠ d
⊢ False
have hc₁ : c ≠ a ∧ c ≠ (g : (a : α) → α) a
Tactic: simp only [Finset.compl_insert, Finset.mem_erase, ← ne_eq, Finset.mem_compl,
    Finset.mem_singleton] at hc hd
Cleared hypotheses: hc, hd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hc : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ c
hd : Membership.mem (γ := Finset α) (insert a (singleton (α := α) ((g : (a : α) → α) a : α)))ᶜ d
hcd : c ≠ d
hc₁ : c ≠ a ∧ c ≠ (g : (a : α) → α) a
⊢ False
have hd₁ : d ≠ a ∧ d ≠ (g : (a : α) → α) a
Tactic: simp only [Finset.compl_insert, Finset.mem_erase, ← ne_eq, Finset.mem_compl,
    Finset.mem_singleton] at hc hd
Cleared hypotheses: hc, hd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
⊢ k • a = a
have simp : ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α)
    (((swap ((g : (a : α) → α) a) c : Perm α) : (a : α) → α) a : α) =
  a
Tactic: simp only [Perm.smul_def, coe_mul, Function.comp_apply, k]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
⊢ ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α)
      (((swap ((g : (a : α) → α) a) c : Perm α) : (a : α) → α) a : α) =
    a
have rw : ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α) a = a
Tactic: rw [swap_apply_of_ne_of_ne (x := a) hab.symm hc.1.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
⊢ ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α) a = a
have rw : a = a
Tactic: rw [swap_apply_of_ne_of_ne hab.symm hd.1.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
⊢ False
have hka : k • a = a
Tactic: have hka : k • a = a := by
    simp only [Perm.smul_def, coe_mul, Function.comp_apply, k]
    rw [swap_apply_of_ne_of_ne (x := a) hab.symm hc.1.symm]
    rw [swap_apply_of_ne_of_ne hab.symm hd.1.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
⊢ HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c
have simp : ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α) c = c
Tactic: simp only [Perm.smul_def, coe_mul, Function.comp_apply, swap_apply_left, k]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
⊢ ((swap ((g : (a : α) → α) a) d : Perm α) : (a : α) → α) c = c
have rw : c = c
Tactic: rw [swap_apply_of_ne_of_ne hc.2 hcd]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
⊢ False
have hkga : HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c
Tactic: have hkga : k • (g a) = c := by
    simp only [Perm.smul_def, coe_mul, Function.comp_apply, swap_apply_left, k]
    rw [swap_apply_of_ne_of_ne hc.2 hcd]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
hkga : HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c
this : k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c
⊢ False
have apply : k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a = c
Tactic: apply this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
hkga : HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c
⊢ False
have suffices : k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c
Tactic: suffices k • (⟨g, hg⟩ : alternatingGroup α) • a ≠ c by
    apply this; simp [← hkga]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
hkga : HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c
this :
  k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
⊢ k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c
have rw : Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c
Tactic: rw [this, hka]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (center ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
a : α
ha : a ∈ g.support
hab : (g : (a : α) → α) a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ (g : (a : α) → α) a
hd : d ≠ a ∧ d ≠ (g : (a : α) → α) a
k : Perm α :=
  HMul.hMul (α := Perm α) (β := Perm α) (swap ((g : (a : α) → α) a) d : Perm α) (swap ((g : (a : α) → α) a) c : Perm α)
hka : k • a = a
hkga : HSMul.hSMul (β := α) k ((g : (a : α) → α) a : α) = c
⊢ k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a ≠ c
have suffices : k • Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • a =
  Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
Tactic: suffices k • (⟨g, hg⟩ : alternatingGroup α) • a = (⟨g, hg⟩ : alternatingGroup α) • k • a by
    rw [this, hka]; exact hc.right.symm