refactor(Normed/Group/Quotient): generalise to non-commutative groups

The goal is to apply this to the free group.

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -180,6 +180,10 @@ theorem isClosed_setOf_map_smul {N : Type*} [Monoid N] (α β) [MulAction M α]
   exact isClosed_iInter fun c => isClosed_iInter fun x =>
     isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)
 
+@[to_additive]
+instance Submonoid.continuousConstSMul {S : Submonoid M} : ContinuousConstSMul S α :=
+  IsInducing.id.continuousConstSMul Subtype.val rfl
+
 end Monoid
 
 section Group
@@ -191,6 +195,10 @@ theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} (c : G)
     Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
   ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul c⁻¹, fun h => h.const_smul _⟩
 
+@[to_additive]
+instance Subgroup.continuousConstSMul {S : Subgroup G} : ContinuousConstSMul S α :=
+  IsInducing.id.continuousConstSMul Subtype.val rfl
+
 variable [TopologicalSpace β] {f : β → α} {b : β} {s : Set β}
 
 @[to_additive]

Mathlib/Topology/Algebra/Group/Quotient.lean

@@ -41,9 +41,8 @@ alias quotientMap_mk := isQuotientMap_mk
 theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) :=
   continuous_quot_mk
 
-section ContinuousMul
-
-variable [ContinuousMul G] {N : Subgroup G}
+section ContinuousMulConst
+variable [ContinuousConstSMul Gᵐᵒᵖ G] {N : Subgroup G}
 
 @[to_additive]
 theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) := isOpenMap_quotient_mk'_mul
@@ -61,21 +60,27 @@ theorem dense_image_mk {s : Set G} :
     Dense (mk '' s : Set (G ⧸ N)) ↔ Dense (s * (N : Set G)) := by
   rw [← dense_preimage_mk, preimage_image_mk_eq_mul]
 
-@[to_additive]
-instance instContinuousSMul : ContinuousSMul G (G ⧸ N) where
-  continuous_smul := by
-    rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
-    exact continuous_mk.comp continuous_mul
-
-@[to_additive]
-instance instContinuousConstSMul : ContinuousConstSMul G (G ⧸ N) := inferInstance
-
 /-- A quotient of a locally compact group is locally compact. -/
 @[to_additive]
 instance instLocallyCompactSpace [LocallyCompactSpace G] (N : Subgroup G) :
     LocallyCompactSpace (G ⧸ N) :=
   QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace
 
+end ContinuousMulConst
+
+section ContinuousMul
+
+variable [ContinuousConstSMul Gᵐᵒᵖ G] {N : Subgroup G}
+
+-- @[to_additive]
+-- instance instContinuousSMul : ContinuousSMul G (G ⧸ N) where
+--   continuous_smul := by
+--     rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
+--     exact continuous_mk.comp continuous_mul
+
+-- @[to_additive]
+-- instance instContinuousConstSMul : ContinuousConstSMul G (G ⧸ N) := inferInstance
+
 @[to_additive (attr := deprecated "No deprecation message was provided." (since := "2024-10-05"))]
 theorem continuous_smul₁ (x : G ⧸ N) : Continuous fun g : G => g • x :=
   continuous_id.smul continuous_const