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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↥↑S = 4
Tactic:
rw [Sylow.card_eq_multiplicity, ← Nat.factors_count_eq, A4_card α hα4]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ 2 ^ List.count 2 (Nat.factors 12) = 4

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ 2 ^ List.count 2 (Nat.factors 12) = 4
Tactic:
rfl
State after:
no goals