Theorem: IsPreprimitive.mk_mem (Jordan/Primitive.lean)

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
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

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
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

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
State after:
no goals

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
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

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]
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 ∅

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
State after:
no goals

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
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

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
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

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]
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)

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)
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

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
State after:
no goals