G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) =
    Nat.card
      ↑(↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
          commutatorSet { x // x ∈ closureCommutatorRepresentatives G })
G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) = Nat.card ↑(commutatorSet G)
rw [← image_commutatorSet_closureCommutatorRepresentatives G]
no goals
G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) =
    Nat.card
      ↑(↑(Subgroup.subtype (closureCommutatorRepresentatives G)) ''
          commutatorSet { x // x ∈ closureCommutatorRepresentatives G })
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))