awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
out : Nat.Prime (Nat.card.{u_2} (Perm α))
⊢ Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))

Tactic:
apply Fact.mk

Premises used: Fact.mk
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
out : Nat.Prime 2
⊢ Nat.Prime (Nat.card.{u_2} (Perm α))

Tactic:
rw [Nat.card_perm, hα, Nat.factorial_two]

Premises used: Nat.card_perm, Nat.factorial_two
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
⊢ Nat.Prime 2

Tactic:
Nat.prime_two

Premises used: Nat.prime_two
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
⊢ Nat.Prime 2

Tactic:
exact Nat.prime_two

Premises used: Nat.prime_two
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
⊢ Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))

Tactic:
have hα2 : Fact (Nat.card (Perm α)).Prime := by
    apply Fact.mk
    rw [Nat.card_perm, hα, Nat.factorial_two]
    exact Nat.prime_two
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h_1 : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
h : G = ⊥
inr : False
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

Tactic:
exfalso
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h_1 : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
h : G = ⊥
⊢ False

Tactic:
ne_bot_of_gt hG h

Premises used: ne_bot_of_gt
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h_1 : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
h : G = ⊥
⊢ False

Tactic:
exact ne_bot_of_gt hG h

Premises used: ne_bot_of_gt
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h_1 : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
h : G = ⊤
inr : ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) (α := Set α) univ) g
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

Tactic:
rw [h, ← stabilizer_univ_eq_top (Perm α) α]

Premises used: Equiv.Perm, stabilizer_univ_eq_top
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h_1 : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
h : G = ⊤
inr : 1 < encard.{u_2} (α := α) univ
⊢ ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) (α := Set α) univ) g

Tactic:
apply this
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h_1 : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
h : G = ⊤
⊢ 1 < encard.{u_2} (α := α) univ

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
⊢ G = ⊥ ∨ G = ⊤

Tactic:
cases G.eq_bot_or_eq_top_of_prime_card with
  | inl h =>
    exfalso; exact ne_bot_of_gt hG h
  | inr h =>
    rw [h, ← stabilizer_univ_eq_top (Perm α) α]
    apply this
    simp_all

Premises used: Subgroup.eq_bot_or_eq_top_of_prime_card, Equiv.Perm, stabilizer_univ_eq_top
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : ↥G), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : ↥G), g • a = b
hM : Ne.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
⊢ IsPretransitive.{u_1, u_2} (↥G) α

Tactic:
apply IsPretransitive.of_partition (s := s)

Premises used: MulAction.IsPretransitive.of_partition
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hs :
  ∀ (g : M) (hg : Membership.mem (γ := Subgroup M) (stabilizer M s) g) (hb : g • a ∈ s), ∃ (g_1 : ↥G), g_1 • a = g • a
⊢ ∃ (g : ↥G), g • a = b

Tactic:
obtain ⟨g, hg, rfl⟩ := moves a ha b hb

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ s
g : M
hg : Membership.mem (γ := Subgroup M) (stabilizer M s) g
hb : g • a ∈ s
⊢ ∃ (g_1 : ↥G), g_1 • a = g • a

Tactic:
⟨⟨g, hG.le hg⟩, rfl⟩

Premises used: LT.lt.le, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ s
g : M
hg : Membership.mem (γ := Subgroup M) (stabilizer M s) g
hb : g • a ∈ s
⊢ ∃ (g_1 : ↥G), g_1 • a = g • a

Tactic:
exact ⟨⟨g, hG.le hg⟩, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hs' :
  ∀ (g : M) (hg : Membership.mem (γ := Subgroup M) (stabilizer M sᶜ) g) (hb : g • a ∈ sᶜ), ∃ (g_1 : ↥G), g_1 • a = g • a
⊢ ∃ (g : ↥G), g • a = b

Tactic:
obtain ⟨g, hg, rfl⟩ := moves a ha b hb

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ sᶜ
g : M
hg : Membership.mem (γ := Subgroup M) (stabilizer M sᶜ) g
hb : g • a ∈ sᶜ
⊢ Membership.mem (γ := Subgroup M) (stabilizer M s) g

Tactic:
rw [stabilizer_compl] at hg

Premises used: stabilizer_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ sᶜ
g : M
hg : Membership.mem (γ := Subgroup M) (stabilizer M sᶜ) g
hb : g • a ∈ sᶜ
hg₁ : Membership.mem (γ := Subgroup M) (stabilizer M s) g
⊢ g • a ∈ sᶜ

Tactic:
rw [stabilizer_compl] at hg

Premises used: stabilizer_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ sᶜ
g : M
hg : Membership.mem (γ := Subgroup M) (stabilizer M s) g
hb : g • a ∈ sᶜ
⊢ ∃ (g_1 : ↥G), g_1 • a = g • a

Tactic:
⟨⟨g, hG.le hg⟩, rfl⟩

Premises used: LT.lt.le, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ sᶜ
g : M
hg : Membership.mem (γ := Subgroup M) (stabilizer M s) g
hb : g • a ∈ sᶜ
⊢ ∃ (g_1 : ↥G), g_1 • a = g • a

Tactic:
exact ⟨⟨g, hG.le hg⟩, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hM : ∀ (hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤), ¬stabilizer M s < G
⊢ Ne.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤

Tactic:
contrapose hG
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
hM : G ≤ stabilizer M s
⊢ ¬stabilizer M s < G

Tactic:
apply not_lt_of_ge

Premises used: not_lt_of_ge
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
rw : G = G.subtype.range
rw₁ rw₂ : G = G
⊢ G = Subgroup.map G.subtype ⊤

Tactic:
rw [← MonoidHom.range_eq_map, Subgroup.range_subtype]

Premises used: MonoidHom.range_eq_map, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
⊢ G = Subgroup.map G.subtype ⊤

Tactic:
have : G = Subgroup.map G.subtype ⊤ := by
      rw [← MonoidHom.range_eq_map, Subgroup.range_subtype]
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
this : G = Subgroup.map G.subtype ⊤
hM : ⊤ ≤ Subgroup.comap G.subtype (stabilizer M s)
⊢ G ≤ stabilizer M s

Tactic:
rw [this, Subgroup.map_le_iff_le_comap]

Premises used: Subgroup.map_le_iff_le_comap
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
this : G = Subgroup.map G.subtype ⊤
hM : LE.le.{u_1} (α := Subgroup ↥G) ⊤ (stabilizer (↥G) s)
hM₁ hM₂ : LE.le.{u_1} (α := Subgroup ↥G) ⊤ ⊤
⊢ ⊤ ≤ Subgroup.comap G.subtype (stabilizer M s)

Tactic:
rw [show Subgroup.comap G.subtype (stabilizer M s) = stabilizer G s from rfl, hG]

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
rw :
  (Set.image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)).Subsingleton
⊢ B.Subsingleton

Tactic:
rw [← inter_eq_self_of_subset_right (subset_of_ssubset hB_ss_sc), ← Subtype.image_preimage_val]

Premises used: subset_of_ssubset, Subtype.image_preimage_val, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
hs : Set.Subsingleton (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ (Set.image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)).Subsingleton

Tactic:
apply Set.Subsingleton.image

Premises used: Set.Subsingleton.image
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
apply : ¬Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
⊢ Set.Subsingleton (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)

Tactic:
apply Or.resolve_right this

Premises used: Or.resolve_right
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
rw : ¬{x : α | x ∈ s} ⊆ B
⊢ ¬Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ

Tactic:
rw [preimage_eq_univ_iff, Subtype.range_coe_subtype]

Premises used: Set.preimage_eq_univ_iff, Subtype.range_coe_subtype
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ ¬{x : α | x ∈ s} ⊆ B

Tactic:
not_subset_of_ssubset hB_ss_sc

Premises used: not_subset_of_ssubset
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ ¬{x : α | x ∈ s} ⊆ B

Tactic:
exact not_subset_of_ssubset hB_ss_sc

Premises used: not_subset_of_ssubset
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
hs : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ Set.Subsingleton (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)

Tactic:
suffices IsTrivialBlock (Subtype.val ⁻¹' B : Set (s : Set α)) by
    apply Or.resolve_right this
    rw [preimage_eq_univ_iff, Subtype.range_coe_subtype]
    exact not_subset_of_ssubset hB_ss_sc
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)
apply : IsBlock.{u_1, u_2} ↥(stabilizer M s) (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)

Tactic:
apply this.isTrivialBlock_of_isBlock

Premises used: MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)
φ' : ↥(stabilizer M s) → M := Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M s) x)
f' : (↑s : Type u_2) →ₑ[φ'] α := { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ s), map_smul' := ⋯ }
⊢ IsBlock.{u_1, u_2} ↥(stabilizer M s) (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)

Tactic:
hB.preimage f'

Premises used: MulAction.IsBlock.preimage
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)
φ' : ↥(stabilizer M s) → M := Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (stabilizer M s) x)
f' : (↑s : Type u_2) →ₑ[φ'] α := { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ s), map_smul' := ⋯ }
⊢ IsBlock.{u_1, u_2} ↥(stabilizer M s) (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)

Tactic:
exact hB.preimage f'

Premises used: MulAction.IsBlock.preimage
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
hs : IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)
⊢ IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)

Tactic:
suffices IsPreprimitive (stabilizer M (s : Set α)) (s : Set α) by
    apply this.isTrivialBlock_of_isBlock
    let φ' : stabilizer M (s : Set α) → M := Subtype.val
    let f' : (s : Set α) →ₑ[φ'] α := {
      toFun := Subtype.val
      map_smul' _ _ := rfl }
    exact hB.preimage f'
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)

Tactic:
isPreprimitive_stabilizer_of_surjective _ hG

Premises used: MulAction.isPreprimitive_stabilizer_of_surjective
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)

Tactic:
exact isPreprimitive_stabilizer_of_surjective _ hG

Premises used: MulAction.isPreprimitive_stabilizer_of_surjective
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
apply : Function.Surjective.{u_2 + 1, u_2 + 1} (α := ↥(stabilizer (↥G) s)) (β := Perm (↑s : Type u_2)) toPerm
⊢ B.Subsingleton

Tactic:
apply hB.subsingleton_of_ssubset_of_stabilizer_le hB_ss_sc

Premises used: MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_le
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
g : Perm (↑s : Type u_2)
obtain :
  ∀ (k : Perm α) (hk : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) k),
    ∃ (a : ↥(stabilizer (↥G) s)),
      Eq (α := Perm (↑s : Type u_2)) (toPerm a)
        (toPerm
          (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) x) k hk))
⊢ ∃ (a : ↥(stabilizer (↥G) s)), toPerm a = g

Tactic:
obtain ⟨⟨k, hk⟩, rfl⟩ := stabilizer.surjective_toPerm s g

Premises used: Equiv.Perm.stabilizer.surjective_toPerm, rfl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
k : Perm α
hk : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) k
h : ↥G := Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) k ⋯
⊢ Membership.mem (γ := Subgroup ↥G) (stabilizer (↥G) s) h

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
k : Perm α
hk : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) k
h : ↥G := Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) k ⋯
⊢ Membership.mem (γ := Subgroup ↥G) (stabilizer (↥G) s) h

Tactic:
have : h ∈ stabilizer G s := by aesop