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
diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
index ed9dfb472f78f..2389e25ab80ba 100644
--- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
+++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
@@ -596,7 +596,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 𝔖
 
@@ -735,6 +736,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 α)⦄
@@ -828,30 +870,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
+  -- 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 ?_
+  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
@@ -899,12 +924,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