Theorem: hasMaximalStabilizersOfPreprimitive (Jordan/Primitive.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
⊢ Subgroup.IsMaximal (stabilizer G a)
Tactic:
haveI : IsPretransitive G X := hpGX.toIsPretransitive
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
this : IsPretransitive G X
⊢ Subgroup.IsMaximal (stabilizer G a)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
this : IsPretransitive G X
⊢ Subgroup.IsMaximal (stabilizer G a)
Tactic:
rw [maximal_stabilizer_iff_preprimitive]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
this : IsPretransitive G X
⊢ IsPreprimitive G X

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
hnX : Nontrivial X
hpGX : IsPreprimitive G X
a : X
this : IsPretransitive G X
⊢ IsPreprimitive G X
Tactic:
exact hpGX
State after:
no goals