From 42c8d83d0b3ed400cb25f596edebba6ee58fc16e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Fri, 18 Aug 2023 21:40:45 -0500
Subject: [PATCH 1/8] feat: define `CocompactSMul`

---
 Mathlib.lean                                |  1 +
 Mathlib/Topology/Algebra/CocompactSMul.lean | 41 +++++++++++++++++++++
 Mathlib/Topology/Separation.lean            |  4 ++
 3 files changed, 46 insertions(+)
 create mode 100644 Mathlib/Topology/Algebra/CocompactSMul.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 1bf8d114d1aa0..1745db0ec2c99 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3125,6 +3125,7 @@ import Mathlib.Testing.SlimCheck.Sampleable
 import Mathlib.Testing.SlimCheck.Testable
 import Mathlib.Topology.Algebra.Affine
 import Mathlib.Topology.Algebra.Algebra
+import Mathlib.Topology.Algebra.CocompactSMul
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions
 import Mathlib.Topology.Algebra.ContinuousAffineMap
diff --git a/Mathlib/Topology/Algebra/CocompactSMul.lean b/Mathlib/Topology/Algebra/CocompactSMul.lean
new file mode 100644
index 0000000000000..ecf798d8aecff
--- /dev/null
+++ b/Mathlib/Topology/Algebra/CocompactSMul.lean
@@ -0,0 +1,41 @@
+/-
+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
+/-!
+# Cocompact actions
+
+In this file we define `CocompactSMul M X` to be a mixin `Prop`-value class
+stating that the preimage of a compact set under `(c • ·)` is a compact set.
+
+We also provide 2 instances:
+- for a continuous action on a compact Hausdorff space,
+- and for a continuous group action on a general space.
+-/
+
+/-- A mixin typeclass saying that
+the preimage of a compact set under `(c +ᵥ ·)` is a compact set. -/
+class CocompactVAdd (M X : Type*) [VAdd M X] [TopologicalSpace X] : Prop where
+  /-- The preimage of a compact set under `(c +ᵥ ·)` is a compact set. -/
+  isCompact_preimage_vadd (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c +ᵥ ·) ⁻¹' s)
+
+/-- A mixin typeclass saying that the preimage of a compact set under `(c • ·)` is a compact set. -/
+@[to_additive]
+class CocompactSMul (M X : Type*) [SMul M X] [TopologicalSpace X] : Prop where
+  /-- The preimage of a compact set under `(c • ·)` is a compact set. -/
+  isCompact_preimage_smul (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c • ·) ⁻¹' s)
+
+alias CocompactSMul.isCompact_preimage_smul ← IsCompact.preimage_smul
+attribute [to_additive] IsCompact.preimage_smul
+
+@[to_additive]
+instance (priority := 100) {M X : Type*} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X]
+    [T2Space X] [CompactSpace X] : CocompactSMul M X :=
+  ⟨fun c _s hs ↦ hs.preimage_continuous (continuous_const_smul c)⟩
+
+@[to_additive]
+instance (priority := 100) {G X : Type*} [Group G] [MulAction G X] [TopologicalSpace X]
+    [ContinuousConstSMul G X] : CocompactSMul G X :=
+  ⟨fun c _s hs ↦ by rw [Set.preimage_smul]; exact hs.smul _⟩
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
index 87f61d0372917..7752dd6b4ebf6 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

From 0725c5afd6bc69a8739fb5454c07d469c70524ad Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Fri, 18 Aug 2023 22:42:00 -0500
Subject: [PATCH 2/8] Apply suggestions from code review

---
 Mathlib/Topology/Algebra/CocompactSMul.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/CocompactSMul.lean b/Mathlib/Topology/Algebra/CocompactSMul.lean
index ecf798d8aecff..b14eb3539804a 100644
--- a/Mathlib/Topology/Algebra/CocompactSMul.lean
+++ b/Mathlib/Topology/Algebra/CocompactSMul.lean
@@ -27,8 +27,10 @@ class CocompactSMul (M X : Type*) [SMul M X] [TopologicalSpace X] : Prop where
   /-- The preimage of a compact set under `(c • ·)` is a compact set. -/
   isCompact_preimage_smul (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c • ·) ⁻¹' s)
 
+/-- The preimage of a compact set under `(c • ·)` is a compact set. -/
 alias CocompactSMul.isCompact_preimage_smul ← IsCompact.preimage_smul
-attribute [to_additive] IsCompact.preimage_smul
+attribute [to_additive "The preimage of a compact set under `(c +ᵥ ·)` is a compact set."]
+  IsCompact.preimage_smul
 
 @[to_additive]
 instance (priority := 100) {M X : Type*} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X]

From 6b6493fe23466c30b74a046e763ec63ffad061e0 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 19 Aug 2023 00:24:16 -0500
Subject: [PATCH 3/8] Fix def/lemma

---
 Mathlib/Topology/Algebra/CocompactSMul.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Algebra/CocompactSMul.lean b/Mathlib/Topology/Algebra/CocompactSMul.lean
index b14eb3539804a..2b94ea00aee71 100644
--- a/Mathlib/Topology/Algebra/CocompactSMul.lean
+++ b/Mathlib/Topology/Algebra/CocompactSMul.lean
@@ -28,9 +28,10 @@ class CocompactSMul (M X : Type*) [SMul M X] [TopologicalSpace X] : Prop where
   isCompact_preimage_smul (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c • ·) ⁻¹' s)
 
 /-- The preimage of a compact set under `(c • ·)` is a compact set. -/
-alias CocompactSMul.isCompact_preimage_smul ← IsCompact.preimage_smul
-attribute [to_additive "The preimage of a compact set under `(c +ᵥ ·)` is a compact set."]
-  IsCompact.preimage_smul
+@[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] [CocompactSMul M X]
+    {s : Set X} (hs : IsCompact s) (c : M) : IsCompact ((c • ·) ⁻¹' s) :=
+  CocompactSMul.isCompact_preimage_smul c hs
 
 @[to_additive]
 instance (priority := 100) {M X : Type*} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X]

From e1085629f9f867c6d5d1f968bc03375f0a7423fe Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 19 Aug 2023 11:26:21 -0500
Subject: [PATCH 4/8] Rename file&TC

---
 Mathlib.lean                                   |  2 +-
 ...mpactSMul.lean => CompactPreimageSMul.lean} | 18 +++++++++---------
 2 files changed, 10 insertions(+), 10 deletions(-)
 rename Mathlib/Topology/Algebra/{CocompactSMul.lean => CompactPreimageSMul.lean} (73%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 297787ad7a2c0..d9273f94aadbf 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3126,7 +3126,7 @@ import Mathlib.Testing.SlimCheck.Sampleable
 import Mathlib.Testing.SlimCheck.Testable
 import Mathlib.Topology.Algebra.Affine
 import Mathlib.Topology.Algebra.Algebra
-import Mathlib.Topology.Algebra.CocompactSMul
+import Mathlib.Topology.Algebra.CompactPreimageSMul
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions
 import Mathlib.Topology.Algebra.ContinuousAffineMap
diff --git a/Mathlib/Topology/Algebra/CocompactSMul.lean b/Mathlib/Topology/Algebra/CompactPreimageSMul.lean
similarity index 73%
rename from Mathlib/Topology/Algebra/CocompactSMul.lean
rename to Mathlib/Topology/Algebra/CompactPreimageSMul.lean
index 2b94ea00aee71..6e696e3121ccc 100644
--- a/Mathlib/Topology/Algebra/CocompactSMul.lean
+++ b/Mathlib/Topology/Algebra/CompactPreimageSMul.lean
@@ -5,9 +5,9 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Topology.Algebra.ConstMulAction
 /-!
-# Cocompact actions
+# Compact preimage actions
 
-In this file we define `CocompactSMul M X` to be a mixin `Prop`-value class
+In this file we define `CompactPreimageSMul M X` to be a mixin `Prop`-value class
 stating that the preimage of a compact set under `(c • ·)` is a compact set.
 
 We also provide 2 instances:
@@ -17,28 +17,28 @@ We also provide 2 instances:
 
 /-- A mixin typeclass saying that
 the preimage of a compact set under `(c +ᵥ ·)` is a compact set. -/
-class CocompactVAdd (M X : Type*) [VAdd M X] [TopologicalSpace X] : Prop where
+class CompactPreimageVAdd (M X : Type*) [VAdd M X] [TopologicalSpace X] : Prop where
   /-- The preimage of a compact set under `(c +ᵥ ·)` is a compact set. -/
   isCompact_preimage_vadd (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c +ᵥ ·) ⁻¹' s)
 
 /-- A mixin typeclass saying that the preimage of a compact set under `(c • ·)` is a compact set. -/
 @[to_additive]
-class CocompactSMul (M X : Type*) [SMul M X] [TopologicalSpace X] : Prop where
+class CompactPreimageSMul (M X : Type*) [SMul M X] [TopologicalSpace X] : Prop where
   /-- The preimage of a compact set under `(c • ·)` is a compact set. -/
   isCompact_preimage_smul (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c • ·) ⁻¹' s)
 
 /-- 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] [CocompactSMul M X]
-    {s : Set X} (hs : IsCompact s) (c : M) : IsCompact ((c • ·) ⁻¹' s) :=
-  CocompactSMul.isCompact_preimage_smul c hs
+theorem IsCompact.preimage_smul {M X : Type*} [SMul M X] [TopologicalSpace X]
+    [CompactPreimageSMul M X] {s : Set X} (hs : IsCompact s) (c : M) : IsCompact ((c • ·) ⁻¹' s) :=
+  CompactPreimageSMul.isCompact_preimage_smul c hs
 
 @[to_additive]
 instance (priority := 100) {M X : Type*} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X]
-    [T2Space X] [CompactSpace X] : CocompactSMul M X :=
+    [T2Space X] [CompactSpace X] : CompactPreimageSMul M X :=
   ⟨fun c _s hs ↦ hs.preimage_continuous (continuous_const_smul c)⟩
 
 @[to_additive]
 instance (priority := 100) {G X : Type*} [Group G] [MulAction G X] [TopologicalSpace X]
-    [ContinuousConstSMul G X] : CocompactSMul G X :=
+    [ContinuousConstSMul G X] : CompactPreimageSMul G X :=
   ⟨fun c _s hs ↦ by rw [Set.preimage_smul]; exact hs.smul _⟩

From 74f8ea4c1a8e1bc15d865466db5e3229a7dcea00 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Fri, 25 Aug 2023 01:34:14 -0500
Subject: [PATCH 5/8] Add a lemma requested in a review

---
 Mathlib/Topology/ProperMap.lean | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Topology/ProperMap.lean b/Mathlib/Topology/ProperMap.lean
index 12a3b1c256506..93dbae52f22d6 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] :

From c8c7696d5cb10e1acb83040b434df81dcab168ed Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Fri, 25 Aug 2023 09:44:09 -0500
Subject: [PATCH 6/8] Fix

---
 Mathlib/Topology/ProperMap.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/ProperMap.lean b/Mathlib/Topology/ProperMap.lean
index 93dbae52f22d6..e576d67c01f6a 100644
--- a/Mathlib/Topology/ProperMap.lean
+++ b/Mathlib/Topology/ProperMap.lean
@@ -128,7 +128,7 @@ lemma isProperMap_iff_ultrafilter : IsProperMap f ↔ Continuous f ∧
 
 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 ↦
+  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
 

From 444260e125ff7db9ca14ce1820c82f65201161c0 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Fri, 25 Aug 2023 11:57:51 -0500
Subject: [PATCH 7/8] Snapshot

---
 Mathlib.lean                                  |  2 +-
 .../Topology/Algebra/CompactPreimageSMul.lean | 44 ------------
 Mathlib/Topology/Algebra/ProperConstSMul.lean | 67 +++++++++++++++++++
 3 files changed, 68 insertions(+), 45 deletions(-)
 delete mode 100644 Mathlib/Topology/Algebra/CompactPreimageSMul.lean
 create mode 100644 Mathlib/Topology/Algebra/ProperConstSMul.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index cdee69b1bd098..3fa3db84ecc00 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3130,7 +3130,6 @@ import Mathlib.Testing.SlimCheck.Sampleable
 import Mathlib.Testing.SlimCheck.Testable
 import Mathlib.Topology.Algebra.Affine
 import Mathlib.Topology.Algebra.Algebra
-import Mathlib.Topology.Algebra.CompactPreimageSMul
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions
 import Mathlib.Topology.Algebra.ContinuousAffineMap
@@ -3186,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/CompactPreimageSMul.lean b/Mathlib/Topology/Algebra/CompactPreimageSMul.lean
deleted file mode 100644
index 6e696e3121ccc..0000000000000
--- a/Mathlib/Topology/Algebra/CompactPreimageSMul.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-/-
-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
-/-!
-# Compact preimage actions
-
-In this file we define `CompactPreimageSMul M X` to be a mixin `Prop`-value class
-stating that the preimage of a compact set under `(c • ·)` is a compact set.
-
-We also provide 2 instances:
-- for a continuous action on a compact Hausdorff space,
-- and for a continuous group action on a general space.
--/
-
-/-- A mixin typeclass saying that
-the preimage of a compact set under `(c +ᵥ ·)` is a compact set. -/
-class CompactPreimageVAdd (M X : Type*) [VAdd M X] [TopologicalSpace X] : Prop where
-  /-- The preimage of a compact set under `(c +ᵥ ·)` is a compact set. -/
-  isCompact_preimage_vadd (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c +ᵥ ·) ⁻¹' s)
-
-/-- A mixin typeclass saying that the preimage of a compact set under `(c • ·)` is a compact set. -/
-@[to_additive]
-class CompactPreimageSMul (M X : Type*) [SMul M X] [TopologicalSpace X] : Prop where
-  /-- The preimage of a compact set under `(c • ·)` is a compact set. -/
-  isCompact_preimage_smul (c : M) {s : Set X} (hs : IsCompact s) : IsCompact ((c • ·) ⁻¹' s)
-
-/-- 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]
-    [CompactPreimageSMul M X] {s : Set X} (hs : IsCompact s) (c : M) : IsCompact ((c • ·) ⁻¹' s) :=
-  CompactPreimageSMul.isCompact_preimage_smul c hs
-
-@[to_additive]
-instance (priority := 100) {M X : Type*} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X]
-    [T2Space X] [CompactSpace X] : CompactPreimageSMul M X :=
-  ⟨fun c _s hs ↦ hs.preimage_continuous (continuous_const_smul c)⟩
-
-@[to_additive]
-instance (priority := 100) {G X : Type*} [Group G] [MulAction G X] [TopologicalSpace X]
-    [ContinuousConstSMul G X] : CompactPreimageSMul G X :=
-  ⟨fun c _s hs ↦ by rw [Set.preimage_smul]; exact hs.smul _⟩
diff --git a/Mathlib/Topology/Algebra/ProperConstSMul.lean b/Mathlib/Topology/Algebra/ProperConstSMul.lean
new file mode 100644
index 0000000000000..bbfe7fad97ac2
--- /dev/null
+++ b/Mathlib/Topology/Algebra/ProperConstSMul.lean
@@ -0,0 +1,67 @@
+/-
+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`. -/
+@[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)⟩

From 4a04c8bae97fd39bc08b20f4a332e20842d3d105 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 30 Aug 2023 10:06:58 -0500
Subject: [PATCH 8/8] Update Mathlib/Topology/Algebra/ProperConstSMul.lean

---
 Mathlib/Topology/Algebra/ProperConstSMul.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/ProperConstSMul.lean b/Mathlib/Topology/Algebra/ProperConstSMul.lean
index bbfe7fad97ac2..88028aeddf562 100644
--- a/Mathlib/Topology/Algebra/ProperConstSMul.lean
+++ b/Mathlib/Topology/Algebra/ProperConstSMul.lean
@@ -28,7 +28,9 @@ 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`. -/
+/-- 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. -/