chore(ConstMulAction): generalize some lemmas (#31042)

... from `MulAction` to `SMul`.

Author: urkud

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -154,17 +154,6 @@ theorem Topology.IsInducing.continuousConstSMul {N β : Type*} [SMul N β] [Topo
   continuous_const_smul c := by
     simpa only [Function.comp_def, hf, hg.continuous_iff] using hg.continuous.const_smul (f c)
 
-end SMul
-
-section Monoid
-
-variable [TopologicalSpace α]
-variable [Monoid M] [MulAction M α] [ContinuousConstSMul M α]
-
-@[to_additive]
-instance Units.continuousConstSMul : ContinuousConstSMul Mˣ α where
-  continuous_const_smul m := continuous_const_smul (m : M)
-
 @[to_additive]
 theorem smul_closure_subset (c : M) (s : Set α) : c • closure s ⊆ closure (c • s) :=
   ((Set.mapsTo_image _ _).closure <| continuous_const_smul c).image_subset
@@ -175,18 +164,29 @@ theorem set_smul_closure_subset (s : Set M) (t : Set α) : s • closure t ⊆ c
   exact iUnion₂_subset fun c hc ↦ (smul_closure_subset c t).trans <| closure_mono <|
     subset_biUnion_of_mem (u := (· • t)) hc
 
-@[to_additive]
-theorem smul_closure_orbit_subset (c : M) (x : α) :
-    c • closure (MulAction.orbit M x) ⊆ closure (MulAction.orbit M x) :=
-  (smul_closure_subset c _).trans <| closure_mono <| MulAction.smul_orbit_subset _ _
-
-theorem isClosed_setOf_map_smul {N : Type*} [Monoid N] (α β) [MulAction M α] [MulAction N β]
+theorem isClosed_setOf_map_smul {N : Type*} (α β) [SMul M α] [SMul N β]
     [TopologicalSpace β] [T2Space β] [ContinuousConstSMul N β] (σ : M → N) :
     IsClosed { f : α → β | ∀ c x, f (c • x) = σ c • f x } := by
   simp only [Set.setOf_forall]
   exact isClosed_iInter fun c => isClosed_iInter fun x =>
     isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)
 
+end SMul
+
+section Monoid
+
+variable [TopologicalSpace α]
+variable [Monoid M] [MulAction M α] [ContinuousConstSMul M α]
+
+@[to_additive]
+instance Units.continuousConstSMul : ContinuousConstSMul Mˣ α where
+  continuous_const_smul m := continuous_const_smul (m : M)
+
+@[to_additive]
+theorem smul_closure_orbit_subset (c : M) (x : α) :
+    c • closure (MulAction.orbit M x) ⊆ closure (MulAction.orbit M x) :=
+  (smul_closure_subset c _).trans <| closure_mono <| MulAction.smul_orbit_subset _ _
+
 end Monoid
 
 section Group