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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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]
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 ∈ ⊤

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

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

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

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

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

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

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