Theorem: maximal_stabilizer_iff_preprimitive (Jordan/Primitive.lean)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ Subgroup.IsMaximal (stabilizer G a) ↔ IsPreprimitive G X
Tactic:
rw [isPreprimitive_iff_isSimpleOrder_blocks G a, Subgroup.isMaximal_def, ← Set.isSimpleOrder_Ici_iff_isCoatom]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ IsSimpleOrder ↑(Set.Ici (stabilizer G a)) ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ IsSimpleOrder ↑(Set.Ici (stabilizer G a)) ↔ IsSimpleOrder { B // a ∈ B ∧ IsBlock G B }
Tactic:
simp only [isSimpleOrder_iff_isCoatom_bot]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ IsCoatom ⊥ ↔ IsCoatom ⊥

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
htGX : IsPretransitive G X
hnX : Nontrivial X
a : X
⊢ IsCoatom ⊥ ↔ IsCoatom ⊥
Tactic:
rw [← OrderIso.isCoatom_iff (stabilizerBlockEquiv G a), OrderIso.map_bot]
State after:
no goals