From 2b9b8fc48788e32fd4e8338fbb38e60bcf67513c Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 21 Feb 2024 02:49:41 -0600
Subject: [PATCH 1/5] feat(UniformConvergenceTopology): add
 `UniformOnFun.uniformity_eq` etc

---
 .../UniformConvergenceTopology.lean           | 82 ++++++++++++-------
 1 file changed, 51 insertions(+), 31 deletions(-)

diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
index acd3d351dee01..dc4ff5dde1131 100644
--- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
+++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
@@ -590,7 +590,8 @@ declared as an instance on `α →ᵤ[𝔖] β`. It is defined as the infimum, f
 by `S.restrict`, the map of restriction to `S`, of the uniform structure `𝒰(s, β, uβ)` on
 `↥S →ᵤ β`. We will denote it `𝒱(α, β, 𝔖, uβ)`, where `uβ` is the uniform structure on `β`. -/
 instance uniformSpace : UniformSpace (α →ᵤ[𝔖] β) :=
-  ⨅ (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap s.restrict 𝒰(s, β, _)
+  ⨅ (s : Set α) (_ : s ∈ 𝔖),
+    .comap (UniformFun.ofFun ∘ s.restrict ∘ UniformOnFun.toFun 𝔖) 𝒰(s, β, _)
 
 local notation "𝒱(" α ", " β ", " 𝔖 ", " u ")" => @UniformOnFun.uniformSpace α β u 𝔖
 
@@ -682,6 +683,47 @@ protected theorem uniformContinuous_restrict (h : s ∈ 𝔖) :
 
 variable {α}
 
+/-- A version of `UniformOnFun.hasBasis_uniformity_of_basis`
+with weaker conclusion and weaker assumptions.
+
+We make no assumptions about the set `𝔖`
+but conclude only that the uniformity is equal to some indexed infimum. -/
+protected theorem uniformity_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)}
+    (h : (𝓤 β).HasBasis p V) :
+    𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)) := by
+  simp_rw [iInf_uniformity, uniformity_comap,
+    (UniformFun.hasBasis_uniformity_of_basis _ _ h).eq_biInf, comap_iInf, comap_principal,
+    Function.comp_apply, UniformFun.gen, Subtype.forall]
+  rfl
+
+protected theorem uniformity_eq : 𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V) :=
+  UniformOnFun.uniformity_eq_of_basis _ _ (𝓤 β).basis_sets
+
+protected theorem gen_mem_uniformity (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
+    UniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β) := by
+  rw [UniformOnFun.uniformity_eq]
+  apply_rules [mem_iInf_of_mem, mem_principal_self]
+
+/-- A version of `UniformOnFun.hasBasis_nhds_of_basis`
+with weaker conclusion and weaker assumptions.
+
+We make no assumptions about the set `𝔖`
+but conclude only that the neighbourhoods filter is equal to some indexed infimum. -/
+protected theorem nhds_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)}
+    (h : (𝓤 β).HasBasis p V) (f : α →ᵤ[𝔖] β) :
+    𝓝 f = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V i} := by
+  simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf,
+    comap_principal]; rfl
+
+protected theorem nhds_eq (f : α →ᵤ[𝔖] β) :
+    𝓝 f = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} :=
+  UniformOnFun.nhds_eq_of_basis _ _ (𝓤 β).basis_sets f
+
+protected theorem gen_mem_nhds (f : α →ᵤ[𝔖] β) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
+    {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} ∈ 𝓝 f := by
+  rw [UniformOnFun.nhds_eq]
+  apply_rules [mem_iInf_of_mem, mem_principal_self]
+
 /-- Let `u₁`, `u₂` be two uniform structures on `γ` and `𝔖₁ 𝔖₂ : Set (Set α)`. If `u₁ ≤ u₂` and
 `𝔖₂ ⊆ 𝔖₁` then `𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂)`. -/
 protected theorem mono ⦃u₁ u₂ : UniformSpace γ⦄ (hu : u₁ ≤ u₂) ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄
@@ -775,30 +817,13 @@ Note that one can easily see that assuming `∀ T ∈ 𝔗, ∃ S ∈ 𝔖, f ''
 we will get this for free when we prove that `𝒱(α, β, 𝔖, uβ) = 𝒱(α, β, 𝔖', uβ)` where `𝔖'` is the
 ***noncovering*** bornology generated by `𝔖`. -/
 protected theorem precomp_uniformContinuous {𝔗 : Set (Set γ)} {f : γ → α}
-    (hf : 𝔗 ⊆ image f ⁻¹' 𝔖) :
-    UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (g ∘ f) := by
-  -- Since `comap` distributes on `iInf`, it suffices to prove that
-  -- `⨅ s ∈ 𝔖, comap s.restrict 𝒰(↥s, β, uβ) ≤ ⨅ t ∈ 𝔗, comap (t.restrict ∘ (— ∘ f)) 𝒰(↥t, β, uβ)`.
-  simp_rw [uniformContinuous_iff, UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ←
-    UniformSpace.comap_comap]
-  -- For any `t ∈ 𝔗`, note `s := f '' t ∈ 𝔖`.
-  -- We will show that `comap s.restrict 𝒰(↥s, β, uβ) ≤ comap (t.restrict ∘ (— ∘ f)) 𝒰(↥t, β, uβ)`.
-  refine' le_iInf₂ fun t ht => iInf_le_of_le (f '' t) <| iInf_le_of_le (hf ht) _
-  -- Let `f'` be the map from `t` to `f '' t` induced by `f`.
-  let f' : t → f '' t := (mapsTo_image f t).restrict f t (f '' t)
-  -- By definition `t.restrict ∘ (— ∘ f) = (— ∘ f') ∘ (f '' t).restrict`.
-  have :
-    (t.restrict ∘ fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (g ∘ f)) =
-      (fun g : f '' t → β => g ∘ f') ∘ (f '' t).restrict :=
-    rfl
-  -- Thus, we have to show `comap (f '' t).restrict 𝒰(↥(f '' t), β, uβ) ≤`
-  -- `comap (f '' t).restrict (comap (— ∘ f') 𝒰(↥t, β, uβ))`.
-  rw [this, @UniformSpace.comap_comap (α →ᵤ[𝔖] β) (f '' t →ᵤ β)]
-  -- But this is exactly monotonicity of `comap` applied to
-  -- `UniformFun.precomp_continuous`.
-  refine' UniformSpace.comap_mono _
-  rw [← uniformContinuous_iff]
-  exact UniformFun.precomp_uniformContinuous
+    (hf : MapsTo (f '' ·) 𝔗 𝔖) :
+    UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (toFun 𝔖 g ∘ f) := by
+  simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf, tendsto_principal]
+  intro t ht V hV
+  refine Eventually.filter_mono (biInf_le _ (hf ht)) ?_
+  refine Eventually.filter_mono (biInf_le _ hV) (eventually_principal.2 ?_)
+  exact fun _ ↦ ball_image_iff.1
 #align uniform_on_fun.precomp_uniform_continuous UniformOnFun.precomp_uniformContinuous
 
 /-- Turn a bijection `e : γ ≃ α` such that we have both `∀ T ∈ 𝔗, e '' T ∈ 𝔖` and
@@ -838,12 +863,7 @@ protected theorem uniformContinuous_toFun (h : ⋃₀ 𝔖 = univ) :
 of `TendstoUniformlyOn`) for all `S ∈ 𝔖`. -/
 protected theorem tendsto_iff_tendstoUniformlyOn {F : ι → α →ᵤ[𝔖] β} {f : α →ᵤ[𝔖] β} :
     Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (toFun 𝔖 ∘ F) (toFun 𝔖 f) p s := by
-  rw [UniformOnFun.topologicalSpace_eq, nhds_iInf, tendsto_iInf]
-  refine' forall_congr' fun s => _
-  rw [nhds_iInf, tendsto_iInf]
-  refine' forall_congr' fun hs => _
-  rw [nhds_induced (T := _), tendsto_comap_iff, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe,
-    UniformFun.tendsto_iff_tendstoUniformly]
+  simp only [UniformOnFun.nhds_eq, tendsto_iInf, tendsto_principal]
   rfl
 #align uniform_on_fun.tendsto_iff_tendsto_uniformly_on UniformOnFun.tendsto_iff_tendstoUniformlyOn
 

From 1e1a955e96cbc681e612e692a846ef94fe5e35b2 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 20 Mar 2024 21:29:07 -0500
Subject: [PATCH 2/5] Fix

---
 .../Topology/UniformSpace/UniformConvergenceTopology.lean    | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
index 0c9d1a793b42a..3e6b828157ce4 100644
--- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
+++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
@@ -870,10 +870,9 @@ protected theorem precomp_uniformContinuous {𝔗 : Set (Set γ)} {f : γ → α
     (hf : MapsTo (f '' ·) 𝔗 𝔖) :
     UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (toFun 𝔖 g ∘ f) := by
   simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf, tendsto_principal]
-  intro t ht V hV
-  refine Eventually.filter_mono (biInf_le _ (hf ht)) ?_
+  refine fun t ht V hV ↦ Eventually.filter_mono (biInf_le _ (hf ht)) ?_
   refine Eventually.filter_mono (biInf_le _ hV) (eventually_principal.2 ?_)
-  exact fun _ ↦ ball_image_iff.1
+  exact fun _ ↦ forall_mem_image.1
 #align uniform_on_fun.precomp_uniform_continuous UniformOnFun.precomp_uniformContinuous
 
 /-- Turn a bijection `e : γ ≃ α` such that we have both `∀ T ∈ 𝔗, e '' T ∈ 𝔖` and

From 85e9ac7ff57bdbd951836c007996b0137d24941c Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 21 Apr 2024 13:18:46 -0500
Subject: [PATCH 3/5] Update
 Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
---
 .../Topology/UniformSpace/UniformConvergenceTopology.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
index 3e6b828157ce4..416af59b0ee63 100644
--- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
+++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
@@ -869,10 +869,10 @@ we will get this for free when we prove that `𝒱(α, β, 𝔖, uβ) = 𝒱(α,
 protected theorem precomp_uniformContinuous {𝔗 : Set (Set γ)} {f : γ → α}
     (hf : MapsTo (f '' ·) 𝔗 𝔖) :
     UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (toFun 𝔖 g ∘ f) := by
-  simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf, tendsto_principal]
-  refine fun t ht V hV ↦ Eventually.filter_mono (biInf_le _ (hf ht)) ?_
-  refine Eventually.filter_mono (biInf_le _ hV) (eventually_principal.2 ?_)
-  exact fun _ ↦ forall_mem_image.1
+  simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]
+  refine fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <|
+    tendsto_iInf' V <| tendsto_iInf' hV ?_
+  simpa only [tendsto_principal_principal, UniformOnFun.gen] using fun _ ↦ forall_mem_image.1
 #align uniform_on_fun.precomp_uniform_continuous UniformOnFun.precomp_uniformContinuous
 
 /-- Turn a bijection `e : γ ≃ α` such that we have both `∀ T ∈ 𝔗, e '' T ∈ 𝔖` and

From 57f2488b52d3accca7cf464c9b2773d4e8b87ec1 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 21 Apr 2024 13:21:08 -0500
Subject: [PATCH 4/5] Add a comment

---
 Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
index 3f8dc93bf9f25..2389e25ab80ba 100644
--- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
+++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
@@ -872,6 +872,7 @@ we will get this for free when we prove that `𝒱(α, β, 𝔖, uβ) = 𝒱(α,
 protected theorem precomp_uniformContinuous {𝔗 : Set (Set γ)} {f : γ → α}
     (hf : MapsTo (f '' ·) 𝔗 𝔖) :
     UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (toFun 𝔖 g ∘ f) := by
+  -- This follows from the fact that `(· ∘ f) × (· ∘ f)` maps `gen (f '' t) V` to `gen t V`.
   simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]
   refine fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <|
     tendsto_iInf' V <| tendsto_iInf' hV ?_

From af985f344a359226d5e9670e7cf818cedc86399f Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 21 Apr 2024 15:20:59 -0500
Subject: [PATCH 5/5] Fix

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

diff --git a/Mathlib/Topology/UniformSpace/Ascoli.lean b/Mathlib/Topology/UniformSpace/Ascoli.lean
index d56ca122f174a..85a33eeb55b36 100644
--- a/Mathlib/Topology/UniformSpace/Ascoli.lean
+++ b/Mathlib/Topology/UniformSpace/Ascoli.lean
@@ -218,7 +218,7 @@ theorem EquicontinuousOn.comap_uniformOnFun_eq {𝔖 : Set (Set X)} (𝔖_compac
   -- `K.restrict ∘ F : ι → (K →ᵤ α)` for `K ∈ 𝔖`.
   have H1 : (UniformOnFun.uniformSpace X α 𝔖).comap F =
       ⨅ (K ∈ 𝔖), (UniformFun.uniformSpace _ _).comap (K.restrict ∘ F) := by
-    simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_comap]
+    simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap]; rfl
   -- Now, note that a similar fact is true for the uniform structure on `X → α` induced by
   -- the map `(⋃₀ 𝔖).restrict : (X → α) → ((⋃₀ 𝔖) → α)`: it is equal to the one induced by
   -- all maps `K.restrict : (X → α) → (K → α)` for `K ∈ 𝔖`, which means that the RHS of our