awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h_1 : ¬(l.formPerm ^ n : (a : α) → α) x = x
h :
  Membership.mem (α := α) (γ := Set α) {x : α | (l.formPerm ^ n : (a : α) → α) x ≠ x}
    ((l.formPerm ^ n : (a : α) → α) x : α)
⊢ Membership.mem (α := α) (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} ((l.formPerm ^ n : (a : α) → α) x : α)

Tactic:
replace h := set_support_zpow_subset _ _ h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h_1 : ¬(l.formPerm ^ n : (a : α) → α) x = x
h :
  Membership.mem (α := α) (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} ((l.formPerm ^ n : (a : α) → α) x : α)
⊢ Membership.mem (α := α) l ((l.formPerm ^ n : (a : α) → α) x : α)

Tactic:
simpa using support_formPerm_le' _ h

Premises used: List.support_formPerm_le'
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
H : ∀ (x : α), Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ l.formPerm ^ l.length = 1

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
pos : ∀ (hx : x ∈ l), Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
neg : ∀ (hx : x ∉ l), Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)

Tactic:
by_cases hx : x ∈ l
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
pos :
  ∀ (k : ℕ) (hk : k < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l),
    Eq (α := α)
      ((l.formPerm ^ l.length : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) : α)
      ((1 : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) : α)
⊢ Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Premises used: List.getElem_of_mem, rfl
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
⊢ Eq (α := α)
    ((l.formPerm ^ l.length : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) : α)
    ((1 : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) : α)

Tactic:
simp [formPerm_pow_apply_getElem _ hl, Nat.mod_eq_of_lt hk]

Premises used: Nat.mod_eq_of_lt, List.formPerm_pow_apply_getElem
-- Module: Mathlib.GroupTheory.Perm.List
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

Tactic:
hx ?_
-- Module: Mathlib.GroupTheory.Perm.List
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
refine : x ∈ l
⊢ False

Tactic:
refine hx ?_
-- Module: Mathlib.GroupTheory.Perm.List
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
⊢ Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x

Tactic:
replace H := set_support_zpow_subset l.formPerm l.length H
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x
⊢ x ∈ l

Tactic:
simpa using support_formPerm_le' _ H

Premises used: List.support_formPerm_le'
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ 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
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
this : x ∉ {x : α | (l.formPerm ^ l.length : (a : α) → α) x ≠ x}
⊢ Eq (α := α) ((l.formPerm ^ l.length : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)

Tactic:
simpa using this
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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' := ⋯ }
⊢ 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
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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))
rw : IsPreprimitive.{u_2, u_2} (Perm (↑s : Type u_2)) (↑s : Type u_2)
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)

Tactic:
rw [isPreprimitive_congr hs hf]

Premises used: MulAction.isPreprimitive_congr
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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_2, u_2} (Perm (↑s : Type u_2)) (↑s : Type u_2)

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)
G : Subgroup M
hG : stabilizer M s ≤ G
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)

Tactic:
let φ (g : stabilizer M 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, Subtype.prop, Function.surjective_id, Subtype.val, rfl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
obtain : ∀ (a b : α) (g : M) (ha : a ∈ s) (hb : b ∈ sᶜ) (hgab : g • a = b), IsPretransitive M α
⊢ IsPretransitive M α

Tactic:
obtain ⟨a, b, g, ha, hb, hgab⟩ := this
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
rw : ∀ (x : α), ∃ (g : M), g • a = x
⊢ IsPretransitive M α

Tactic:
rw [isPretransitive_iff_base a]

Premises used: MulAction.isPretransitive_iff_base
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
neg : ∀ (hx : x ∉ s), ∃ (g : M), g • a = x
⊢ ∃ (g : M), g • a = x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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

Tactic:
hs a ha x hx
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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

Tactic:
exact hs a ha x hx
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ x ∈ sᶜ

Tactic:
rw [← Set.mem_compl_iff] at hx

Premises used: Set.mem_compl_iff
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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ᶜ
neg : ∀ (k : M) (hk : k • b = x), ∃ (g : M), g • a = x
⊢ ∃ (g : M), g • a = x

Tactic:
obtain ⟨k, hk⟩ := hs' b hb x hx
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ ∃ (g : M), g • a = x

Tactic:
use k * g
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
h₂ h₃ : x = x
⊢ (k * g) • a = x

Tactic:
rw [mul_smul, hgab, hk]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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) ⊤
suffices : ∃ (a : α) (b : α) (g : M), a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
⊢ IsPretransitive M α

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]
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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) ⊤
contrapose! : ∀ (hM : ∀ (a b : α) (g : M) (_ : a ∈ s) (_ : b ∈ sᶜ), g • a ≠ b), Eq (α := Subgroup M) (stabilizer M s) ⊤
⊢ ∃ (a : α) (b : α) (g : M), a ∈ s ∧ b ∈ sᶜ ∧ g • a = b

Tactic:
contrapose! hM
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
rw : ∀ (g : M), Membership.mem (γ := Subgroup M) ⊤ g → g • s ⊆ s
⊢ Eq (α := Subgroup M) (stabilizer M s) ⊤

Tactic:
rw [eq_top_iff, le_stabilizer_iff_smul_le]

Premises used: eq_top_iff, MulAction.le_stabilizer_iff_smul_le
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
by_contra : ∀ (hb : b ∉ s), False
⊢ b ∈ s

Tactic:
by_contra hb
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
hb : b ∉ s
⊢ False

Tactic:
hM a b g ha (Set.mem_compl hb) hgab

Premises used: Set.mem_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
hb : b ∉ s
⊢ False

Tactic:
exact hM a b g ha (Set.mem_compl hb) hgab

Premises used: Set.mem_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : Perm (↑s : Type u_2)
h :
  ∀ (g' : α),
    g' ∈
        HSMul.hSMul (α := Perm α)
          ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s ↔
      g' ∈ s
⊢ HSMul.hSMul (α := Perm α) ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
      s =
    s

Tactic:
ext g'
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ g' ∈
      HSMul.hSMul (α := Perm α)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s ↔
    g' ∈ s

Tactic:
simp_rw [mem_smul_set, Perm.smul_def]

Premises used: Equiv.Perm.smul_def, Set.mem_smul_set
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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

Tactic:
⟨?_, fun a ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
h₁ :
  ∀ (a : g' ∈ s),
    ∃ y ∈ s,
      (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) y =
        g'
⊢ (∃ 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 ↦ ?_⟩
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : Perm (↑s : Type u_2)
w : α
hs : w ∈ s
⊢ Membership.mem (α := α) s
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) w : α)

Tactic:
simp [ofSubtype_apply_of_mem _ hs]

Premises used: Equiv.Perm.ofSubtype_apply_of_mem
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : Perm (↑s : Type u_2)
g' : α
a : g' ∈ s
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'
⊢ ∃ y ∈ s,
    (((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) : (a : α) → α) y = g'

Tactic:
use (g⁻¹ ⟨g', a⟩)

Premises used: Subtype.mk, Inv.inv, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : Perm (↑s : Type u_2)
g' : α
a : g' ∈ s
⊢ (↑((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:
simp
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
apply : s ⊆ swap a b • s
⊢ swap a b • s = s

Tactic:
apply Set.Subset.antisymm this

Premises used: Set.Subset.antisymm
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s

Tactic:
Set.subset_smul_set_iff.mpr this

Premises used: Iff.mpr, Set.subset_smul_set_iff
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s

Tactic:
exact Set.subset_smul_set_iff.mpr this

Premises used: Iff.mpr, Set.subset_smul_set_iff
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
suffices : swap a b • s ⊆ s
⊢ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b)

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
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
neg : ∀ (h : x ∉ {a, b}), (fun (x : α) ↦ swap a b • x) x ∈ s
⊢ (fun (x : α) ↦ swap a b • x) x ∈ s

Tactic:
by_cases h : x ∈ ({a, b} : Set α)

Premises used: Insert.insert, Singleton.singleton
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
h : Membership.mem (γ := Set α) {a, b} x
⊢ (fun (x : α) ↦ swap a b • x) x ∈ s

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
h : x ∉ {a, b}
⊢ x ≠ a → x ≠ b → (swap a b : (a : α) → α) x = x

Tactic:
have := swap_apply_of_ne_of_ne (a := a) (b := b) (x := x)
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
h : x ∉ {a, b}
this : x ≠ a → x ≠ b → (swap a b : (a : α) → α) x = x
⊢ (fun (x : α) ↦ swap a b • x) x ∈ s

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g • a = b

Tactic:
⟨swap a b, swap_mem_stabilizer ha hb, swap_apply_left a b⟩

Premises used: Equiv.swap, Equiv.Perm.swap_mem_stabilizer, And.intro, Exists.intro, Equiv.swap_apply_left
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g • a = b

Tactic:
exact ⟨swap a b, swap_mem_stabilizer ha hb, swap_apply_left a b⟩
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g • a = b

Tactic:
classical
  exact ⟨swap a b, swap_mem_stabilizer ha hb, swap_apply_left a b⟩
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
g : Perm (↑s : Type u_2)
⊢ ∃ (a : ↥(stabilizer (Perm α) s)), toPerm a = g

Tactic:
Perm.ofSubtype g

Premises used: Equiv.Perm.ofSubtype, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 α)
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) ⋯ :
        ↥(stabilizer (Perm α) s)) =
    g
⊢ ∃ (a : ↥(stabilizer (Perm α) s)), toPerm a = g

Tactic:
use! Perm.ofSubtype g

Premises used: Equiv.Perm.ofSubtype, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
g : Perm (↑s : Type u_2)
⊢ Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (stabilizer (Perm α) s)
    ((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)

Tactic:
apply ofSubtype_mem_stabilizer

Premises used: Equiv.Perm.ofSubtype_mem_stabilizer
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
g : Perm (↑s : Type u_2)
⊢ 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) ⋯ :
        ↥(stabilizer (Perm α) s)) =
    g

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

Tactic:
classical
  use! Perm.ofSubtype g
  · apply ofSubtype_mem_stabilizer
  · aesop

Premises used: Equiv.Perm.ofSubtype_mem_stabilizer