Theorem: MulAction.AlternatingGroup.isPreprimitive (Jordan/MultipleTransitivity.lean)

State before:
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Tactic:
have := alternatingGroup.isPretransitive h
State after:
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ IsPreprimitive (↥(alternatingGroup α)) α

State before:
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Tactic:
apply IsPreprimitive.mk
State after:
case has_trivial_blocks'
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ ∀ {B : Set α}, IsBlock (↥(alternatingGroup α)) B → IsTrivialBlock B

State before:
case has_trivial_blocks'
M : Type ?u.309192
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ ∀ {B : Set α}, IsBlock (↥(alternatingGroup α)) B → IsTrivialBlock B
Tactic:
apply alternatingGroup.has_trivial_blocks
State after:
no goals