awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
property :
  HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        (HMul.hMul (α := Perm α)
          ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
        ⋯)
      s =
    s
property₁ :
  HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k •
      s =
    s
property₂ :
  HSMul.hSMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) (k • s) =
    s
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      (HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
      ⋯)
have property₃ : HSMul.hSMul (α := Perm α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s =
  s
Tactic: rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
property :
  HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        (HMul.hMul (α := Perm α)
          ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
        ⋯)
      s =
    s
property₁ :
  HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k •
      s =
    s
property₂ :
  HSMul.hSMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) (k • s) =
    s
property₃ :
  HSMul.hSMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s =
    s
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      (HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
      ⋯)
have property₄ : s = s
Tactic: rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
⊢ toPerm (α := ↥(stabilizer (↥(alternatingGroup α)) s))
      (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦
        Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) x)
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
          (HMul.hMul (α := Perm α)
            ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
          ⋯)
        ⋯) =
    g
have h : ∀ (x : (↑s : Type u_1)),
  Eq.{u_1 + 1} (α := α)
    (↑((toPerm (α := ↥(stabilizer (↥(alternatingGroup α)) s))
              (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦
                Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) x)
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
                  (HMul.hMul (α := Perm α)
                    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
                  sorry)
                sorry) :
            (a : (↑s : Type u_1)) → (↑s : Type u_1))
          x) :
      α)
    (↑((g : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x) : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
x : (↑s : Type u_1)
⊢ Eq.{u_1 + 1} (α := α)
    (↑((toPerm (α := ↥(stabilizer (↥(alternatingGroup α)) s))
              (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦
                Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) x)
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
                  (HMul.hMul (α := Perm α)
                    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
                  ⋯)
                ⋯) :
            (a : (↑s : Type u_1)) → (↑s : Type u_1))
          x) :
      α)
    (↑((g : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x) : α)
have h : (k : (a : α) → α) (↑x : α) = (↑x : α)
Tactic: suffices k x = x by simp [this]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
x : (↑s : Type u_1)
⊢ (k : (a : α) → α) (↑x : α) = (↑x : α)
have h : ∀ (hk_support : ∀ ⦃a : α⦄, a ∈ s → a ∉ (↑k.support : Set α)) (hks : k • s = s) (g : Perm (↑s : Type u_1))
  (hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ))
  (x : (↑s : Type u_1)), (k : (a : α) → α) (↑x : α) = (↑x : α)
Tactic: rw [Set.disjoint_left] at hk_support
Cleared hypotheses: hk_support, hks, g, hsg, x
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : ∀ ⦃a : α⦄, a ∈ s → a ∉ (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
x : (↑s : Type u_1)
⊢ (k : (a : α) → α) (↑x : α) = (↑x : α)
have h : (↑x : α) ∉ k.support
Tactic: rw [← notMem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
have have : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
Tactic: classical
  have : ∃ k : Perm α, IsSwap k ∧ _root_.Disjoint s k.support := by
    obtain ⟨a, ha, b, hb, hab⟩ := hs
    use Equiv.swap a b
    rw [swap_isSwap_iff]; aesop
  obtain ⟨k, hk_swap, hk_support⟩ := this
  have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx
  intro g
  rcases Int.units_eq_one_or (sign g) with hsg | hsg
  · use! Equiv.Perm.ofSubtype g
    · simp [mem_alternatingGroup, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g
    · aesop
  · use! Equiv.Perm.ofSubtype g * k
    · simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
    · ext x
      suffices k x = x by simp [this]
      rw [Set.disjoint_left] at hk_support
      rw [← notMem_support]
      exact hk_support x.prop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
have : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
have have₁ : ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
  Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
Tactic: classical
  have : ∃ k : Perm α, IsSwap k ∧ _root_.Disjoint s k.support := by
    obtain ⟨a, ha, b, hb, hab⟩ := hs
    use Equiv.swap a b
    rw [swap_isSwap_iff]; aesop
  obtain ⟨k, hk_swap, hk_support⟩ := this
  have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx
  intro g
  rcases Int.units_eq_one_or (sign g) with hsg | hsg
  · use! Equiv.Perm.ofSubtype g
    · simp [mem_alternatingGroup, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g
    · aesop
  · use! Equiv.Perm.ofSubtype g * k
    · simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
    · ext x
      suffices k x = x by simp [this]
      rw [Set.disjoint_left] at hk_support
      rw [← notMem_support]
      exact hk_support x.prop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
have : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₁ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₂ : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₃ have₄ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
have have₅ : ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)),
  Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
Tactic: classical
  have : ∃ k : Perm α, IsSwap k ∧ _root_.Disjoint s k.support := by
    obtain ⟨a, ha, b, hb, hab⟩ := hs
    use Equiv.swap a b
    rw [swap_isSwap_iff]; aesop
  obtain ⟨k, hk_swap, hk_support⟩ := this
  have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx
  intro g
  rcases Int.units_eq_one_or (sign g) with hsg | hsg
  · use! Equiv.Perm.ofSubtype g
    · simp [mem_alternatingGroup, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g
    · aesop
  · use! Equiv.Perm.ofSubtype g * k
    · simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
    · ext x
      suffices k x = x by simp [this]
      rw [Set.disjoint_left] at hk_support
      rw [← notMem_support]
      exact hk_support x.prop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
have : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₁ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₂ : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₃ have₄ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₅ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
have have₆ : ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s),
  Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
Tactic: classical
  have : ∃ k : Perm α, IsSwap k ∧ _root_.Disjoint s k.support := by
    obtain ⟨a, ha, b, hb, hab⟩ := hs
    use Equiv.swap a b
    rw [swap_isSwap_iff]; aesop
  obtain ⟨k, hk_swap, hk_support⟩ := this
  have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx
  intro g
  rcases Int.units_eq_one_or (sign g) with hsg | hsg
  · use! Equiv.Perm.ofSubtype g
    · simp [mem_alternatingGroup, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g
    · aesop
  · use! Equiv.Perm.ofSubtype g * k
    · simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
    · ext x
      suffices k x = x by simp [this]
      rw [Set.disjoint_left] at hk_support
      rw [← notMem_support]
      exact hk_support x.prop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
have : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₁ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₂ : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₃ have₄ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₅ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₆ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
have have₇ : ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s)
  (g : Perm (↑s : Type u_1)), ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
Tactic: classical
  have : ∃ k : Perm α, IsSwap k ∧ _root_.Disjoint s k.support := by
    obtain ⟨a, ha, b, hb, hab⟩ := hs
    use Equiv.swap a b
    rw [swap_isSwap_iff]; aesop
  obtain ⟨k, hk_swap, hk_support⟩ := this
  have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx
  intro g
  rcases Int.units_eq_one_or (sign g) with hsg | hsg
  · use! Equiv.Perm.ofSubtype g
    · simp [mem_alternatingGroup, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g
    · aesop
  · use! Equiv.Perm.ofSubtype g * k
    · simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
    · ext x
      suffices k x = x by simp [this]
      rw [Set.disjoint_left] at hk_support
      rw [← notMem_support]
      exact hk_support x.prop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
have : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₁ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₂ : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have₃ have₄ :
  ∀ (this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₅ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₆ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s),
    Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
      toPerm
have₇ :
  ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s)
    (g : Perm (↑s : Type u_1)), ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
have inl : ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)) (hks : k • s = s)
  (g : Perm (↑s : Type u_1))
  (hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (1 : ℤˣ)),
  ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
Tactic: classical
  have : ∃ k : Perm α, IsSwap k ∧ _root_.Disjoint s k.support := by
    obtain ⟨a, ha, b, hb, hab⟩ := hs
    use Equiv.swap a b
    rw [swap_isSwap_iff]; aesop
  obtain ⟨k, hk_swap, hk_support⟩ := this
  have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx
  intro g
  rcases Int.units_eq_one_or (sign g) with hsg | hsg
  · use! Equiv.Perm.ofSubtype g
    · simp [mem_alternatingGroup, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g
    · aesop
  · use! Equiv.Perm.ofSubtype g * k
    · simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]
    · rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
    · ext x
      suffices k x = x by simp [this]
      rw [Set.disjoint_left] at hk_support
      rw [← notMem_support]
      exact hk_support x.prop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nontrivial
⊢ Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤
have obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hsc : sᶜ.Nontrivial
a : α
ha : a ∈ s
⊢ Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤
have obtain : ∀ (b : α) (hb : b ∈ sᶜ) (c : α) (hc : c ∈ sᶜ) (hbc : b ≠ c),
  Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤
Tactic: obtain ⟨b, hb, c, hc, hbc⟩ := hsc
Cleared hypotheses: hsc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
this : ∃ (g : ↥(alternatingGroup α)), g ∉ stabilizer (↥(alternatingGroup α)) s
⊢ Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤
have contrapose! : ∀ (this : Eq (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤)
  (g : ↥(alternatingGroup α)),
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) g
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤
have suffices : ∃ (g : ↥(alternatingGroup α)), g ∉ stabilizer (↥(alternatingGroup α)) s
Tactic: suffices ∃ g, g ∉ stabilizer (alternatingGroup α) s by contrapose! this; simp [this]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ ∃ (g : ↥(alternatingGroup α)), g ∉ stabilizer (↥(alternatingGroup α)) s
have h : Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap a c) sorry ∉
  stabilizer (↥(alternatingGroup α)) s
Tactic: use ⟨Equiv.swap a b * Equiv.swap a c, by aesop⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) (swap a b * swap a c) ⋯ ∉
    stabilizer (↥(alternatingGroup α)) s
have h : ¬∀ (b_1 : α), Membership.mem (α := α) s ((swap a b : (a : α) → α) ((swap a c : (a : α) → α) b_1 : α) : α) ↔ b_1 ∈ s
Tactic: simp_rw [mem_stabilizer_set, Subgroup.mk_smul, mul_smul, Perm.smul_def]