Theorem: alternatingGroup.le_of_isPreprimitive (Jordan/AlternatingMaximal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
⊢ IsPreprimitive (↥G) α → alternatingGroup α ≤ G
Tactic:
intro hG'
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
⊢ alternatingGroup α ≤ G

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
⊢ alternatingGroup α ≤ G
Tactic:
obtain ⟨g, hg3, hg⟩ := has_three_cycle_of_stabilizer s hα
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ alternatingGroup α ≤ G

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ alternatingGroup α ≤ G
Tactic:
apply jordan_three_cycle hG' hg3
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ G

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ G
Tactic:
apply hG
State after:
case intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α

State before:
case intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Tactic:
simp only [Subgroup.mem_inf, hg, true_and_iff]
State after:
case intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ alternatingGroup α

State before:
case intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ alternatingGroup α
Tactic:
exact Equiv.Perm.IsThreeCycle.mem_alternatingGroup hg3
State after:
no goals