feat(Subgroup/IsCommutative): add instance for MonoidHom.range (#15370)

This PR adds:

- `instance Subgroup.commGroup_isCommutative [CommGroup G] (H : Subgroup G) : H.IsCommutative` for subgroups of an abelian group; and
- `instance MonoidHom.range_isCommutative [CommGroup G] (f : G →* N) : f.range.IsCommutative`, for the range of a `MonoidHom` whose domain is abelian.

It also adds a lemma `Subgroup.mul_comm_of_mem_isCommutative` to allow applying the commutativity without constructing terms of a `Subgroup`. (This lemma is included in this same PR as I mentioned it in the same Zulip thread, but is independent of the two instances above.)

Please refer to the [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/CommGroup.20MonoidHom.2Erange.20if.20the.20domain.20is.20a.20CommGroup) for discussions.

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -1728,6 +1728,11 @@ attribute [class] AddSubgroup.IsCommutative
 instance IsCommutative.commGroup [h : H.IsCommutative] : CommGroup H :=
   { H.toGroup with mul_comm := h.is_comm.comm }
 
+/-- A subgroup of a commutative group is commutative. -/
+@[to_additive "A subgroup of a commutative group is commutative."]
+instance commGroup_isCommutative {G : Type*} [CommGroup G] (H : Subgroup G) : H.IsCommutative :=
+  ⟨CommMagma.to_isCommutative⟩
+
 @[to_additive]
 instance map_isCommutative (f : G →* G') [H.IsCommutative] : (H.map f).IsCommutative :=
   ⟨⟨by
@@ -1749,6 +1754,11 @@ theorem comap_injective_isCommutative {f : G' →* G} (hf : Injective f) [H.IsCo
 instance subgroupOf_isCommutative [H.IsCommutative] : (H.subgroupOf K).IsCommutative :=
   H.comap_injective_isCommutative Subtype.coe_injective
 
+@[to_additive]
+lemma mul_comm_of_mem_isCommutative [H.IsCommutative] {a b : G} (ha : a ∈ H) (hb : b ∈ H) :
+    a * b = b * a := by
+  simpa only [Submonoid.mk_mul_mk, Subtype.mk.injEq] using mul_comm (⟨a, ha⟩ : H) (⟨b, hb⟩ : H)
+
 end Subgroup
 
 namespace MulEquiv
@@ -1954,6 +1964,11 @@ theorem mem_range {f : G →* N} {y : N} : y ∈ f.range ↔ ∃ x, f x = y :=
 @[to_additive]
 theorem range_eq_map (f : G →* N) : f.range = (⊤ : Subgroup G).map f := by ext; simp
 
+@[to_additive]
+instance range_isCommutative {G : Type*} [CommGroup G] {N : Type*} [Group N] (f : G →* N) :
+    f.range.IsCommutative :=
+  range_eq_map f ▸ Subgroup.map_isCommutative ⊤ f
+
 @[to_additive (attr := simp)]
 theorem restrict_range (f : G →* N) : (f.restrict K).range = K.map f := by
   simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,