awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
h : a ≠ b ∧ _root_.Disjoint s (↑(swap a b).support : Set α)
⊢ (swap a b).IsSwap ∧ _root_.Disjoint s (↑(swap a b).support : Set α)

Tactic:
rw [swap_isSwap_iff]

Premises used: Equiv.Perm.swap_isSwap_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ a ≠ b ∧ _root_.Disjoint s (↑(swap a b).support : Set α)

Tactic:
aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
⊢ ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)

Tactic:
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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
obtain :
  ∀ (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

Tactic:
obtain ⟨k, hk_swap, hk_support⟩ := this
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 α)
rw : k • s ⊆ s
⊢ k • s = s

Tactic:
rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]

Premises used: Set.toFinite, MulAction.mem_stabilizer_set_iff_smul_set_subset, MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 α)
x : α
hx : x ∈ s
⊢ x ∈ s

Tactic:
hx
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 α)
x : α
hx : x ∈ s
h : k • x = x
⊢ k • x ∈ s

Tactic:
convert! hx
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 α)
x : α
hx : x ∈ s
h : x ∉ k.support
⊢ k • x = x

Tactic:
rw [Perm.smul_def, ← Perm.notMem_support]

Premises used: Equiv.Perm.smul_def, Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 α)
x : α
hx : x ∈ s
⊢ x ∉ k.support

Tactic:
(Set.disjoint_left.mp hk_support) hx

Premises used: Set.disjoint_left, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 α)
x : α
hx : x ∈ s
⊢ x ∉ k.support

Tactic:
exact (Set.disjoint_left.mp hk_support) hx

Premises used: Set.disjoint_left, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 α)
⊢ k • s = s

Tactic:
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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
inl :
  ∀ (hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (1 : ℤˣ)),
    ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
inr :
  ∀ (hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)),
    ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g

Tactic:
rcases Int.units_eq_one_or (sign g) with hsg | hsg

Premises used: Equiv.Perm.sign, Int.units_eq_one_or, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 : ℤˣ)
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g

Tactic:
Equiv.Perm.ofSubtype g

Premises used: Equiv.Perm.ofSubtype, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 :
  Membership.mem (α := Perm α) (alternatingGroup α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
property₁ :
  Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α))
    (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) ⋯ :
      ↥(alternatingGroup α))
h :
  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 α)
            ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) ⋯)
          ⋯ :
        ↥(stabilizer (↥(alternatingGroup α)) s)) =
    g
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g

Tactic:
use! Equiv.Perm.ofSubtype g

Premises used: Equiv.Perm.ofSubtype, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 : ℤˣ)
⊢ Membership.mem (α := Perm α) (alternatingGroup α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)

Tactic:
simp [mem_alternatingGroup, hsg]

Premises used: Equiv.Perm.mem_alternatingGroup
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s =
    s
⊢ Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α))
    (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) ⋯ :
      ↥(alternatingGroup α))

Tactic:
rw [mem_stabilizer_iff, Submonoid.mk_smul]

Premises used: Submonoid.mk_smul, MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 : ℤˣ)
⊢ HSMul.hSMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s =
    s

Tactic:
ofSubtype_mem_stabilizer g

Premises used: Set.Mem, setOf, Equiv.Perm.ofSubtype_mem_stabilizer
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 : ℤˣ)
⊢ HSMul.hSMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s =
    s

Tactic:
exact ofSubtype_mem_stabilizer g

Premises used: Equiv.Perm.ofSubtype_mem_stabilizer
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 α)
            ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) ⋯)
          ⋯ :
        ↥(stabilizer (↥(alternatingGroup α)) s)) =
    g

Tactic:
aesop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 :
  HMul.hMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k ∈
    alternatingGroup α
property₁ :
  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)
      ⋯)
h :
  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
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g

Tactic:
use! Equiv.Perm.ofSubtype g * k

Premises used: Equiv.Perm.ofSubtype, DFunLike.coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 : ℤˣ)
⊢ HMul.hMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k ∈
    alternatingGroup α

Tactic:
simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]

Premises used: Equiv.Perm.mem_alternatingGroup, Equiv.Perm.IsSwap.sign_eq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
property₄ property₅ : 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)
      ⋯)

Tactic:
rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]

Premises used: Submonoid.mk_smul, MulAction.mem_stabilizer_iff, Equiv.Perm.ofSubtype_mem_stabilizer, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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 : ℤˣ)
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)
                    ⋯)
                  ⋯) :
              (a : (↑s : Type u_1)) → (↑s : Type u_1))
            x) :
        α)
      (↑((g : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x) : α)
⊢ 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

Tactic:
ext x
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
this : (k : (a : α) → α) (↑x : α) = (↑x : α)
⊢ 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) : α)

Tactic:
simp [this]
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
h : (k : (a : α) → α) (↑x : α) = (↑x : α)
⊢ 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) : α)

Tactic:
suffices k x = x by simp [this]
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
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 : α)
⊢ (k : (a : α) → α) (↑x : α) = (↑x : α)

Tactic:
rw [Set.disjoint_left] at hk_support

Premises used: Set.disjoint_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
h : (↑x : α) ∉ k.support
⊢ (k : (a : α) → α) (↑x : α) = (↑x : α)

Tactic:
rw [← notMem_support]

Premises used: Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
⊢ (↑x : α) ∉ k.support

Tactic:
hk_support x.prop

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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)
⊢ (↑x : α) ∉ k.support

Tactic:
exact hk_support x.prop

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
⊢ IsPreprimitive.{u_1, u_1} ↥(stabilizer (↥(alternatingGroup α)) s) (↑s : Type u_1)

Tactic:
isPreprimitive_stabilizer_of_surjective s (stabilizer.surjective_toPerm hs)

Premises used: Set.Mem, setOf, alternatingGroup.stabilizer.surjective_toPerm, MulAction.isPreprimitive_stabilizer_of_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hsc : sᶜ.Nontrivial
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
⊢ IsPreprimitive.{u_1, u_1} ↥(stabilizer (↥G) s) (↑s : Type u_1)

Tactic:
have := stabilizer_isPreprimitive hsc
  let φ (g : stabilizer (alternatingGroup α) s) : stabilizer G s :=
      ⟨⟨g, hG g.prop⟩, g.prop⟩
  let f : s →ₑ[φ] s := {
      toFun := id
      map_smul' _ _ := rfl }
  IsPreprimitive.of_surjective (f := f) Function.surjective_id

Premises used: MulAction.IsPreprimitive.of_surjective, id, MulActionHom.mk, Subtype.mk, alternatingGroup.stabilizer_isPreprimitive, Subtype.prop, Function.surjective_id, Subtype.val, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nontrivial
obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤
⊢ Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hsc : sᶜ.Nontrivial
a : α
ha : a ∈ s
obtain :
  ∀ (b : α) (hb : b ∈ sᶜ) (c : α) (hc : c ∈ sᶜ) (hbc : b ≠ c),
    Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤
⊢ Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤

Tactic:
obtain ⟨b, hb, c, hc, hbc⟩ := hsc
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
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
contrapose! :
  ∀ (this : Eq (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤)
    (g : ↥(alternatingGroup α)),
    Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) g
⊢ Ne (α := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) ⊤

Tactic:
contrapose! this