Theorem: MulAction.top_IsBlock (Jordan/Blocks.lean)

State before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ IsBlock G ⊤
Tactic:
apply IsBlock_of_fixed
State after:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ IsFixedBlock G ⊤

State before:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ IsFixedBlock G ⊤
Tactic:
intro g
State after:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
g : G
⊢ g • ⊤ = ⊤

State before:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
g : G
⊢ g • ⊤ = ⊤
Tactic:
simp only [Set.top_eq_univ, Set.smul_set_univ]
State after:
no goals