Theorem: isTrivialBlock_of_block (Jordan/Primitive.lean)

State before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : IsTrivialBlock B
⊢ IsTrivialBlock (g • B)
Tactic:
cases hB with
| inl hB =>
  left
  apply Set.Subsingleton.image hB
| inr hB =>
  apply Or.intro_right
  rw [hB, eq_top_iff]
  intro x _
  rw [Set.mem_smul_set_iff_inv_smul_mem]
  exact Set.mem_univ _
State after:
no goals

State before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : Set.Subsingleton B
⊢ IsTrivialBlock (g • B)
Tactic:
left
State after:
case inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : Set.Subsingleton B
⊢ Set.Subsingleton (g • B)

State before:
case inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : Set.Subsingleton B
⊢ Set.Subsingleton (g • B)
Tactic:
apply Set.Subsingleton.image hB
State after:
no goals

State before:
case inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ IsTrivialBlock (g • B)
Tactic:
apply Or.intro_right
State after:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ g • B = ⊤

State before:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ g • B = ⊤
Tactic:
rw [hB, eq_top_iff]
State after:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ ⊤ ≤ g • ⊤

State before:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ ⊤ ≤ g • ⊤
Tactic:
intro x _
State after:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
x : X
a✝ : x ∈ ⊤
⊢ x ∈ g • ⊤

State before:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
x : X
a✝ : x ∈ ⊤
⊢ x ∈ g • ⊤
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem]
State after:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
x : X
a✝ : x ∈ ⊤
⊢ g⁻¹ • x ∈ ⊤

State before:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
x : X
a✝ : x ∈ ⊤
⊢ g⁻¹ • x ∈ ⊤
Tactic:
exact Set.mem_univ _
State after:
no goals