awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⋯
this : Membership.mem (γ := Subgroup ↥G) (stabilizer (↥G) s) h
⊢ ∃ (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))

Tactic:
⟨⟨h, this⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, 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 ⋯
this : Membership.mem (γ := Subgroup ↥G) (stabilizer (↥G) s) h
⊢ ∃ (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))

Tactic:
exact ⟨⟨h, this⟩, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
this : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
inl : ∀ (hB' : Set.Subsingleton (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)), B.Subsingleton
inr : ∀ (hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ), B.Subsingleton
⊢ B.Subsingleton

Tactic:
rcases this with hB' | hB'
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Set.Subsingleton (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
inl :
  (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 hBs, ← Subtype.image_preimage_val]

Premises used: 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 α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Set.Subsingleton (α := (↑s : Type u_2)) (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 hB'

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 α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
⊢ s ⊆ B

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
⊢ B = s

Tactic:
have hBs' : B = s := Set.Subset.antisymm hBs (by simp_all)
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)

Tactic:
subst hBs'
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst_1 : Group M
inst_2 : MulAction M α
s B : Set α
G : Subgroup M
inst_3 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
inst : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
⊢ ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton

Tactic:
subst hBs'
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst_1 : Group M
inst_2 : MulAction M α
s B : Set α
G : Subgroup M
inst_3 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
inst : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc₁ : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
⊢ stabilizer M B < G

Tactic:
subst hBs'
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst_1 : Group M
inst_2 : MulAction M α
s B : Set α
G : Subgroup M
inst_3 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
inst : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc₁ : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG₁ : stabilizer M B < G
⊢ B ⊆ B

Tactic:
subst hBs'
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst_1 : Group M
inst_2 : MulAction M α
s B : Set α
G : Subgroup M
inst_3 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
inst : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc₁ : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG₁ : stabilizer M B < G
hBs₁ : B ⊆ B
⊢ Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ

Tactic:
subst hBs'
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
inr : ∀ (g' : M) (hg' : g' ∈ G) (hg's : g' ∉ stabilizer M B), B.Subsingleton
⊢ B.Subsingleton

Tactic:
obtain ⟨g', hg', hg's⟩ := SetLike.exists_of_lt hG

Premises used: SetLike.exists_of_lt
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
⊢ _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B

Tactic:
have h := (isBlock_iff_smul_eq_or_disjoint.mp hB ⟨g', hg'⟩).resolve_left hg's
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B
this : (g' • B).Subsingleton
⊢ B.Subsingleton

Tactic:
subsingleton_of_image (MulAction.injective g') B this

Premises used: Set.subsingleton_of_image, MulAction.injective
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B
this : (g' • B).Subsingleton
⊢ B.Subsingleton

Tactic:
exact subsingleton_of_image (MulAction.injective g') B this

Premises used: Set.subsingleton_of_image, MulAction.injective
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B
inr : (g' • B).Subsingleton
⊢ B.Subsingleton

Tactic:
suffices (g' • B).Subsingleton by
        exact subsingleton_of_image (MulAction.injective g') B this
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B
inr : Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B ⊆ Bᶜ
⊢ (g' • B).Subsingleton

Tactic:
apply hB_not_le_sc (⟨g', hg'⟩ • B) (hB.translate _)

Premises used: MulAction.IsBlock.translate, HSMul.hSMul
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B ⊆ Bᶜ

Tactic:
Disjoint.subset_compl_right h

Premises used: Disjoint.subset_compl_right
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B ⊆ Bᶜ

Tactic:
exact Disjoint.subset_compl_right h

Premises used: Disjoint.subset_compl_right
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
suffices : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ B.Subsingleton

Tactic:
suffices IsTrivialBlock (Subtype.val ⁻¹' B : Set s) by
    rcases this with hB' | hB'
    · -- trivial case
      rw [← inter_eq_self_of_subset_right hBs, ← Subtype.image_preimage_val]
      apply Set.Subsingleton.image hB'
    · -- `Subtype.val ⁻¹' B = s`
      have hBs' : B = s := Set.Subset.antisymm hBs (by simp_all)
      subst hBs'
      obtain ⟨g', hg', hg's⟩ := SetLike.exists_of_lt hG
      have h := (isBlock_iff_smul_eq_or_disjoint.mp hB ⟨g', hg'⟩).resolve_left hg's
      suffices (g' • B).Subsingleton by
        exact subsingleton_of_image (MulAction.injective g') B this
      apply hB_not_le_sc (⟨g', hg'⟩ • B) (hB.translate _)
      exact Disjoint.subset_compl_right h
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
this : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
apply : IsBlock.{u_1, u_2} ↥(stabilizer (↥G) 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 α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
this : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
φ' : ↥(stabilizer (↥G) s) → ↥G :=
  Subtype.val (p := fun (x : ↥G) ↦ Membership.mem (γ := Subgroup ↥G) (stabilizer (↥G) s) x)
f' : (↑s : Type u_2) →ₑ[φ'] α := { toFun := Subtype.val (p := fun (x : α) ↦ x ∈ s), map_smul' := ⋯ }
⊢ IsBlock.{u_1, u_2} ↥(stabilizer (↥G) s) (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)

Tactic:
apply MulAction.IsBlock.preimage f' hB

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 α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
suffices : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
⊢ IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)

Tactic:
suffices IsPreprimitive (stabilizer G s) s by
    apply this.isTrivialBlock_of_isBlock
    -- `IsBlock (Subtype.val ⁻¹' B : Set s)`
    let φ' : stabilizer G s → G := Subtype.val
    let f' : s →ₑ[φ'] α := {
      toFun := Subtype.val
      map_smul' _ _ := rfl }
    apply MulAction.IsBlock.preimage f' hB
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
⊢ IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑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 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
⊢ ∃ a ∈ B, a ∈ s

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
⊢ ∃ a ∈ B, a ∈ s

Tactic:
have : ∃ a : α, a ∈ B ∧ a ∈ s := by grind
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
this : ∃ a ∈ B, a ∈ s
obtain : ∀ (a : α) (ha : a ∈ B) (ha' : a ∈ s), sᶜ ⊆ B
⊢ sᶜ ⊆ B

Tactic:
obtain ⟨a, ha, ha'⟩ := this
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
⊢ ∃ b ∈ B, b ∈ sᶜ

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
⊢ ∃ b ∈ B, b ∈ sᶜ

Tactic:
have : ∃ b : α, b ∈ B ∧ b ∈ sᶜ := by grind
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
this : ∃ b ∈ B, b ∈ sᶜ
obtain : ∀ (b : α) (hb : b ∈ B) (hb' : b ∈ sᶜ), sᶜ ⊆ B
⊢ sᶜ ⊆ B

Tactic:
obtain ⟨b, hb, hb'⟩ := this
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
this : ∃ (k : ↥(fixingSubgroup M s)), k • b = x
obtain :
  ∀ (k : M) (hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k)
    (hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ),
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ B
⊢ x ∈ B

Tactic:
obtain ⟨⟨k, hk⟩, rfl⟩ := this

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 α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
suffices : k • B = B
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ B

Tactic:
suffices k • B = B from this.le (smul_mem_smul_set hb)
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
apply : (Subtype.mk (p := fun (x : M) ↦ x ∈ G) k ⋯ • B ∩ B).Nonempty
apply₁ : k ∈ G
⊢ k • B = B

Tactic:
apply isBlock_iff_smul_eq_of_nonempty.mp hB (g := ⟨k, ?_⟩)

Premises used: Iff.mp, MulAction.isBlock_iff_smul_eq_of_nonempty
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
⊢ (Subtype.mk (p := fun (x : M) ↦ x ∈ G) k ⋯ • B ∩ B).Nonempty

Tactic:
⟨a, ?_, ha⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
refine : a ∈ Subtype.mk (p := fun (x : M) ↦ x ∈ G) k ⋯ • B
⊢ (Subtype.mk (p := fun (x : M) ↦ x ∈ G) k ⋯ • B ∩ B).Nonempty

Tactic:
refine ⟨a, ?_, ha⟩