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

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

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

State before:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
g : G
⊢ g • orbit G a = orbit G a
Tactic:
apply smul_orbit
State after:
no goals