G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ Subgroup.closure (commutatorSet G) } ≤ Nat.card ↑(commutatorSet G)
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ commutator G } ≤ Nat.card ↑(commutatorSet G)
rw [Subgroup.rank_congr (commutator_eq_closure G)]
no goals
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ Subgroup.closure (commutatorSet G) } ≤ Nat.card ↑(commutatorSet G)
apply Subgroup.rank_closure_finite_le_nat_card