Theorem: Equiv.Perm.isPreprimitive (Jordan/MultipleTransitivity.lean)

State before:
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
⊢ IsPreprimitive (Equiv.Perm α) α
Tactic:
cases subsingleton_or_nontrivial α
State after:
case inl
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Subsingleton α
⊢ IsPreprimitive (Equiv.Perm α) α

case inr
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Nontrivial α
⊢ IsPreprimitive (Equiv.Perm α) α

State before:
case inr
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Nontrivial α
⊢ IsPreprimitive (Equiv.Perm α) α
Tactic:
apply IsMultiplyPretransitive.isPreprimitive_of_two
State after:
case inr.h2
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Nontrivial α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α 2

State before:
case inr.h2
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Nontrivial α
⊢ IsMultiplyPretransitive (Equiv.Perm α) α 2
Tactic:
apply Equiv.Perm.isMultiplyPretransitive
State after:
no goals

State before:
case inl
M : Type ?u.243758
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
h✝ : Subsingleton α
⊢ IsPreprimitive (Equiv.Perm α) α
Tactic:
exact IsPreprimitive.on_subsingleton
State after:
no goals