diff --git a/Mathlib/Topology/UniformSpace/Compact.lean b/Mathlib/Topology/UniformSpace/Compact.lean
index 97c5a9266ef0d..364e8b1bbad26 100644
--- a/Mathlib/Topology/UniformSpace/Compact.lean
+++ b/Mathlib/Topology/UniformSpace/Compact.lean
@@ -169,9 +169,10 @@ def uniformSpaceOfCompactT2 [TopologicalSpace γ] [CompactSpace γ] [T2Space γ]
 continuous. -/
 theorem CompactSpace.uniformContinuous_of_continuous [CompactSpace α] {f : α → β}
     (h : Continuous f) : UniformContinuous f :=
-  have : Tendsto (Prod.map f f) (𝓝ˢ (diagonal α)) (𝓝ˢ (diagonal β)) :=
-    (h.prod_map h).tendsto_nhdsSet mapsTo_prod_map_diagonal
-  (this.mono_left nhdsSet_diagonal_eq_uniformity.ge).mono_right nhdsSet_diagonal_le_uniformity
+calc map (Prod.map f f) (𝓤 α)
+   = map (Prod.map f f) (𝓝ˢ (diagonal α)) := by rw [nhdsSet_diagonal_eq_uniformity]
+ _ ≤ 𝓝ˢ (diagonal β)                      := (h.prod_map h).tendsto_nhdsSet mapsTo_prod_map_diagonal
+ _ ≤ 𝓤 β                                  := nhdsSet_diagonal_le_uniformity
 #align compact_space.uniform_continuous_of_continuous CompactSpace.uniformContinuous_of_continuous
 
 /-- Heine-Cantor: a continuous function on a compact set of a uniform space is uniformly