Theorem: alternatingGroup.V4_is_characteristic (Jordan/V4.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Subgroup.Characteristic (V4 α)
Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Characteristic (V4 α)

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Characteristic (V4 α)
Tactic:
rw [V4_is_unique_sylow α hα4 S]
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Characteristic ↑S

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Characteristic ↑S
Tactic:
refine' Sylow.characteristic_of_normal S _
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Normal ↑S

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Normal ↑S
Tactic:
rw [← Subgroup.normalizer_eq_top]
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.normalizer ↑S = ⊤

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.normalizer ↑S = ⊤
Tactic:
rw [← Subgroup.index_eq_one]
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.index (Subgroup.normalizer ↑S) = 1

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.index (Subgroup.normalizer ↑S) = 1
Tactic:
rw [← card_sylow_eq_index_normalizer]
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card (Sylow 2 ↥(alternatingGroup α)) = 1

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card (Sylow 2 ↥(alternatingGroup α)) = 1
Tactic:
exact A4_card_two_sylow_eq_one α hα4
State after:
no goals