Theorem: alternatingGroup_is_perfect' (Jordan/Mathlib/Alternating.lean)

State before:
β : Type ?u.7470
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α
Tactic:
rw [← Subgroup.commutator_eq', alternatingGroup_is_perfect h5, Subgroup.map_top_eq_range,
  Subgroup.subtype_range]
State after:
no goals