awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : Membership.mem (γ := Set α) {x : α | (l.formPerm ^ l.length : (a : α) → α) x ≠ x} x
⊢ False
have refine : x ∈ l
Tactic: refine hx ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : Membership.mem (γ := Set α) {x : α | (l.formPerm ^ l.length : (a : α) → α) x ≠ x} x
⊢ x ∈ l
have H₁ : Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x
Tactic: replace H := set_support_zpow_subset l.formPerm l.length H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
have this : x ∉ {x : α | (l.formPerm ^ l.length : (a : α) → α) x ≠ x}
Tactic: have : x ∉ { x | (l.formPerm ^ l.length) x ≠ x } := by
      intro H
      refine hx ?_
      replace H := set_support_zpow_subset l.formPerm l.length H
      simpa using support_formPerm_le' _ H
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
φ : ↥(stabilizer M s) → Perm (↑s : Type u_2) := toPerm
f : (↑s : Type u_2) →ₑ[φ] (↑s : Type u_2) := { toFun := id, map_smul' := ⋯ }
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)
have hf : Function.Bijective (α := (↑s : Type u_2)) (β := (↑s : Type u_2)) (⇑f : (a : (↑s : Type u_2)) → (↑s : Type u_2))
Tactic: have hf : Function.Bijective f := Function.bijective_id
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
φ : ↥(stabilizer M s) → Perm (↑s : Type u_2) := toPerm
f : (↑s : Type u_2) →ₑ[φ] (↑s : Type u_2) := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective (α := (↑s : Type u_2)) (β := (↑s : Type u_2)) (⇑f : (a : (↑s : Type u_2)) → (↑s : Type u_2))
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)
have rw : IsPreprimitive.{u_2, u_2} (Perm (↑s : Type u_2)) (↑s : Type u_2)
Tactic: rw [isPreprimitive_congr hs hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
this : ∃ (a : α) (b : α) (g : M), a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
⊢ IsPretransitive M α
have obtain : ∀ (a b : α) (g : M) (ha : a ∈ s) (hb : b ∈ sᶜ) (hgab : g • a = b), IsPretransitive M α
Tactic: obtain ⟨a, b, g, ha, hb, hgab⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
⊢ IsPretransitive M α
have rw : ∀ (x : α), ∃ (g : M), g • a = x
Tactic: rw [isPretransitive_iff_base a]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
⊢ ∃ (g : M), g • a = x
have pos : ∀ (hx : x ∈ s), ∃ (g : M), g • a = x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
pos : ∀ (hx : x ∈ s), ∃ (g : M), g • a = x
⊢ ∃ (g : M), g • a = x
have neg : ∀ (hx : x ∉ s), ∃ (g : M), g • a = x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∉ s
⊢ ∃ (g : M), g • a = x
have hx₁ : x ∈ sᶜ
Tactic: rw [← Set.mem_compl_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
⊢ ∃ (g : M), g • a = x
have neg : ∀ (k : M) (hk : k • b = x), ∃ (g : M), g • a = x
Tactic: obtain ⟨k, hk⟩ := hs' b hb x hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : M
hk : k • b = x
⊢ ∃ (g : M), g • a = x
have h : (k * g) • a = x
Tactic: use k * g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : M
hk : k • b = x
⊢ (k * g) • a = x
have h : k • g • a = x
Tactic: rw [mul_smul, hgab, hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
k : M
hk : k • b = x
h : k • g • a = x
h₁ : k • b = x
⊢ (k * g) • a = x
have h₂ : x = x
Tactic: rw [mul_smul, hgab, hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
⊢ IsPretransitive M α
have suffices : ∃ (a : α) (b : α) (g : M), a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
Tactic: suffices ∃ (a b : α) (g : M), a ∈ s ∧ b ∈ sᶜ ∧ g • a = b by
    obtain ⟨a, b, g, ha, hb, hgab⟩ := this
    rw [isPretransitive_iff_base a]
    intro x
    by_cases hx : x ∈ s
    · exact hs a ha x hx
    · rw [← Set.mem_compl_iff] at hx
      obtain ⟨k, hk⟩ := hs' b hb x hx
      use k * g
      rw [mul_smul, hgab, hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : Ne (α := Subgroup M) (stabilizer M s) ⊤
⊢ ∃ (a : α) (b : α) (g : M), a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
have contrapose! : ∀ (hM : ∀ (a b : α) (g : M) (_ : a ∈ s) (_ : b ∈ sᶜ), g • a ≠ b), Eq (α := Subgroup M) (stabilizer M s) ⊤
Tactic: contrapose! hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : ∀ (a b : α) (g : M) (_ : a ∈ s) (_ : b ∈ sᶜ), g • a ≠ b
⊢ Eq (α := Subgroup M) (stabilizer M s) ⊤
have rw : ∀ (g : M), Membership.mem (γ := Subgroup M) ⊤ g → g • s ⊆ s
Tactic: rw [eq_top_iff, le_stabilizer_iff_smul_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b
hM : ∀ (a b : α) (g : M) (_ : a ∈ s) (_ : b ∈ sᶜ), g • a ≠ b
g : M
h : Membership.mem (γ := Subgroup M) ⊤ g
b a : α
ha : a ∈ s
hgab : (fun (x : α) ↦ g • x) a = b
⊢ b ∈ s
have by_contra : ∀ (hb : b ∉ s), False
Tactic: by_contra hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : Perm (↑s : Type u_2)
⊢ HSMul.hSMul (α := Perm α) ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
      s =
    s
have h : ∀ (g' : α),
  g' ∈
      HSMul.hSMul (α := Perm α)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s ↔
    g' ∈ s
Tactic: ext g'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : Perm (↑s : Type u_2)
g' : α
⊢ g' ∈
      HSMul.hSMul (α := Perm α)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s ↔
    g' ∈ s
have h : (∃ y ∈ s,
    (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) y =
      g') ↔
  g' ∈ s
Tactic: simp_rw [mem_smul_set, Perm.smul_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : Perm (↑s : Type u_2)
g' : α
⊢ (∃ y ∈ s,
      (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) y =
        g') ↔
    g' ∈ s
have h : (∃ y ∈ s,
    (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) y =
      g') →
  g' ∈ s
Tactic: refine ⟨?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : Perm (↑s : Type u_2)
g' : α
h :
  (∃ y ∈ s,
      (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) y =
        g') →
    g' ∈ s
⊢ (∃ y ∈ s,
      (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) y =
        g') ↔
    g' ∈ s
have h₁ : ∀ (a : g' ∈ s),
  ∃ y ∈ s,
    (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) y = g'
Tactic: refine ⟨?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : Perm (↑s : Type u_2)
g' : α
a : g' ∈ s
⊢ ∃ y ∈ s,
    (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) y = g'
have h : (↑((g⁻¹ : (a : (↑s : Type u_2)) → (↑s : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) g' a)) : α) ∈ s ∧
  (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α)
      (↑((g⁻¹ : (a : (↑s : Type u_2)) → (↑s : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) g' a)) : α) =
    g'
Tactic: use (g⁻¹ ⟨g', a⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s = s
have apply : s ⊆ swap a b • s
Tactic: apply Set.Subset.antisymm this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b)
have suffices : swap a b • s ⊆ s
Tactic: suffices swap a b • s ⊆ s by
    rw [mem_stabilizer_iff]
    apply Set.Subset.antisymm this
    exact Set.subset_smul_set_iff.mpr this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
⊢ (fun (x : α) ↦ swap a b • x) x ∈ s
have pos : ∀ (h : Membership.mem (γ := Set α) {a, b} x), (fun (x : α) ↦ swap a b • x) x ∈ s
Tactic: by_cases h : x ∈ ({a, b} : Set α)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
pos : ∀ (h : Membership.mem (γ := Set α) {a, b} x), (fun (x : α) ↦ swap a b • x) x ∈ s
⊢ (fun (x : α) ↦ swap a b • x) x ∈ s
have neg : ∀ (h : x ∉ {a, b}), (fun (x : α) ↦ swap a b • x) x ∈ s
Tactic: by_cases h : x ∈ ({a, b} : Set α)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
h : x ∉ {a, b}
⊢ (fun (x : α) ↦ swap a b • x) x ∈ s
have this : x ≠ a → x ≠ b → (swap a b : (a : α) → α) x = x
Tactic: have := swap_apply_of_ne_of_ne (a := a) (b := b) (x := x)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
g : Perm (↑s : Type u_2)
⊢ ∃ (a : ↥(stabilizer (Perm α) s)), toPerm a = g
have property : Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (stabilizer (Perm α) s)
  ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
Tactic: use! Perm.ofSubtype g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
g : Perm (↑s : Type u_2)
property :
  Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (stabilizer (Perm α) s)
    ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
⊢ ∃ (a : ↥(stabilizer (Perm α) s)), toPerm a = g
have h : toPerm (α := ↥(stabilizer (Perm α) s))
    (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) x)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) sorry :
      ↥(stabilizer (Perm α) s)) =
  g
Tactic: use! Perm.ofSubtype g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
g : Perm (↑s : Type u_2)
⊢ ∃ (a : ↥(stabilizer (Perm α) s)), toPerm a = g
have w : ↥(stabilizer (Perm α) s)
Tactic: classical
  use! Perm.ofSubtype g
  · apply ofSubtype_mem_stabilizer
  · aesop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
g : Perm (↑s : Type u_2)
w : ↥(stabilizer (Perm α) s)
⊢ ∃ (a : ↥(stabilizer (Perm α) s)), toPerm a = g
have val : Perm α
Tactic: classical
  use! Perm.ofSubtype g
  · apply ofSubtype_mem_stabilizer
  · aesop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
g : Perm (↑s : Type u_2)
w : ↥(stabilizer (Perm α) s)
val : Perm α
⊢ ∃ (a : ↥(stabilizer (Perm α) s)), toPerm a = g
have property : Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (stabilizer (Perm α) s)
  ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
Tactic: classical
  use! Perm.ofSubtype g
  · apply ofSubtype_mem_stabilizer
  · aesop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
g : Perm (↑s : Type u_2)
w : ↥(stabilizer (Perm α) s)
val : Perm α
property :
  Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (stabilizer (Perm α) s)
    ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
⊢ ∃ (a : ↥(stabilizer (Perm α) s)), toPerm a = g
have h : toPerm (α := ↥(stabilizer (Perm α) s))
    (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) x)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) sorry :
      ↥(stabilizer (Perm α) s)) =
  g
Tactic: classical
  use! Perm.ofSubtype g
  · apply ofSubtype_mem_stabilizer
  · aesop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nonempty
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
have obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
Tactic: obtain ⟨a, ha⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
hsc : sᶜ.Nonempty
a : α
ha : a ∈ s
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
have obtain : ∀ (b : α) (hb : b ∈ sᶜ), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
Tactic: obtain ⟨b, hb⟩ := hsc
Cleared hypotheses: hsc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
⊢ False
have hb₁ : b ∉ s
Tactic: rw [Set.mem_compl_iff] at hb
Cleared hypotheses: hb, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
⊢ False
have apply : b ∈ s
Tactic: apply hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
⊢ b ∈ s
have hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b)
Tactic: have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b)
⊢ b ∈ s
have hg₁ : swap a b • s = s
Tactic: rw [mem_stabilizer_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
hg : swap a b • s = s
⊢ b ∈ s
have rw : ∃ y ∈ s, swap a b • y = b
Tactic: rw [← hg, Set.mem_smul_set]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nonempty
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
have obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
Tactic: classical
  obtain ⟨a, ha⟩ := hs
  obtain ⟨b, hb⟩ := hsc
  intro h
  rw [Set.mem_compl_iff] at hb; apply hb
  have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all
  rw [mem_stabilizer_iff] at hg
  rw [← hg, Set.mem_smul_set]
  aesop
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nonempty
obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
have obtain₁ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
Tactic: classical
  obtain ⟨a, ha⟩ := hs
  obtain ⟨b, hb⟩ := hsc
  intro h
  rw [Set.mem_compl_iff] at hb; apply hb
  have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all
  rw [mem_stabilizer_iff] at hg
  rw [← hg, Set.mem_smul_set]
  aesop
Cleared hypotheses: hs, hsc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nonempty
obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₁ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₂ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
have obtain₃ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
Tactic: classical
  obtain ⟨a, ha⟩ := hs
  obtain ⟨b, hb⟩ := hsc
  intro h
  rw [Set.mem_compl_iff] at hb; apply hb
  have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all
  rw [mem_stabilizer_iff] at hg
  rw [← hg, Set.mem_smul_set]
  aesop
Cleared hypotheses: hs, hsc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nonempty
obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₁ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₂ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
obtain₃ obtain₄ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
have obtain₅ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), b ∈ s
Tactic: classical
  obtain ⟨a, ha⟩ := hs
  obtain ⟨b, hb⟩ := hsc
  intro h
  rw [Set.mem_compl_iff] at hb; apply hb
  have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all
  rw [mem_stabilizer_iff] at hg
  rw [← hg, Set.mem_smul_set]
  aesop
Cleared hypotheses: hs, hsc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nonempty
obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₁ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₂ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
obtain₃ obtain₄ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
obtain₅ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), b ∈ s
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
have obtain₆ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤)
  (hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b)), b ∈ s
Tactic: classical
  obtain ⟨a, ha⟩ := hs
  obtain ⟨b, hb⟩ := hsc
  intro h
  rw [Set.mem_compl_iff] at hb; apply hb
  have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all
  rw [mem_stabilizer_iff] at hg
  rw [← hg, Set.mem_smul_set]
  aesop
Cleared hypotheses: hs, hsc