diff --git a/Mathlib.lean b/Mathlib.lean
index 34b7d642b64d3..3fa3db84ecc00 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3185,6 +3185,7 @@ import Mathlib.Topology.Algebra.Order.Rolle
 import Mathlib.Topology.Algebra.Order.T5
 import Mathlib.Topology.Algebra.Order.UpperLower
 import Mathlib.Topology.Algebra.Polynomial
+import Mathlib.Topology.Algebra.ProperConstSMul
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Algebra.Ring.Ideal
 import Mathlib.Topology.Algebra.Semigroup
diff --git a/Mathlib/Topology/Algebra/ProperConstSMul.lean b/Mathlib/Topology/Algebra/ProperConstSMul.lean
new file mode 100644
index 0000000000000..88028aeddf562
--- /dev/null
+++ b/Mathlib/Topology/Algebra/ProperConstSMul.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Topology.Algebra.ConstMulAction
+import Mathlib.Topology.ProperMap
+/-!
+# Actions by proper maps
+
+In this file we define `ProperConstSMul M X` to be a mixin `Prop`-value class
+stating that `(c • ·)` is a proper map for all `c`.
+
+Note that this is **not** the same as a proper action (not yet in `Mathlib`)
+which requires `(c, x) ↦ (c • x, x)` to be a proper map.
+
+We also provide 4 instances:
+- for a continuous action on a compact Hausdorff space,
+- and for a continuous group action on a general space;
+- for the action on `X × Y`;
+- for the action on `∀ i, X i`.
+-/
+
+/-- A mixin typeclass saying that the `(c +ᵥ ·)` is a proper map for all `c`.
+
+Note that this is **not** the same as a proper additive action (not yet in `Mathlib`). -/
+class ProperConstVAdd (M X : Type*) [VAdd M X] [TopologicalSpace X] : Prop where
+  /-- `(c +ᵥ ·)` is a proper map. -/
+  isProperMap_vadd (c : M) : IsProperMap ((c +ᵥ ·) : X → X)
+
+/-- A mixin typeclass saying that `(c • ·)` is a proper map for all `c`.
+
+Note that this is **not** the same as a proper multiplicative action (not yet in `Mathlib`). -/
+@[to_additive]
+class ProperConstSMul (M X : Type*) [SMul M X] [TopologicalSpace X] : Prop where
+  /-- `(c • ·)` is a proper map. -/
+  isProperMap_smul (c : M) : IsProperMap ((c • ·) : X → X)
+
+/-- `(c • ·)` is a proper map. -/
+@[to_additive "`(c +ᵥ ·)` is a proper map."]
+theorem isProperMap_smul {M : Type*} (c : M) (X : Type*) [SMul M X] [TopologicalSpace X]
+    [h : ProperConstSMul M X] : IsProperMap ((c • ·) : X → X) := h.1 c
+
+/-- The preimage of a compact set under `(c • ·)` is a compact set. -/
+@[to_additive "The preimage of a compact set under `(c +ᵥ ·)` is a compact set."]
+theorem IsCompact.preimage_smul {M X : Type*} [SMul M X] [TopologicalSpace X]
+    [ProperConstSMul M X] {s : Set X} (hs : IsCompact s) (c : M) : IsCompact ((c • ·) ⁻¹' s) :=
+  (isProperMap_smul c X).isCompact_preimage hs
+
+@[to_additive]
+instance (priority := 100) {M X : Type*} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X]
+    [T2Space X] [CompactSpace X] : ProperConstSMul M X :=
+  ⟨fun c ↦ (continuous_const_smul c).isProperMap⟩
+
+@[to_additive]
+instance (priority := 100) {G X : Type*} [Group G] [MulAction G X] [TopologicalSpace X]
+    [ContinuousConstSMul G X] : ProperConstSMul G X :=
+  ⟨fun c ↦ (Homeomorph.smul c).isProperMap⟩
+
+instance {M X Y : Type*}
+    [SMul M X] [TopologicalSpace X] [ProperConstSMul M X]
+    [SMul M Y] [TopologicalSpace Y] [ProperConstSMul M Y] :
+    ProperConstSMul M (X × Y) :=
+  ⟨fun c ↦ (isProperMap_smul c X).prod_map (isProperMap_smul c Y)⟩
+
+instance {M ι : Type*} {X : ι → Type*}
+    [∀ i, SMul M (X i)] [∀ i, TopologicalSpace (X i)] [∀ i, ProperConstSMul M (X i)] :
+    ProperConstSMul M (∀ i, X i) :=
+  ⟨fun c ↦ .pi_map fun i ↦ isProperMap_smul c (X i)⟩
diff --git a/Mathlib/Topology/ProperMap.lean b/Mathlib/Topology/ProperMap.lean
index 12a3b1c256506..e576d67c01f6a 100644
--- a/Mathlib/Topology/ProperMap.lean
+++ b/Mathlib/Topology/ProperMap.lean
@@ -126,6 +126,12 @@ lemma isProperMap_iff_ultrafilter : IsProperMap f ↔ Continuous f ∧
     rcases H (tendsto_iff_comap.mpr <| hy.trans inf_le_left) with ⟨x, hxy, hx⟩
     exact ⟨x, hxy, 𝒰, le_inf hx (hy.trans inf_le_right)⟩
 
+lemma isProperMap_iff_ultrafilter_of_t2 [T2Space Y] : IsProperMap f ↔ Continuous f ∧
+    ∀ ⦃𝒰 : Ultrafilter X⦄, ∀ ⦃y : Y⦄, Tendsto f 𝒰 (𝓝 y) → ∃ x, 𝒰.1 ≤ 𝓝 x :=
+  isProperMap_iff_ultrafilter.trans <| and_congr_right fun hc ↦ forall₃_congr fun _𝒰 _y hy ↦
+    exists_congr fun x ↦ and_iff_right_of_imp fun h ↦
+      tendsto_nhds_unique ((hc.tendsto x).mono_left h) hy
+
 /-- If `f` is proper and converges to `y` along some ultrafilter `𝒰`, then `𝒰` converges to some
 `x` such that `f x = y`. -/
 lemma IsProperMap.ultrafilter_le_nhds_of_tendsto (h : IsProperMap f) ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄
@@ -234,6 +240,10 @@ lemma isProperMap_iff_isClosedMap_and_tendsto_cofinite [T1Space Y] :
   exact isCompact_of_isClosed_subset hK (isClosed_singleton.preimage f_cont)
     (compl_le_compl_iff_le.mp hKy)
 
+/-- A continuous map from a compact space to a T₂ space is a proper map. -/
+theorem Continuous.isProperMap [CompactSpace X] [T2Space Y] (hf : Continuous f) : IsProperMap f :=
+  isProperMap_iff_isClosedMap_and_tendsto_cofinite.2 ⟨hf, hf.isClosedMap, by simp⟩
+
 /-- If `Y` is locally compact and Hausdorff, then proper maps `X → Y` are exactly continuous maps
 such that the preimage of any compact set is compact. -/
 theorem isProperMap_iff_isCompact_preimage [T2Space Y] [LocallyCompactSpace Y] :
@@ -241,19 +251,18 @@ theorem isProperMap_iff_isCompact_preimage [T2Space Y] [LocallyCompactSpace Y] :
   constructor <;> intro H
   -- The direct implication follows from the previous results
   · exact ⟨H.continuous, fun K hK ↦ H.isCompact_preimage hK⟩
-  · rw [isProperMap_iff_ultrafilter]
-  -- Let `𝒰 : Ultrafilter X`, and assume that `f` tends to some `y` along `𝒰`.
+  · rw [isProperMap_iff_ultrafilter_of_t2]
+    -- Let `𝒰 : Ultrafilter X`, and assume that `f` tends to some `y` along `𝒰`.
     refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
-  -- Pick `K` some compact neighborhood of `y`, which exists by local compactness.
+    -- Pick `K` some compact neighborhood of `y`, which exists by local compactness.
     rcases exists_compact_mem_nhds y with ⟨K, hK, hKy⟩
-  -- Then `map f 𝒰 ≤ 𝓝 y ≤ 𝓟 K`, hence `𝒰 ≤ 𝓟 (f ⁻¹' K)`
+    -- Then `map f 𝒰 ≤ 𝓝 y ≤ 𝓟 K`, hence `𝒰 ≤ 𝓟 (f ⁻¹' K)`
     have : 𝒰 ≤ 𝓟 (f ⁻¹' K) := by
       simpa only [← comap_principal, ← tendsto_iff_comap] using
         hy.mono_right (le_principal_iff.mpr hKy)
-  -- By compactness of `f ⁻¹' K`, `𝒰` converges to some `x ∈ f ⁻¹' K`.
+    -- By compactness of `f ⁻¹' K`, `𝒰` converges to some `x ∈ f ⁻¹' K`.
     rcases (H.2 hK).ultrafilter_le_nhds _ this with ⟨x, -, hx⟩
-  -- Finally, `f` tends to `f x` along `𝒰` by continuity, thus `f x = y`.
-    refine ⟨x, tendsto_nhds_unique ((H.1.tendsto _).comp hx) hy, hx⟩
+    exact ⟨x, hx⟩
 
 /-- Version of `isProperMap_iff_isCompact_preimage` in terms of `cocompact`. -/
 lemma isProperMap_iff_tendsto_cocompact [T2Space Y] [LocallyCompactSpace Y] :
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index 73590576f25a0..e96b4e724267e 100644
--- a/Mathlib/Topology/Separation.lean
+++ b/Mathlib/Topology/Separation.lean
@@ -1311,6 +1311,10 @@ theorem Bornology.relativelyCompact_eq_inCompact [T2Space α] :
   Bornology.ext _ _ Filter.coclosedCompact_eq_cocompact
 #align bornology.relatively_compact_eq_in_compact Bornology.relativelyCompact_eq_inCompact
 
+theorem IsCompact.preimage_continuous [CompactSpace α] [T2Space β] {f : α → β} {s : Set β}
+    (hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s) :=
+  (hs.isClosed.preimage hf).isCompact
+
 /-- If `V : ι → Set α` is a decreasing family of compact sets then any neighborhood of
 `⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhds_of_isCompact'` where we
 don't need to assume each `V i` closed because it follows from compactness since `α` is