Theorem: MulAction.isMultiplyPreprimitive_zero (Jordan/MultiplePrimitivity.lean)

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPreprimitive M α 0
Tactic:
constructor
State after:
case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPretransitive M α 0

case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑0 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPretransitive M α 0
Tactic:
apply MulAction.is_zero_pretransitive
State after:
no goals

State before:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑0 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
intro s
State after:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
⊢ Set.encard s + 1 = ↑0 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
⊢ Set.encard s + 1 = ↑0 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
simp
State after:
no goals