internlm/Lean-Github huggingface dataset:
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α
Tactic:
intro hN
Proof state after:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
⊢ IsPreprimitive M α
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
⊢ IsPreprimitive M α
Tactic:
haveI := (isPretransitive.of_bijective_map_iff hφ hf).mpr hN.toIsPretransitive
Proof state after:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
⊢ IsPreprimitive M α
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mpr
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
⊢ IsPreprimitive M α
Tactic:
apply IsPreprimitive.mk
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Tactic:
intro B hB
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Tactic:
rw [← Set.preimage_image_eq B hf.injective]
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f ⁻¹' (⇑f '' B))
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f ⁻¹' (⇑f '' B))
Tactic:
apply isTrivialBlock_of_injective_map hf.injective
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f '' B)
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock (⇑f '' B)
Tactic:
apply hN.has_trivial_blocks
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsBlock N (⇑f '' B)
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsBlock N (⇑f '' B)
Tactic:
apply IsBlock_image f hφ hf.injective
Proof state after:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsBlock M B
Theorem: isPreprimitive_of_bijective_map_iff'
Proof state before:
case mpr.has_trivial_blocks'
M : Type u_4
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
N : Type u_3
β : Type u_1
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsBlock M B
Tactic:
exact hB
Proof state after:
no goals
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ Nontrivial { B // a ∈ B ∧ IsBlock G B }
Tactic:
rw [nontrivial_iff]
Proof state after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ∃ x y, x ≠ y
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ∃ x y, x ≠ y
Tactic:
use (Block.boundedOrderOfMem G a).bot
Proof state after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ∃ y, ⊥ ≠ y
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ∃ y, ⊥ ≠ y
Tactic:
use (Block.boundedOrderOfMem G a).top
Proof state after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ⊥ ≠ ⊤
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
⊢ ⊥ ≠ ⊤
Tactic:
intro h
Proof state after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : ⊥ = ⊤
⊢ False
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : ⊥ = ⊤
⊢ False
Tactic:
rw [← Subtype.coe_inj] at h
Proof state after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : ↑⊥ = ↑⊤
⊢ False
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : ↑⊥ = ↑⊤
⊢ False
Tactic:
simp only [Block.boundedOrderOfMem.top_eq, Block.boundedOrderOfMem.bot_eq] at h
Proof state after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
⊢ False
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
⊢ False
Tactic:
obtain ⟨b, hb⟩ := exists_ne a
Proof state after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ False
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ False
Tactic:
apply hb
Proof state after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b = a
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b = a
Tactic:
rw [← Set.mem_singleton_iff]
Proof state after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ {a}
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ {a}
Tactic:
rw [h]
Proof state after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ ⊤
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ ⊤
Tactic:
rw [Set.top_eq_univ]
Proof state after:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ Set.univ
Theorem: Block.mem_is_nontrivial_order_of_nontrivial
Proof state before:
case h.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : Nontrivial X
a : X
h : {a} = ⊤
b : X
hb : b ≠ a
⊢ b ∈ Set.univ
Tactic:
apply Set.mem_univ
Proof state after:
no goals
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsPreprimitive G X ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
haveI : Nontrivial { B : Set X // a ∈ B ∧ IsBlock G B } :=
  Block.mem_is_nontrivial_order_of_nontrivial G a
Proof state after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
constructor
Proof state after:
case mp
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X → IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }

case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B } → IsPreprimitive G X
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X → IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
intro hGX'
Proof state after:
case mp
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
⊢ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
⊢ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
apply IsSimpleOrder.mk
Proof state after:
case mp.eq_bot_or_eq_top
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
⊢ ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp.eq_bot_or_eq_top
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
⊢ ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤
Tactic:
rintro ⟨B, haB, hB⟩
Proof state after:
case mp.eq_bot_or_eq_top.mk.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ { val := B, property := ⋯ } = ⊥ ∨ { val := B, property := ⋯ } = ⊤
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp.eq_bot_or_eq_top.mk.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ { val := B, property := ⋯ } = ⊥ ∨ { val := B, property := ⋯ } = ⊤
Tactic:
simp only [← Subtype.coe_inj, Subtype.coe_mk]
Proof state after:
case mp.eq_bot_or_eq_top.mk.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ B = ↑⊥ ∨ B = ↑⊤
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp.eq_bot_or_eq_top.mk.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ B = ↑⊥ ∨ B = ↑⊤
Tactic:
cases hGX'.has_trivial_blocks hB with
| inl h =>
  apply Or.intro_left
  change B = ↑(Block.boundedOrderOfMem G a).bot
  rw [Block.boundedOrderOfMem.bot_eq]
  exact Set.Subsingleton.eq_singleton_of_mem h haB
| inr h =>
  apply Or.intro_right
  change B = ↑(Block.boundedOrderOfMem G a).top
  exact h
Proof state after:
no goals
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp.eq_bot_or_eq_top.mk.intro.inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = ↑⊥ ∨ B = ↑⊤
Tactic:
apply Or.intro_left
Proof state after:
case mp.eq_bot_or_eq_top.mk.intro.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = ↑⊥
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp.eq_bot_or_eq_top.mk.intro.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = ↑⊥
Tactic:
rw [Block.boundedOrderOfMem.bot_eq]
Proof state after:
case mp.eq_bot_or_eq_top.mk.intro.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = {a}
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp.eq_bot_or_eq_top.mk.intro.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : Set.Subsingleton B
⊢ B = {a}
Tactic:
exact Set.Subsingleton.eq_singleton_of_mem h haB
Proof state after:
no goals
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp.eq_bot_or_eq_top.mk.intro.inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : B = ⊤
⊢ B = ↑⊥ ∨ B = ↑⊤
Tactic:
apply Or.intro_right
Proof state after:
case mp.eq_bot_or_eq_top.mk.intro.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : B = ⊤
⊢ B = ↑⊤
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mp.eq_bot_or_eq_top.mk.intro.inr.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : B = ⊤
⊢ B = ↑⊤
Tactic:
exact h
Proof state after:
no goals
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
⊢ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B } → IsPreprimitive G X
Tactic:
intro h
Proof state after:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
⊢ IsPreprimitive G X
Tactic:
let h_bot_or_top := h.eq_bot_or_eq_top
Proof state after:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ IsPreprimitive G X
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ IsPreprimitive G X
Tactic:
apply IsPreprimitive.mk_mem a
Proof state after:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ ∀ (B : Set X), a ∈ B → IsBlock G B → IsTrivialBlock B
Tactic:
intro B haB hB
Proof state after:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ IsTrivialBlock B
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ IsTrivialBlock B
Tactic:
cases' h_bot_or_top ⟨B, haB, hB⟩ with hB' hB' <;>
  simp only [← Subtype.coe_inj, Subtype.coe_mk] at hB'
Proof state after:
case mpr.inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ IsTrivialBlock B

case mpr.inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ IsTrivialBlock B
Theorem: isPreprimitive_iff_isSimpleOrder_blocks
Proof state before:
case mpr.inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ IsTrivialBlock B
Tactic:
left
Proof state after:
case mpr.inl.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
htGX : IsPretransitive G X
inst✝ : Nontrivial X
a : X
this : Nontrivial { B // a ∈ B ∧ IsBlock G B }
h : IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
h_bot_or_top : ∀ (a_1 : { B // a ∈ B ∧ IsBlock G B }), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ Set.Subsingleton B