feat: generalize IsClosed.vadd_right_of_isCompact to proper actions (#29715)

I realized a few weeks after adding them to Mathlib that the more conceptual approach for lemmas of the form "`s • t` is closed when one of `s` and `t` is closed and the other is compact" is that of proper maps and proper actions. This PR switches to this approach.

More precisely:
- I refactored the proof [IsClosed.smul_left_of_isCompact](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Group/Pointwise.html#IsClosed.smul_left_of_isCompact) in terms of properness. The proof is essentially the same length, but conceptually simpler.
- More importantly, I generalize [IsClosed.vadd_right_of_isCompact](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Group/AddTorsor.html#IsClosed.vadd_right_of_isCompact) from topological torsors to proper actions. Note that I do not assume separation, which creates some troubles as compact sets are not closed...

Author: ADedecker

Mathlib/Topology/Algebra/Group/AddTorsor.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Attila Gáspár
 -/
 import Mathlib.Algebra.AddTorsor.Basic
-import Mathlib.Topology.Algebra.Group.Pointwise
+import Mathlib.Topology.Algebra.Monoid
+import Mathlib.Topology.Algebra.Group.Defs
 
 /-!
 # Topological torsors of additive groups
@@ -84,22 +85,6 @@ def Homeomorph.vaddConst (p : P) : V ≃ₜ P where
   continuous_toFun := by fun_prop
   continuous_invFun := by fun_prop
 
-section Pointwise
-
-open Pointwise
-
-theorem IsClosed.vadd_right_of_isCompact {s : Set V} {t : Set P} (hs : IsClosed s)
-    (ht : IsCompact t) : IsClosed (s +ᵥ t) := by
-  have ⟨p⟩ : Nonempty P := inferInstance
-  have cont : Continuous (· -ᵥ p) := by fun_prop
-  have := IsTopologicalAddTorsor.to_isTopologicalAddGroup V P
-  convert (hs.add_right_of_isCompact <| ht.image cont).preimage cont
-  rw [Set.eq_preimage_iff_image_eq <| by exact (Equiv.vaddConst p).symm.bijective,
-    ← Set.image2_vadd, Set.image_image2, ← Set.image2_add, Set.image2_image_right]
-  simp only [vadd_vsub_assoc]
-
-end Pointwise
-
 end AddTorsor
 
 section AddGroup

Mathlib/Topology/Algebra/Group/Pointwise.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
 import Mathlib.Topology.Algebra.Group.Basic
+import Mathlib.Topology.Maps.Proper.Basic
 
 /-!
 # Pointwise operations on sets in topological groups
@@ -44,38 +45,33 @@ section ContinuousSMul
 variable [TopologicalSpace α] [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousInv α]
   [ContinuousSMul α β] {s : Set α} {t : Set β}
 
-@[to_additive]
+open Prod in
+/-- If `G` acts on `X` continuously, the set `s • t` is closed when `s : Set G` is *compact* and
+`t : Set X` is *closed*.
+
+See also `IsClosed.smul_right_of_isCompact` for a version with the assumptions on `s` and `t`
+reversed, assuming that the action is *proper*. -/
+@[to_additive
+/-- If `G` acts on `X` continuously, the set `s +ᵥ t` is closed when `s : Set G` is *compact* and
+`t : Set X` is *closed*.
+
+See also `IsClosed.vadd_right_of_isCompact` for a version with the assumptions on `s` and `t`
+reversed, assuming that the action is *proper*. -/]
 theorem IsClosed.smul_left_of_isCompact (ht : IsClosed t) (hs : IsCompact s) :
     IsClosed (s • t) := by
-  have : ∀ x ∈ s • t, ∃ g ∈ s, g⁻¹ • x ∈ t := by
-    rintro x ⟨g, hgs, y, hyt, rfl⟩
-    refine ⟨g, hgs, ?_⟩
-    rwa [inv_smul_smul]
-  choose! f hf using this
-  refine isClosed_of_closure_subset (fun x hx ↦ ?_)
-  rcases mem_closure_iff_ultrafilter.mp hx with ⟨u, hust, hux⟩
-  have : Ultrafilter.map f u ≤ 𝓟 s :=
-    calc Ultrafilter.map f u ≤ map f (𝓟 (s • t)) := map_mono (le_principal_iff.mpr hust)
-      _ = 𝓟 (f '' (s • t)) := map_principal
-      _ ≤ 𝓟 s := principal_mono.mpr (image_subset_iff.mpr (fun x hx ↦ (hf x hx).1))
-  rcases hs.ultrafilter_le_nhds (Ultrafilter.map f u) this with ⟨g, hg, hug⟩
-  suffices g⁻¹ • x ∈ t from
-    ⟨g, hg, g⁻¹ • x, this, smul_inv_smul _ _⟩
-  exact ht.mem_of_tendsto ((Tendsto.inv hug).smul hux)
-    (Eventually.mono hust (fun y hy ↦ (hf y hy).2))
-
-/-! One may expect a version of `IsClosed.smul_left_of_isCompact` where `t` is compact and `s` is
-closed, but such a lemma can't be true in this level of generality. For a counterexample, consider
-`ℚ` acting on `ℝ` by translation, and let `s : Set ℚ := univ`, `t : set ℝ := {0}`. Then `s` is
-closed and `t` is compact, but `s +ᵥ t` is the set of all rationals, which is definitely not
-closed in `ℝ`.
-To fix the proof, we would need to make two additional assumptions:
-- for any `x ∈ t`, `s • {x}` is closed
-- for any `x ∈ t`, there is a continuous function `g : s • {x} → s` such that, for all
-  `y ∈ s • {x}`, we have `y = (g y) • x`
-These are fairly specific hypotheses so we don't state this version of the lemmas, but an
-interesting fact is that these two assumptions are verified in the case of an
-`IsTopologicalAddTorsor`. We prove this special case in `IsClosed.vadd_right_of_isCompact`. -/
+  let Φ : s × β ≃ₜ s × β :=
+  { toFun := fun gx ↦ (gx.1, (gx.1 : α) • gx.2)
+    invFun := fun gx ↦ (gx.1, (gx.1 : α)⁻¹ • gx.2)
+    left_inv := fun _ ↦ by simp
+    right_inv := fun _ ↦ by simp }
+  have : s • t = (snd ∘ Φ) '' (snd ⁻¹' t) :=
+    subset_antisymm
+      (smul_subset_iff.mpr fun g hg x hx ↦ mem_image_of_mem (snd ∘ Φ) (x := ⟨⟨g, hg⟩, x⟩) hx)
+      (image_subset_iff.mpr fun ⟨⟨g, hg⟩, x⟩ hx ↦ smul_mem_smul hg hx)
+  rw [this]
+  have : CompactSpace s := isCompact_iff_compactSpace.mp hs
+  exact (isProperMap_snd_of_compactSpace.comp Φ.isProperMap).isClosedMap _
+    (ht.preimage continuous_snd)
 
 @[to_additive]
 theorem MulAction.isClosedMap_quotient [CompactSpace α] :

Mathlib/Topology/Algebra/ProperAction/Basic.lean

@@ -5,8 +5,8 @@ Authors: Anatole Dedeker, Etienne Marion, Florestan Martin-Baillon, Vincent Guir
 -/
 import Mathlib.Topology.Algebra.Group.Quotient
 import Mathlib.Topology.Algebra.MulAction
-import Mathlib.Topology.Maps.Proper.Basic
-import Mathlib.Topology.Maps.OpenQuotient
+import Mathlib.Topology.Algebra.Group.Defs
+import Mathlib.Topology.LocalAtTarget
 
 /-!
 # Proper group action
@@ -205,3 +205,52 @@ instance [IsTopologicalGroup G] {H : Subgroup G} [H_closed : IsClosed (H : Set G
 instance QuotientGroup.instT2Space [IsTopologicalGroup G] {H : Subgroup G} [IsClosed (H : Set G)] :
     T2Space (G ⧸ H) :=
   t2Space_quotient_mulAction_of_properSMul
+
+/-- If `G` acts on `X` properly, then the map `G × T → X × T, (g, t) ↦ (g • t, t)` is still
+proper for *any* subset `T` of `X`. -/
+@[to_additive
+/-- If `G` acts on `X` properly, then the map `G × T → X × T, (g, t) ↦ (g +ᵥ t, t)` is still
+proper for *any* subset `T` of `X`. -/]
+lemma ProperSMul.isProperMap_smul_pair_set [ProperSMul G X] {t : Set X} :
+    IsProperMap (fun (gx : G × t) ↦ ((gx.1 • gx.2, gx.2) : X × t)) := by
+  let Φ : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
+  have Φ_proper : IsProperMap Φ := ProperSMul.isProperMap_smul_pair
+  let α : G × t ≃ₜ (Φ ⁻¹' (snd ⁻¹' t)) :=
+    have : univ ×ˢ t = Φ ⁻¹' (snd ⁻¹' t) := by rw [univ_prod]; rfl
+    Homeomorph.Set.univ G |>.symm.prodCongr (.refl t) |>.trans
+      ((Homeomorph.Set.prod _ t).symm) |>.trans (Homeomorph.setCongr this)
+  let β : X × t ≃ₜ (snd ⁻¹' t) :=
+    Homeomorph.Set.univ X |>.symm.prodCongr (.refl t) |>.trans
+      ((Homeomorph.Set.prod _ t).symm) |>.trans (Homeomorph.setCongr univ_prod)
+  exact β.symm.isProperMap.comp (Φ_proper.restrictPreimage (snd ⁻¹' t)) |>.comp α.isProperMap
+
+open Pointwise in
+/-- If `G` acts on `X` properly, the set `s • t` is closed when `s : Set G` is *closed* and
+`t : Set X` is *compact*.
+
+See also `IsClosed.smul_left_of_isCompact` for a version with the assumptions on `s` and `t`
+reversed. -/
+@[to_additive
+/-- If `G` acts on `X` properly, the set `s +ᵥ t` is closed when `s : Set G` is *closed* and
+`t : Set X` is *compact*. In particular, this applies when the action comes from an
+`IsTopologicalAddTorsor`.
+
+See also `IsClosed.vadd_left_of_isCompact` for a version with the assumptions on `s` and `t`
+reversed. -/]
+theorem IsClosed.smul_right_of_isCompact [ProperSMul G X] {s : Set G} {t : Set X} (hs : IsClosed s)
+    (ht : IsCompact t) : IsClosed (s • t) := by
+  let Ψ : G × t → X × t := fun gx ↦ (gx.1 • gx.2, gx.2)
+  have Ψ_proper : IsProperMap Ψ := ProperSMul.isProperMap_smul_pair_set
+  have : s • t = (fst ∘ Ψ) '' (fst ⁻¹' s) :=
+    subset_antisymm
+      (smul_subset_iff.mpr fun g hg x hx ↦ mem_image_of_mem (fst ∘ Ψ) (x := ⟨g, ⟨x, hx⟩⟩) hg)
+      (image_subset_iff.mpr fun ⟨g, ⟨x, hx⟩⟩ hg ↦ smul_mem_smul hg hx)
+  rw [this]
+  have : CompactSpace t := isCompact_iff_compactSpace.mp ht
+  exact (isProperMap_fst_of_compactSpace.comp Ψ_proper).isClosedMap _ (hs.preimage continuous_fst)
+
+/-! One may expect `IsClosed.smul_right_of_isCompact` to hold for arbitrary continuous actions,
+but such a lemma can't be true in this level of generality. For a counterexample, consider
+`ℚ` acting on `ℝ` by translation, and let `s : Set ℚ := univ`, `t : set ℝ := {0}`. Then `s` is
+closed and `t` is compact, but `s +ᵥ t` is the set of all rationals, which is definitely not
+closed in `ℝ`. -/