G : Type u
inst✝ : Group G
⊢ Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } =
    Nat.card
      { x //
        x ∈
          map (Subgroup.subtype (closureCommutatorRepresentatives G))
            (_root_.commutator { x // x ∈ closureCommutatorRepresentatives G }) }
G : Type u
inst✝ : Group G
⊢ Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } =
    Nat.card { x // x ∈ _root_.commutator G }
rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ←
  MonoidHom.map_closure, ← commutator_eq_closure]
no goals
G : Type u
inst✝ : Group G
⊢ Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } =
    Nat.card
      { x //
        x ∈
          map (Subgroup.subtype (closureCommutatorRepresentatives G))
            (_root_.commutator { x // x ∈ closureCommutatorRepresentatives G }) }
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))