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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ (V4 α).carrier = {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
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 α)
⊢ (V4 α).carrier = {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (V4 α).carrier = {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
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 α)
⊢ S.carrier = {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ S.carrier = {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
Tactic:
rw [A4_sylow_carrier α hα4 S]
State after:
no goals