G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ closureCommutatorRepresentatives G } ≤ Nat.card ↑(commutatorSet G) + Nat.card ↑(commutatorSet G)
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ closureCommutatorRepresentatives G } ≤ 2 * Nat.card ↑(commutatorSet G)
rw [two_mul]
no goals
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank { x // x ∈ closureCommutatorRepresentatives G } ≤ Nat.card ↑(commutatorSet G) + Nat.card ↑(commutatorSet G)
exact
  (Subgroup.rank_closure_finite_le_nat_card _).trans
    ((Set.card_union_le _ _).trans
      (add_le_add ((Finite.card_image_le _).trans (Finite.card_range_le _))
        ((Finite.card_image_le _).trans (Finite.card_range_le _))))