awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
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 =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
have rw : ∀
  (hg' :
    ∀ (g_1 : ↥(alternatingGroup α)),
      g_1 * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg =
        Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg * g_1)
  (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),
  let k :=
    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 =
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
Tactic: rw [Subgroup.mem_center_iff] at hg'
Cleared hypotheses: hg', a, ha, hab, c, d, hcd, hc, hd, k, hka, 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' :
  ∀ (g_1 : ↥(alternatingGroup α)),
    g_1 * Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg =
      Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg * g_1
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 =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg • k • a
have suffices : k ∈ alternatingGroup α
Tactic: suffices k ∈ alternatingGroup α by
    simp only [← Subgroup.mk_smul k this, ← mul_smul, hg']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ IsMulCommutative.{u_1} ↥(alternatingGroup α) ↔ Nat.card α ≤ 3
have refine : ∀ (H : IsMulCommutative.{u_1} ↥(alternatingGroup α)), Nat.card α ≤ 3
Tactic: refine ⟨fun H ↦ ?_, fun h ↦ (isCyclic_of_card_le_three h).isMulCommutative⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
⊢ Nat.card α ≤ 3
have rw : ¬3 < Nat.card α
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
h : 3 < Nat.card α
this : Subsingleton.{u_1 + 1} ↥(alternatingGroup α)
⊢ False
have this₁ : ¬Nontrivial.{u_1} ↥(alternatingGroup α)
Tactic: rw [← not_nontrivial_iff_subsingleton] 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 : IsMulCommutative.{u_1} ↥(alternatingGroup α)
h : 3 < Nat.card α
this : ¬Nontrivial.{u_1} ↥(alternatingGroup α)
⊢ False
have apply : Nontrivial.{u_1} ↥(alternatingGroup α)
Tactic: apply this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
H : IsMulCommutative.{u_1} ↥(alternatingGroup α)
h : 3 < Nat.card α
⊢ False
have suffices : Subsingleton.{u_1 + 1} ↥(alternatingGroup α)
Tactic: suffices Subsingleton (alternatingGroup α) by
    rw [← not_nontrivial_iff_subsingleton] at this
    apply this
    exact nontrivial_of_three_le_card h.le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h : IsCyclic.{u_1} ↥(alternatingGroup α)
⊢ Nat.card α ≤ 3
have rw : IsMulCommutative.{u_1} ↥(alternatingGroup α)
Tactic: rw [← isMulCommutative_iff_card_le_three]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
x : ↥(alternatingGroup ↥s)
⊢ Membership.mem (α := Perm α) (alternatingGroup α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑x : Perm ↥s) : Perm α)
have rw : Eq (α := ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑x : Perm ↥s)) :
    ℤˣ)
  (1 : ℤˣ)
Tactic: rw [mem_alternatingGroup, sign_ofSubtype, mem_alternatingGroup.mp x.prop]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
x : ↥(alternatingGroup ↥s)
rw :
  Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑x : Perm ↥s)) :
      ℤˣ)
    (1 : ℤˣ)
⊢ Membership.mem (α := Perm α) (alternatingGroup α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑x : Perm ↥s) : Perm α)
have rw₁ : Eq (α := ℤˣ) (((sign : Perm ↥s →* ℤˣ) : (a : Perm ↥s) → ℤˣ) (↑x : Perm ↥s) : ℤˣ) (1 : ℤˣ)
Tactic: rw [mem_alternatingGroup, sign_ofSubtype, mem_alternatingGroup.mp x.prop]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
x : ↥(alternatingGroup ↥s)
rw :
  Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑x : Perm ↥s)) :
      ℤˣ)
    (1 : ℤˣ)
rw₁ : Eq (α := ℤˣ) (((sign : Perm ↥s →* ℤˣ) : (a : Perm ↥s) → ℤˣ) (↑x : Perm ↥s) : ℤˣ) (1 : ℤˣ)
⊢ Membership.mem (α := Perm α) (alternatingGroup α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (↑x : Perm ↥s) : Perm α)
have rw₂ : Eq (α := ℤˣ) 1 1
Tactic: rw [mem_alternatingGroup, sign_ofSubtype, mem_alternatingGroup.mp x.prop]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ Function.Injective (α := ↥(alternatingGroup ↥s)) (β := ↥(alternatingGroup α))
    (⇑(ofSubtype s) : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α))
have rw : Function.Injective (α := ↥(alternatingGroup ↥s)) (β := Perm α)
  (Function.comp (β := ↥(alternatingGroup α)) (⇑(alternatingGroup α).subtype : (a : ↥(alternatingGroup α)) → Perm α)
    (⇑(ofSubtype s) : (a : ↥(alternatingGroup ↥s)) → ↥(alternatingGroup α)))
Tactic: rw [← Function.Injective.of_comp_iff (alternatingGroup α).subtype_injective]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s) =
    MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α
have h : ∀ (k : Perm α),
  Membership.mem (γ := Subgroup (Perm α))
      (map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s)) k ↔
    k ∈ MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α
Tactic: ext k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ MonoidHom.range (ofSubtype s) =
    subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α)
have rw : map (alternatingGroup α).subtype (MonoidHom.range (ofSubtype s)) =
  map (alternatingGroup α).subtype
    (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
Tactic: rw [← map_subtype_inj, ← MonoidHom.range_comp, ofSubtype_comp_subtype, MonoidHom.range_comp,
    range_subtype, subgroupOf_map_subtype, map_ofSubtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw :
  map (alternatingGroup α).subtype (MonoidHom.range (ofSubtype s)) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
⊢ MonoidHom.range (ofSubtype s) =
    subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α)
have rw₁ : ((alternatingGroup α).subtype.comp (ofSubtype s)).range =
  map (alternatingGroup α).subtype
    (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
Tactic: rw [← map_subtype_inj, ← MonoidHom.range_comp, ofSubtype_comp_subtype, MonoidHom.range_comp,
    range_subtype, subgroupOf_map_subtype, map_ofSubtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw :
  map (alternatingGroup α).subtype (MonoidHom.range (ofSubtype s)) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₁ :
  ((alternatingGroup α).subtype.comp (ofSubtype s)).range =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
⊢ MonoidHom.range (ofSubtype s) =
    subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α)
have rw₂ : MonoidHom.range (G := ↥(alternatingGroup ↥s))
    (MonoidHom.comp (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (Subgroup.subtype (alternatingGroup ↥s))) =
  map (alternatingGroup α).subtype
    (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
Tactic: rw [← map_subtype_inj, ← MonoidHom.range_comp, ofSubtype_comp_subtype, MonoidHom.range_comp,
    range_subtype, subgroupOf_map_subtype, map_ofSubtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw :
  map (alternatingGroup α).subtype (MonoidHom.range (ofSubtype s)) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₁ :
  ((alternatingGroup α).subtype.comp (ofSubtype s)).range =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₂ :
  MonoidHom.range (G := ↥(alternatingGroup ↥s))
      (MonoidHom.comp (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (Subgroup.subtype (alternatingGroup ↥s))) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
⊢ MonoidHom.range (ofSubtype s) =
    subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α)
have rw₃ : map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))
    (MonoidHom.range (G := ↥(alternatingGroup ↥s)) (Subgroup.subtype (alternatingGroup ↥s))) =
  map (alternatingGroup α).subtype
    (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
Tactic: rw [← map_subtype_inj, ← MonoidHom.range_comp, ofSubtype_comp_subtype, MonoidHom.range_comp,
    range_subtype, subgroupOf_map_subtype, map_ofSubtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw :
  map (alternatingGroup α).subtype (MonoidHom.range (ofSubtype s)) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₁ :
  ((alternatingGroup α).subtype.comp (ofSubtype s)).range =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₂ :
  MonoidHom.range (G := ↥(alternatingGroup ↥s))
      (MonoidHom.comp (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (Subgroup.subtype (alternatingGroup ↥s))) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₃ :
  map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))
      (MonoidHom.range (G := ↥(alternatingGroup ↥s)) (Subgroup.subtype (alternatingGroup ↥s))) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
⊢ MonoidHom.range (ofSubtype s) =
    subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α)
have rw₄ : map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s) =
  map (alternatingGroup α).subtype
    (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
Tactic: rw [← map_subtype_inj, ← MonoidHom.range_comp, ofSubtype_comp_subtype, MonoidHom.range_comp,
    range_subtype, subgroupOf_map_subtype, map_ofSubtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw :
  map (alternatingGroup α).subtype (MonoidHom.range (ofSubtype s)) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₁ :
  ((alternatingGroup α).subtype.comp (ofSubtype s)).range =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₂ :
  MonoidHom.range (G := ↥(alternatingGroup ↥s))
      (MonoidHom.comp (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (Subgroup.subtype (alternatingGroup ↥s))) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₃ :
  map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))
      (MonoidHom.range (G := ↥(alternatingGroup ↥s)) (Subgroup.subtype (alternatingGroup ↥s))) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₄ :
  map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
⊢ MonoidHom.range (ofSubtype s) =
    subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α)
have rw₅ : map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s) =
  MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α
Tactic: rw [← map_subtype_inj, ← MonoidHom.range_comp, ofSubtype_comp_subtype, MonoidHom.range_comp,
    range_subtype, subgroupOf_map_subtype, map_ofSubtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
rw :
  map (alternatingGroup α).subtype (MonoidHom.range (ofSubtype s)) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₁ :
  ((alternatingGroup α).subtype.comp (ofSubtype s)).range =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₂ :
  MonoidHom.range (G := ↥(alternatingGroup ↥s))
      (MonoidHom.comp (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (Subgroup.subtype (alternatingGroup ↥s))) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₃ :
  map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))
      (MonoidHom.range (G := ↥(alternatingGroup ↥s)) (Subgroup.subtype (alternatingGroup ↥s))) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₄ :
  map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s) =
    map (alternatingGroup α).subtype
      (subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α))
rw₅ :
  map (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) (alternatingGroup ↥s) =
    MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α
⊢ MonoidHom.range (ofSubtype s) =
    subgroupOf (MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s))) (alternatingGroup α)
have rw₆ : MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α =
  MonoidHom.range (G := Perm ↥s) (Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s)) ⊓ alternatingGroup α
Tactic: rw [← map_subtype_inj, ← MonoidHom.range_comp, ofSubtype_comp_subtype, MonoidHom.range_comp,
    range_subtype, subgroupOf_map_subtype, map_ofSubtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
k : ↥(alternatingGroup α)
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (MonoidHom.range (ofSubtype s)) k ↔ (↑k : Perm α).support ⊆ s
have rw : (↑(↑k : Perm α).support : Set α) ⊆ {x : α | x ∈ s} ↔ (↑k : Perm α).support ⊆ s
Tactic: rw [range_ofSubtype, mem_subgroupOf, Perm.mem_range_ofSubtype_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
g : ↥(alternatingGroup α)
⊢ HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
      ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α)) g : MulAut ↥(alternatingGroup α))
      (MonoidHom.range (ofSubtype s)) =
    MonoidHom.range (ofSubtype (g • s))
have h : ∀ (k : ↥(alternatingGroup α)),
  k ∈
      HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
        ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α)) g : MulAut ↥(alternatingGroup α))
        (MonoidHom.range (ofSubtype s)) ↔
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (MonoidHom.range (ofSubtype (g • s))) k
Tactic: ext k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
⊢ k ∈
      HSMul.hSMul (α := MulAut ↥(alternatingGroup α)) (β := Subgroup ↥(alternatingGroup α))
        ((MulAut.conj : (a : ↥(alternatingGroup α)) → MulAut ↥(alternatingGroup α)) g : MulAut ↥(alternatingGroup α))
        (MonoidHom.range (ofSubtype s)) ↔
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (MonoidHom.range (ofSubtype (g • s))) k
have h : (HSMul.hSMul (α := ConjAct (Perm α))
        ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) (↑g⁻¹ : Perm α) : ConjAct (Perm α))
        (↑k : Perm α)).support ⊆
    s ↔
  (↑k : Perm α).support ⊆ g • s
Tactic: simp_rw [mem_pointwise_smul_iff_inv_smul_mem, mem_range_ofSubtype_iff, ← map_inv,
    MulAut.smul_def, ← ConjAct.toConjAct_smul_eq_mulAut_conj, ConjAct.coe_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
⊢ G = 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 α
G : Subgroup (Perm α)
hG : G.index = 2
h : Nontrivial α
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∉ G
have by_contra! : ∀ (h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
this : G = ⊤
⊢ False
have hG₁ : Eq (α := ℕ) 1 2
Tactic: rw [this, Subgroup.index_top] at hG
Cleared hypotheses: hG, h_1, h, this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
⊢ False
have suffices : G = ⊤
Tactic: suffices G = ⊤ by rw [this, Subgroup.index_top] at hG; cases hG
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
⊢ G = ⊤
have rwa : ⊤ ≤ G
Tactic: rwa [eq_top_iff, ← closure_isSwap, G.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
rwa : ⊤ ≤ G
⊢ G = ⊤
have rwa₁ : closure {σ : Perm α | σ.IsSwap} ≤ G
Tactic: rwa [eq_top_iff, ← closure_isSwap, G.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h_1 : Nontrivial α
h : ∀ (g : Perm α) (_ : g.IsSwap), g ∈ G
rwa : ⊤ ≤ G
rwa₁ : closure {σ : Perm α | σ.IsSwap} ≤ G
⊢ G = ⊤
have rwa₂ : {σ : Perm α | σ.IsSwap} ⊆ (↑G : Set (Perm α))
Tactic: rwa [eq_top_iff, ← closure_isSwap, G.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : Nontrivial α
⊢ G = alternatingGroup α
have obtain : ∀ (a b : α) (hab : a ≠ b) (habG : swap a b ∉ G), G = alternatingGroup α
Tactic: obtain ⟨_, ⟨a, b, hab, rfl⟩, habG⟩ : ∃ g : Perm α, g.IsSwap ∧ g ∉ G := by
    by_contra! h
    suffices G = ⊤ by rw [this, Subgroup.index_top] at hG; cases hG
    rwa [eq_top_iff, ← closure_isSwap, G.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
h : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
⊢ G = alternatingGroup α
have h : ∀ (g : Perm α), g ∈ G ↔ g ∈ alternatingGroup α
Tactic: ext g