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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Subgroup.Normal (V4 α)
Tactic:
haveI := V4_is_characteristic α hα4
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Characteristic (V4 α)
⊢ Subgroup.Normal (V4 α)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Characteristic (V4 α)
⊢ Subgroup.Normal (V4 α)
Tactic:
infer_instance
State after:
no goals