internlm/Lean-Github huggingface dataset:
Theorem: IsPreprimitive.mk_mem
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ IsPreprimitive G X
Tactic:
apply IsPreprimitive.mk
Proof state after:
case has_trivial_blocks'
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Tactic:
intro B hB
Proof state after:
case has_trivial_blocks'
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
⊢ IsTrivialBlock B
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
⊢ IsTrivialBlock B
Tactic:
cases Set.eq_empty_or_nonempty B with
| inl h => apply Or.intro_left; rw [h]; exact Set.subsingleton_empty
| inr h =>
  obtain ⟨b, hb⟩ := h
  obtain ⟨g, hg⟩ := exists_smul_eq G b a
  rw [isTrivialBlock_of_block_iff g]
  refine' H (g • B) _ (IsBlock_of_block g hB)
  use b
Proof state after:
no goals
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'.inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
h : B = ∅
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_left
Proof state after:
case has_trivial_blocks'.inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
h : B = ∅
⊢ Set.Subsingleton B
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'.inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
h : B = ∅
⊢ Set.Subsingleton B
Tactic:
rw [h]
Proof state after:
case has_trivial_blocks'.inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
h : B = ∅
⊢ Set.Subsingleton ∅
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'.inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
h : B = ∅
⊢ Set.Subsingleton ∅
Tactic:
exact Set.subsingleton_empty
Proof state after:
no goals
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'.inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
h : Set.Nonempty B
⊢ IsTrivialBlock B
Tactic:
obtain ⟨b, hb⟩ := h
Proof state after:
case has_trivial_blocks'.inr.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
⊢ IsTrivialBlock B
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'.inr.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
⊢ IsTrivialBlock B
Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq G b a
Proof state after:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock B
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock B
Tactic:
rw [isTrivialBlock_of_block_iff g]
Proof state after:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)
Tactic:
refine' H (g • B) _ (IsBlock_of_block g hB)
Proof state after:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ a ∈ g • B
Theorem: IsPreprimitive.mk_mem
Proof state before:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
htGX : IsPretransitive G X
a : X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ a ∈ g • B
Tactic:
use b
Proof state after:
no goals
Theorem: IsPreprimitive.mk_mem'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
⊢ IsPreprimitive G X
Tactic:
apply IsPreprimitive.mk
Proof state after:
case has_trivial_blocks'
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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}, IsBlock G B → IsTrivialBlock B
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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}, IsBlock G B → IsTrivialBlock B
Tactic:
intro B hB
Proof state after:
case has_trivial_blocks'
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
⊢ IsTrivialBlock B
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
⊢ IsTrivialBlock B
Tactic:
cases Set.eq_empty_or_nonempty B with
| inl h => left; rw [h]; exact Set.subsingleton_empty
| inr h =>
  obtain ⟨b, hb⟩ := h
  obtain ⟨g, hg⟩ := exists_smul_eq G b a
  rw [isTrivialBlock_of_block_iff g]
  refine' H (g • B) _ (IsBlock_of_block g hB)
  use b
Proof state after:
no goals
Theorem: IsPreprimitive.mk_mem'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ IsPretransitive G X
Tactic:
apply IsPretransitive.mk_base a
Proof state after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ ∀ (x : X), ∃ g, g • a = x
Theorem: IsPreprimitive.mk_mem'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ ∀ (x : X), ∃ g, g • a = x
Tactic:
cases' H (orbit G a) (mem_orbit_self a) (IsBlock_of_orbit a) with H H
Proof state after:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : Set.Subsingleton (orbit G a)
⊢ ∀ (x : X), ∃ g, g • a = x

case inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = ⊤
⊢ ∀ (x : X), ∃ g, g • a = x
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : Set.Subsingleton (orbit G a)
⊢ ∀ (x : X), ∃ g, g • a = x
Tactic:
exfalso
Proof state after:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : Set.Subsingleton (orbit G a)
⊢ False
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : Set.Subsingleton (orbit G a)
⊢ False
Tactic:
apply ha
Proof state after:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : Set.Subsingleton (orbit G a)
⊢ a ∈ fixedPoints G X
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : Set.Subsingleton (orbit G a)
⊢ a ∈ fixedPoints G X
Tactic:
rw [Set.subsingleton_iff_singleton (mem_orbit_self a)] at H
Proof state after:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
⊢ a ∈ fixedPoints G X
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
⊢ a ∈ fixedPoints G X
Tactic:
simp only [mem_fixedPoints]
Proof state after:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
⊢ ∀ (m : G), m • a = a
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
⊢ ∀ (m : G), m • a = a
Tactic:
intro g
Proof state after:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a = a
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a = a
Tactic:
rw [← Set.mem_singleton_iff]
Proof state after:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ {a}
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ {a}
Tactic:
rw [← H]
Proof state after:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ orbit G a
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ g • a ∈ orbit G a
Tactic:
exact mem_orbit a g
Proof state after:
no goals
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = ⊤
⊢ ∀ (x : X), ∃ g, g • a = x
Tactic:
intro x
Proof state after:
case inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = ⊤
x : X
⊢ ∃ g, g • a = x
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = ⊤
x : X
⊢ ∃ g, g • a = x
Tactic:
rw [← MulAction.mem_orbit_iff, H]
Proof state after:
case inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = ⊤
x : X
⊢ x ∈ ⊤
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = ⊤
x : X
⊢ x ∈ ⊤
Tactic:
exact Set.mem_univ x
Proof state after:
no goals
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'.inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
h : B = ∅
⊢ IsTrivialBlock B
Tactic:
left
Proof state after:
case has_trivial_blocks'.inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
h : B = ∅
⊢ Set.Subsingleton B
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'.inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
h : B = ∅
⊢ Set.Subsingleton B
Tactic:
rw [h]
Proof state after:
case has_trivial_blocks'.inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
h : B = ∅
⊢ Set.Subsingleton ∅
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'.inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
h : B = ∅
⊢ Set.Subsingleton ∅
Tactic:
exact Set.subsingleton_empty
Proof state after:
no goals
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'.inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
h : Set.Nonempty B
⊢ IsTrivialBlock B
Tactic:
obtain ⟨b, hb⟩ := h
Proof state after:
case has_trivial_blocks'.inr.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
⊢ IsTrivialBlock B
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'.inr.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
⊢ IsTrivialBlock B
Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq G b a
Proof state after:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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 B
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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 B
Tactic:
rw [isTrivialBlock_of_block_iff g]
Proof state after:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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)
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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:
refine' H (g • B) _ (IsBlock_of_block g hB)
Proof state after:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
⊢ a ∈ g • B
Theorem: IsPreprimitive.mk_mem'
Proof state before:
case has_trivial_blocks'.inr.intro.intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : 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
⊢ a ∈ g • B
Tactic:
use b
Proof state after:
no goals
Theorem: IsPreprimitive.mk'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
⊢ IsPreprimitive G X
Tactic:
have : ∃ a : X, a ∉ fixedPoints G X := by
  by_contra h; push_neg at h ; apply Hnt; rw [eq_top_iff]
  intro a _; exact h a
Proof state after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
this : ∃ a, a ∉ fixedPoints G X
⊢ IsPreprimitive G X
Theorem: IsPreprimitive.mk'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
this : ∃ a, a ∉ fixedPoints G X
⊢ IsPreprimitive G X
Tactic:
obtain ⟨a, ha⟩ := this
Proof state after:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
⊢ IsPreprimitive G X
Theorem: IsPreprimitive.mk'
Proof state before:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
⊢ IsPreprimitive G X
Tactic:
apply IsPreprimitive.mk_mem' a ha
Proof state after:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
⊢ ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
Theorem: IsPreprimitive.mk'
Proof state before:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
⊢ ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
Tactic:
intro B _
Proof state after:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
B : Set X
x✝ : a ∈ B
⊢ IsBlock G B → IsTrivialBlock B
Theorem: IsPreprimitive.mk'
Proof state before:
case intro
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
a : X
ha : a ∉ fixedPoints G X
B : Set X
x✝ : a ∈ B
⊢ IsBlock G B → IsTrivialBlock B
Tactic:
exact H B
Proof state after:
no goals
Theorem: IsPreprimitive.mk'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
⊢ ∃ a, a ∉ fixedPoints G X
Tactic:
by_contra h
Proof state after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ¬∃ a, a ∉ fixedPoints G X
⊢ False
Theorem: IsPreprimitive.mk'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ¬∃ a, a ∉ fixedPoints G X
⊢ False
Tactic:
push_neg at h
Proof state after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ False
Theorem: IsPreprimitive.mk'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ False
Tactic:
apply Hnt
Proof state after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ fixedPoints G X = ⊤
Theorem: IsPreprimitive.mk'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ fixedPoints G X = ⊤
Tactic:
rw [eq_top_iff]
Proof state after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ ⊤ ≤ fixedPoints G X
Theorem: IsPreprimitive.mk'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
⊢ ⊤ ≤ fixedPoints G X
Tactic:
intro a _
Proof state after:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
a : X
a✝ : a ∈ ⊤
⊢ a ∈ fixedPoints G X
Theorem: IsPreprimitive.mk'
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ (B : Set X), IsBlock G B → IsTrivialBlock B
h : ∀ (a : X), a ∈ fixedPoints G X
a : X
a✝ : a ∈ ⊤
⊢ a ∈ fixedPoints G X
Tactic:
exact h a
Proof state after:
no goals