From 368923da0362e039715c44e27d5a1e8ec02d43c9 Mon Sep 17 00:00:00 2001
From: Anatole Dedecker <anatolededecker@gmail.com>
Date: Mon, 21 Aug 2023 11:54:42 +0000
Subject: [PATCH] feat: behavior of `Cauchy` under operations on `UniformSpace`
 (#6694)

Some of the lemmas are cherry-picked from leanprover-community/mathlib#17975 and will be useful for the general Arzela-Ascoli theorem, but I also filled some API holes on the way.
---
 Mathlib/Topology/UniformSpace/Cauchy.lean | 47 ++++++++++++++++++-----
 Mathlib/Topology/UniformSpace/Pi.lean     | 37 +++++++++++-------
 2 files changed, 62 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean
index 276e98d544530..ecdc6154e0d31 100644
--- a/Mathlib/Topology/UniformSpace/Cauchy.lean
+++ b/Mathlib/Topology/UniformSpace/Cauchy.lean
@@ -20,7 +20,7 @@ open Filter TopologicalSpace Set Classical UniformSpace Function
 
 open Classical Uniformity Topology Filter
 
-variable {α : Type u} {β : Type v} [UniformSpace α]
+variable {α : Type u} {β : Type v} [uniformSpace : UniformSpace α]
 
 /-- A filter `f` is Cauchy if for every entourage `r`, there exists an
   `s ∈ f` such that `s × s ⊆ r`. This is a generalization of Cauchy
@@ -54,6 +54,10 @@ theorem cauchy_iff {f : Filter α} : Cauchy f ↔ NeBot f ∧ ∀ s ∈ 𝓤 α,
     simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, ball_mem_comm]
 #align cauchy_iff cauchy_iff
 
+lemma cauchy_iff_le {l : Filter α} [hl : l.NeBot] :
+    Cauchy l ↔ l ×ˢ l ≤ 𝓤 α := by
+  simp only [Cauchy, hl, true_and]
+
 theorem Cauchy.ultrafilter_of {l : Filter α} (h : Cauchy l) :
     Cauchy (@Ultrafilter.of _ l h.1 : Filter α) := by
   haveI := h.1
@@ -92,13 +96,40 @@ theorem Filter.Tendsto.cauchy_map {l : Filter β} [NeBot l] {f : β → α} {a :
   cauchy_nhds.mono h
 #align filter.tendsto.cauchy_map Filter.Tendsto.cauchy_map
 
+lemma Cauchy.mono_uniformSpace {u v : UniformSpace β} {F : Filter β} (huv : u ≤ v)
+    (hF : Cauchy (uniformSpace := u) F) : Cauchy (uniformSpace := v) F :=
+  ⟨hF.1, hF.2.trans huv⟩
+
+lemma cauchy_inf_uniformSpace {u v : UniformSpace β} {F : Filter β} :
+    Cauchy (uniformSpace := u ⊓ v) F ↔
+    Cauchy (uniformSpace := u) F ∧ Cauchy (uniformSpace := v) F := by
+  unfold Cauchy
+  rw [inf_uniformity (u := u), le_inf_iff, and_and_left]
+
+lemma cauchy_iInf_uniformSpace {ι : Sort*} [Nonempty ι] {u : ι → UniformSpace β}
+    {l : Filter β} :
+    Cauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l := by
+  unfold Cauchy
+  rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]
+
+lemma cauchy_iInf_uniformSpace' {ι : Sort*} {u : ι → UniformSpace β}
+    {l : Filter β} [l.NeBot] :
+    Cauchy (uniformSpace := ⨅ i, u i) l ↔ ∀ i, Cauchy (uniformSpace := u i) l := by
+  simp_rw [cauchy_iff_le (uniformSpace := _), iInf_uniformity, le_iInf_iff]
+
+lemma cauchy_comap_uniformSpace {u : UniformSpace β} {f : α → β} {l : Filter α} :
+    Cauchy (uniformSpace := comap f u) l ↔ Cauchy (map f l) := by
+  simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap]
+  rfl
+
+lemma cauchy_prod_iff [UniformSpace β] {F : Filter (α × β)} :
+    Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F) := by
+  simp_rw [instUniformSpaceProd, ← cauchy_comap_uniformSpace, ← cauchy_inf_uniformSpace]
+
 theorem Cauchy.prod [UniformSpace β] {f : Filter α} {g : Filter β} (hf : Cauchy f) (hg : Cauchy g) :
     Cauchy (f ×ˢ g) := by
-  refine' ⟨hf.1.prod hg.1, _⟩
-  simp only [uniformity_prod, le_inf_iff, ← map_le_iff_le_comap, ← prod_map_map_eq]
-  exact
-    ⟨le_trans (prod_mono tendsto_fst tendsto_fst) hf.2,
-      le_trans (prod_mono tendsto_snd tendsto_snd) hg.2⟩
+  have := hf.1; have := hg.1
+  simpa [cauchy_prod_iff, hf.1] using ⟨hf, hg⟩
 #align cauchy.prod Cauchy.prod
 
 /-- The common part of the proofs of `le_nhds_of_cauchy_adhp` and
@@ -379,9 +410,7 @@ instance CompleteSpace.prod [UniformSpace β] [CompleteSpace α] [CompleteSpace
   complete hf :=
     let ⟨x1, hx1⟩ := CompleteSpace.complete <| hf.map uniformContinuous_fst
     let ⟨x2, hx2⟩ := CompleteSpace.complete <| hf.map uniformContinuous_snd
-    ⟨(x1, x2), by
-      rw [nhds_prod_eq, Filter.prod_def]
-      exact Filter.le_lift.2 fun s hs => Filter.le_lift'.2 fun t ht => inter_mem (hx1 hs) (hx2 ht)⟩
+    ⟨(x1, x2), by rw [nhds_prod_eq, le_prod]; constructor <;> assumption⟩
 #align complete_space.prod CompleteSpace.prod
 
 @[to_additive]
diff --git a/Mathlib/Topology/UniformSpace/Pi.lean b/Mathlib/Topology/UniformSpace/Pi.lean
index ef2705c087e10..bd62099175ae9 100644
--- a/Mathlib/Topology/UniformSpace/Pi.lean
+++ b/Mathlib/Topology/UniformSpace/Pi.lean
@@ -19,19 +19,22 @@ open Uniformity Topology
 
 section
 
-open Filter UniformSpace
+open Filter UniformSpace Function
 
 universe u
 
 variable {ι : Type*} (α : ι → Type u) [U : ∀ i, UniformSpace (α i)]
 
-
 instance Pi.uniformSpace : UniformSpace (∀ i, α i) :=
   UniformSpace.ofCoreEq (⨅ i, UniformSpace.comap (fun a : ∀ i, α i => a i) (U i)).toCore
       Pi.topologicalSpace <|
     Eq.symm toTopologicalSpace_iInf
 #align Pi.uniform_space Pi.uniformSpace
 
+lemma Pi.uniformSpace_eq :
+    Pi.uniformSpace α = ⨅ i, UniformSpace.comap (fun a : (∀ i, α i) ↦ a i) (U i) := by
+  ext : 1; rfl
+
 theorem Pi.uniformity :
     𝓤 (∀ i, α i) = ⨅ i : ι, (Filter.comap fun a => (a.1 i, a.2 i)) (𝓤 (α i)) :=
   iInf_uniformity
@@ -51,18 +54,26 @@ theorem Pi.uniformContinuous_proj (i : ι) : UniformContinuous fun a : ∀ i : 
   uniformContinuous_pi.1 uniformContinuous_id i
 #align Pi.uniform_continuous_proj Pi.uniformContinuous_proj
 
-instance Pi.complete [∀ i, CompleteSpace (α i)] : CompleteSpace (∀ i, α i) :=
-  ⟨by
-    intro f hf
-    haveI := hf.1
-    have : ∀ i, ∃ x : α i, Filter.map (fun a : ∀ i, α i => a i) f ≤ 𝓝 x := by
-      intro i
-      have key : Cauchy (map (fun a : ∀ i : ι, α i => a i) f) :=
-        hf.map (Pi.uniformContinuous_proj α i)
-      exact cauchy_iff_exists_le_nhds.1 key
-    choose x hx using this
+lemma cauchy_pi_iff [Nonempty ι] {l : Filter (∀ i, α i)} :
+    Cauchy l ↔ ∀ i, Cauchy (map (eval i) l) := by
+  simp_rw [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace, cauchy_comap_uniformSpace]
+
+lemma cauchy_pi_iff' {l : Filter (∀ i, α i)} [l.NeBot] :
+    Cauchy l ↔ ∀ i, Cauchy (map (eval i) l) := by
+  simp_rw [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace', cauchy_comap_uniformSpace]
+
+lemma Cauchy.pi [Nonempty ι] {l : ∀ i, Filter (α i)} (hl : ∀ i, Cauchy (l i)) :
+    Cauchy (Filter.pi l) := by
+  have := fun i ↦ (hl i).1
+  simpa [cauchy_pi_iff]
+
+instance Pi.complete [∀ i, CompleteSpace (α i)] : CompleteSpace (∀ i, α i) where
+  complete {f} hf := by
+    have := hf.1
+    simp_rw [cauchy_pi_iff', cauchy_iff_exists_le_nhds] at hf
+    choose x hx using hf
     use x
-    rwa [nhds_pi, le_pi]⟩
+    rwa [nhds_pi, le_pi]
 #align Pi.complete Pi.complete
 
 instance Pi.separated [∀ i, SeparatedSpace (α i)] : SeparatedSpace (∀ i, α i) :=