awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
inr : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B

Tactic:
rw [← IsTrivialBlock.smul_iff g]

Premises used: MulAction.IsTrivialBlock.smul_iff
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)

Tactic:
H ⟨b, hb, hg⟩ (hB.translate g)

Premises used: And.intro, MulAction.IsBlock.translate, Exists.intro
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)

Tactic:
exact H ⟨b, hb, hg⟩ (hB.translate g)
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
⊢ ∃ (a : X), a ∉ fixedPoints G X

Tactic:
simp only [Set.top_eq_univ, Set.ne_univ_iff_exists_notMem] at Hnt

Premises used: Set.top_eq_univ, Set.ne_univ_iff_exists_notMem
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Hnt : ∃ (a : X), a ∉ fixedPoints G X
obtain : ∀ (w : X) (ha : w ∉ fixedPoints G X), IsPreprimitive G X
⊢ IsPreprimitive G X

Tactic:
obtain ⟨_, ha⟩ := Hnt
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
w : X
ha : w ∉ fixedPoints G X
⊢ IsPreprimitive G X

Tactic:
.of_isTrivialBlock_of_notMem_fixedPoints ha fun {B} _ ↦ H

Premises used: MulAction.IsPreprimitive.of_isTrivialBlock_of_notMem_fixedPoints
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
w : X
ha : w ∉ fixedPoints G X
⊢ IsPreprimitive G X

Tactic:
exact .of_isTrivialBlock_of_notMem_fixedPoints ha fun {B} _ ↦ H
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
inst_4 : IsPreprimitive M α
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : IsBlock N B
rw : IsTrivialBlock.{u_6} (X := β) (Set.image.{u_4, u_6} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' B))
⊢ IsTrivialBlock B

Tactic:
rw [← Set.image_preimage_eq B hf]

Premises used: Set.image_preimage_eq
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
inst_4 : IsPreprimitive M α
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : IsBlock N B
apply : IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
⊢ IsTrivialBlock.{u_6} (X := β) (Set.image.{u_4, u_6} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' B))

Tactic:
apply IsTrivialBlock.image hf

Premises used: MulAction.IsTrivialBlock.image
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
inst_4 : IsPreprimitive M α
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)

Tactic:
isTrivialBlock_of_isBlock (IsBlock.preimage f hB)

Premises used: MulAction.IsBlock.preimage, MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
inst_4 : IsPreprimitive M α
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)

Tactic:
exact isTrivialBlock_of_isBlock (IsBlock.preimage f hB)

Premises used: MulAction.IsBlock.preimage, MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
mp : IsPreprimitive M α → IsPreprimitive N β
mpr : IsPreprimitive N β → IsPreprimitive M α
⊢ IsPreprimitive M α ↔ IsPreprimitive N β

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPreprimitive M α
⊢ IsPreprimitive N β

Tactic:
apply IsPreprimitive.of_surjective hf.surjective

Premises used: MulAction.IsPreprimitive.of_surjective, Function.Bijective.surjective
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPreprimitive N β
⊢ IsPretransitive M α

Tactic:
haveI := (isPretransitive_congr hφ hf).mpr toIsPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
rw : IsTrivialBlock.{u_4} (X := α) (Set.preimage.{u_4, u_6} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' B))
⊢ IsTrivialBlock B

Tactic:
rw [← Set.preimage_image_eq B hf.injective]

Premises used: Function.Bijective.injective, Set.preimage_image_eq
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock.{u_4} (X := α) (Set.preimage.{u_4, u_6} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' B))

Tactic:
IsTrivialBlock.preimage hf.injective
          (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective))

Premises used: Function.Bijective.injective, MulAction.IsTrivialBlock.preimage, MulAction.IsPreprimitive.isTrivialBlock_of_isBlock, MulAction.IsBlock.image
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock.{u_4} (X := α) (Set.preimage.{u_4, u_6} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' B))

Tactic:
exact IsTrivialBlock.preimage hf.injective
          (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective))

Premises used: Function.Bijective.injective, MulAction.IsTrivialBlock.preimage, MulAction.IsPreprimitive.isTrivialBlock_of_isBlock, MulAction.IsBlock.image
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPreprimitive N β
this : IsPretransitive M α
⊢ IsPreprimitive M α

Tactic:
exact {
      isTrivialBlock_of_isBlock {B} hB := by
        rw [← Set.preimage_image_eq B hf.injective]
        exact IsTrivialBlock.preimage hf.injective
          (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective)) }
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
mp : IsSimpleOrder.{u_4} (BlockMem G a) → IsPreprimitive G X
mpr : IsPreprimitive G X → IsSimpleOrder.{u_4} (BlockMem G a)
⊢ IsSimpleOrder.{u_4} (BlockMem G a) ↔ IsPreprimitive G X

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
mp : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ IsPreprimitive G X

Tactic:
apply IsPreprimitive.of_isTrivialBlock_base a

Premises used: MulAction.IsPreprimitive.of_isTrivialBlock_base
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
mp : ∀ (hB' : Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊥), IsTrivialBlock B
mp₁ : ∀ (hB' : Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊤), IsTrivialBlock B
⊢ IsTrivialBlock B

Tactic:
rcases h_bot_or_top ⟨B, haB, hB⟩ with hB' | hB'

Premises used: Subtype.mk, And.intro
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊥
⊢ B = (↑⊥ : Set X)

Tactic:
simp only [← Subtype.coe_inj] at hB'

Premises used: Subtype.coe_inj
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊤
⊢ B = (↑⊤ : Set X)

Tactic:
simp only [← Subtype.coe_inj] at hB'

Premises used: Subtype.coe_inj
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊥ : Set X)
mp : B.Subsingleton
⊢ IsTrivialBlock B

Tactic:
left
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊥ : Set X)
mp : Set.Subsingleton.{u_4} (α := X) (↑⊥ : Set X)
⊢ B.Subsingleton

Tactic:
rw [hB']
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊥ : Set X)
⊢ Set.Subsingleton.{u_4} (α := X) (↑⊥ : Set X)

Tactic:
Set.subsingleton_singleton

Premises used: Set.subsingleton_singleton
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊥ : Set X)
⊢ Set.Subsingleton.{u_4} (α := X) (↑⊥ : Set X)

Tactic:
exact Set.subsingleton_singleton

Premises used: Set.subsingleton_singleton
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊤ : Set X)
mp : B = Set.univ
⊢ IsTrivialBlock B

Tactic:
right
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊤ : Set X)
mp : Eq.{u_4 + 1} (α := Set X) (↑⊤ : Set X) Set.univ
⊢ B = Set.univ

Tactic:
rw [hB']
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊤ : Set X)
⊢ Eq.{u_4 + 1} (α := Set X) (↑⊤ : Set X) Set.univ

Tactic:
rfl
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
hGX' : IsPreprimitive G X
mpr : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤
⊢ IsSimpleOrder.{u_4} (BlockMem G a)

Tactic:
apply IsSimpleOrder.mk

Premises used: IsSimpleOrder.mk
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
mpr : B = (↑⊥ : Set X) ∨ B = (↑⊤ : Set X)
⊢ Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊥ ∨
    Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊤

Tactic:
simp only [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : B.Subsingleton
⊢ B = (↑⊥ : Set X) ∨ B = (↑⊤ : Set X)

Tactic:
simp [BlockMem.coe_bot, h.eq_singleton_of_mem haB]

Premises used: Set.Subsingleton.eq_singleton_of_mem, MulAction.BlockMem.coe_bot
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : B = Set.univ
⊢ B = (↑⊥ : Set X) ∨ B = (↑⊤ : Set X)

Tactic:
simp [BlockMem.coe_top, h]

Premises used: MulAction.BlockMem.coe_top
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ IsTrivialBlock B

Tactic:
cases hGX'.isTrivialBlock_of_isBlock hB with
    | inl h =>
      simp [BlockMem.coe_bot, h.eq_singleton_of_mem haB]
    | inr h =>
      simp [BlockMem.coe_top, h]

Premises used: MulAction.BlockMem.coe_top, MulAction.BlockMem.coe_bot, MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
rw : IsSimpleOrder.{u_3} (↑(Set.Ici (stabilizer G a)) : Type u_3) ↔ IsSimpleOrder.{u_4} (BlockMem G a)
⊢ IsCoatom (α := Subgroup G) (stabilizer G a) ↔ IsPreprimitive G X

Tactic:
rw [← isSimpleOrder_blockMem_iff_isPreprimitive G a, ← Set.isSimpleOrder_Ici_iff_isCoatom]

Premises used: MulAction.isSimpleOrder_blockMem_iff_isPreprimitive, Set.isSimpleOrder_Ici_iff_isCoatom
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
simp : IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔ IsCoatom.{u_4} (α := BlockMem G a) ⊥
⊢ IsSimpleOrder.{u_3} (↑(Set.Ici (stabilizer G a)) : Type u_3) ↔ IsSimpleOrder.{u_4} (BlockMem G a)

Tactic:
simp only [isSimpleOrder_iff_isCoatom_bot]

Premises used: isSimpleOrder_iff_isCoatom_bot
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
rw :
  IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔
    IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3))
      (((block_stabilizerOrderIso G a :
            OrderIso.{u_4, u_3} { B : Set X // a ∈ B ∧ IsBlock G B } (↑(Set.Ici (stabilizer G a)) : Type u_3)) :
          (a_1 : { B : Set X // a ∈ B ∧ IsBlock G B }) → (↑(Set.Ici (stabilizer G a)) : Type u_3))
        ⊥)
rw₁ rw₂ :
  IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔
    IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥
⊢ IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔ IsCoatom.{u_4} (α := BlockMem G a) ⊥

Tactic:
rw [← OrderIso.isCoatom_iff (block_stabilizerOrderIso G a), OrderIso.map_bot]

Premises used: OrderIso.isCoatom_iff, MulAction.block_stabilizerOrderIso, OrderIso.map_bot
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : Nontrivial X
inst_3 : IsPreprimitive G X
a : X
rwa rwa₁ rwa₂ rwa₃ : IsPreprimitive G X
⊢ IsCoatom (α := Subgroup G) (stabilizer G a)

Tactic:
rwa [isCoatom_stabilizer_iff_preprimitive]

Premises used: MulAction.isCoatom_stabilizer_iff_preprimitive
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h : N.Normal
hNX : fixedPoints.{u_3, u_4} (↥N) α ≠ Set.univ
⊢ ∃ (a : α), a ∉ fixedPoints.{u_3, u_4} (↥N) α

Tactic:
rw [Set.ne_univ_iff_exists_notMem] at hNX

Premises used: Set.ne_univ_iff_exists_notMem
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h : N.Normal
hNX : ∃ (a : α), a ∉ fixedPoints.{u_3, u_4} (↥N) α
obtain : ∀ (a : α) (ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α), IsPretransitive.{u_3, u_4} (↥N) α
⊢ IsPretransitive.{u_3, u_4} (↥N) α

Tactic:
obtain ⟨a, ha⟩ := hNX
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
rw : orbit.{u_3, u_4} (↥N) a = Set.univ
⊢ IsPretransitive.{u_3, u_4} (↥N) α

Tactic:
rw [isPretransitive_iff_orbit_eq_univ a]

Premises used: MulAction.isPretransitive_iff_orbit_eq_univ
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
apply : ¬(orbit.{u_3, u_4} (↥N) a).Subsingleton
⊢ orbit.{u_3, u_4} (↥N) a = Set.univ

Tactic:
apply Or.resolve_left (isTrivialBlock_of_isBlock (IsBlock.orbit_of_normal a))

Premises used: MulAction.IsBlock.orbit_of_normal, Or.resolve_left, MulAction.IsPreprimitive.isTrivialBlock_of_isBlock
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
apply : a ∈ fixedPoints.{u_3, u_4} (↥N) α
⊢ False

Tactic:
apply ha
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
this : orbit.{u_3, u_4} (↥N) a = {a}
rw : n • a ∈ orbit.{u_3, u_4} (↥N) a
⊢ Membership.mem (γ := Set α) {a} (n • a)

Tactic:
rw [← this]
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
this : orbit.{u_3, u_4} (↥N) a = {a}
w : ↥N
h₁ : (fun (m : ↥N) ↦ m • a) n = n • a
⊢ n • a ∈ orbit.{u_3, u_4} (↥N) a

Tactic:
use n
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
suffices : orbit.{u_3, u_4} (↥N) a = {a}
⊢ Membership.mem (γ := Set α) {a} (n • a)

Tactic:
suffices orbit N a = {a} by rw [← this]; use n
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
h₁ : ∀ (b : α), b ∈ orbit.{u_3, u_4} (↥N) a ↔ Membership.mem (γ := Set α) {a} b
⊢ orbit.{u_3, u_4} (↥N) a = {a}

Tactic:
ext b
-- Module: Mathlib.GroupTheory.GroupAction.Primitive
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
M : Type u_3
inst_2 : Group M
α : Type u_4
inst_3 : MulAction M α
inst_4 : IsPreprimitive M α
N : Subgroup M
h_1 : N.Normal
a : α
ha : a ∉ fixedPoints.{u_3, u_4} (↥N) α
h : (orbit.{u_3, u_4} (↥N) a).Subsingleton
n : ↥N
b : α
h₁ h₂ : Membership.mem (γ := Set α) {a} b ↔ Membership.mem (γ := Set α) {a} b
⊢ b ∈ orbit.{u_3, u_4} (↥N) a ↔ Membership.mem (γ := Set α) {a} b

Tactic:
rw [Set.Subsingleton.eq_singleton_of_mem h (MulAction.mem_orbit_self a)]

Premises used: Set.Subsingleton.eq_singleton_of_mem, MulAction.mem_orbit_self