chore: don't use TopologicalGroup.toUniformSpace in `tendstoUniform…

…ly_iff` (#19098)

This changes `TopologicalGroup.tendstoUniformly_iff` so that it takes a `UniformSpace` instance instead of only a `TopologicalGroup` instance, along with a proof that the uniform space is the one induced by the topological group structure. The previous version would have been hard to use in case you had, for example, a normed commutative group, as the uniform space structure inferred would not match (defeq) the one given in this theorem, which was previously `TopologicalSpace.toUniformSpace`.

Mathlib/Topology/Algebra/UniformGroup/Basic.lean

@@ -207,37 +207,41 @@ lemma MonoidHom.tendsto_coe_cofinite_of_discrete [T2Space G] {H : Type*} [Group
   replace hf : Function.Injective f.rangeRestrict := by simpa
   exact f.range.tendsto_coe_cofinite_of_discrete.comp hf.tendsto_cofinite
 
+end TopologicalGroup
+
+namespace TopologicalGroup
+
+variable {ι α G : Type*} [Group G] [u : UniformSpace G] [TopologicalGroup G]
+
 @[to_additive]
-theorem TopologicalGroup.tendstoUniformly_iff {ι α : Type*} (F : ι → α → G) (f : α → G)
-    (p : Filter ι) :
-    @TendstoUniformly α G ι (TopologicalGroup.toUniformSpace G) F f p ↔
-      ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a, F i a / f a ∈ u :=
-  ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ =>
-    mem_of_superset (h u hu) fun _ hi a => hv (hi a)⟩
+theorem tendstoUniformly_iff (F : ι → α → G) (f : α → G) (p : Filter ι)
+    (hu : TopologicalGroup.toUniformSpace G = u) :
+    TendstoUniformly F f p ↔ ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a, F i a / f a ∈ u :=
+  hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩,
+    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a => hv (hi a)⟩
 
 @[to_additive]
-theorem TopologicalGroup.tendstoUniformlyOn_iff {ι α : Type*} (F : ι → α → G) (f : α → G)
-    (p : Filter ι) (s : Set α) :
-    @TendstoUniformlyOn α G ι (TopologicalGroup.toUniformSpace G) F f p s ↔
-      ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a ∈ s, F i a / f a ∈ u :=
-  ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ =>
-    mem_of_superset (h u hu) fun _ hi a ha => hv (hi a ha)⟩
+theorem tendstoUniformlyOn_iff (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α)
+    (hu : TopologicalGroup.toUniformSpace G = u) :
+    TendstoUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a ∈ s, F i a / f a ∈ u :=
+  hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩,
+    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a ha => hv (hi a ha)⟩
 
 @[to_additive]
-theorem TopologicalGroup.tendstoLocallyUniformly_iff {ι α : Type*} [TopologicalSpace α]
-    (F : ι → α → G) (f : α → G) (p : Filter ι) :
-    @TendstoLocallyUniformly α G ι (TopologicalGroup.toUniformSpace G) _ F f p ↔
+theorem tendstoLocallyUniformly_iff [TopologicalSpace α] (F : ι → α → G) (f : α → G)
+    (p : Filter ι) (hu : TopologicalGroup.toUniformSpace G = u) :
+    TendstoLocallyUniformly F f p ↔
       ∀ u ∈ 𝓝 (1 : G), ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ i in p, ∀ a ∈ t, F i a / f a ∈ u :=
-    ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
-      Exists.imp (fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩)
-        (h u hu x)⟩
+  hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
+    Exists.imp (fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩)
+      (h u hu x)⟩
 
 @[to_additive]
-theorem TopologicalGroup.tendstoLocallyUniformlyOn_iff {ι α : Type*} [TopologicalSpace α]
-    (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) :
-    @TendstoLocallyUniformlyOn α G ι (TopologicalGroup.toUniformSpace G) _ F f p s ↔
+theorem tendstoLocallyUniformlyOn_iff [TopologicalSpace α] (F : ι → α → G) (f : α → G)
+    (p : Filter ι) (s : Set α) (hu : TopologicalGroup.toUniformSpace G = u) :
+    TendstoLocallyUniformlyOn F f p s ↔
       ∀ u ∈ 𝓝 (1 : G), ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ i in p, ∀ a ∈ t, F i a / f a ∈ u :=
-  ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
+  hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
     (Exists.imp fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩) ∘
       h u hu x⟩