feat(UniformGroup): add UniformInducing.uniformGroup (#8813)

Author: urkud

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -110,10 +110,9 @@ theorem strongTopology.embedding_coeFn [UniformSpace F] [UniformAddGroup F] (
 theorem strongUniformity.uniformAddGroup [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) :
     @UniformAddGroup (E →SL[σ] F) (strongUniformity σ F 𝔖) _ := by
   letI : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
-  rw [strongUniformity, UniformSpace.replaceTopology_eq]
   let φ : (E →SL[σ] F) →+ E →ᵤ[𝔖] F :=
     ⟨⟨(FunLike.coe : (E →SL[σ] F) → E →ᵤ[𝔖] F), rfl⟩, fun _ _ => rfl⟩
-  exact uniformAddGroup_comap φ
+  exact (strongUniformity.uniformEmbedding_coeFn _ _ _).uniformAddGroup φ
 #align continuous_linear_map.strong_uniformity.uniform_add_group ContinuousLinearMap.strongUniformity.uniformAddGroup
 
 theorem strongTopology.topologicalAddGroup [TopologicalSpace F] [TopologicalAddGroup F]

Mathlib/Topology/Algebra/UniformGroup.lean

@@ -196,18 +196,6 @@ instance : UniformGroup αᵐᵒᵖ :=
 
 end MulOpposite
 
-namespace Subgroup
-
-@[to_additive]
-instance uniformGroup (S : Subgroup α) : UniformGroup S :=
-  ⟨uniformContinuous_comap'
-      (uniformContinuous_div.comp <|
-        uniformContinuous_subtype_val.prod_map uniformContinuous_subtype_val)⟩
-#align subgroup.uniform_group Subgroup.uniformGroup
-#align add_subgroup.uniform_add_group AddSubgroup.uniformAddGroup
-
-end Subgroup
-
 section LatticeOps
 
 variable [Group β]
@@ -240,17 +228,31 @@ theorem uniformGroup_inf {u₁ u₂ : UniformSpace β} (h₁ : @UniformGroup β
 #align uniform_add_group_inf uniformAddGroup_inf
 
 @[to_additive]
-theorem uniformGroup_comap {γ : Type*} [Group γ] {u : UniformSpace γ} [UniformGroup γ] {F : Type*}
-    [MonoidHomClass F β γ] (f : F) : @UniformGroup β (u.comap f) _ :=
-  letI : UniformSpace β := u.comap f
-  ⟨uniformContinuous_comap' <| by
-    simp_rw [Function.comp, map_div]
-    exact uniformContinuous_div.comp (uniformContinuous_comap.prod_map uniformContinuous_comap)⟩
-#align uniform_group_comap uniformGroup_comap
-#align uniform_add_group_comap uniformAddGroup_comap
+lemma UniformInducing.uniformGroup {γ : Type*} [Group γ] [UniformSpace γ] [UniformGroup γ]
+    [UniformSpace β] {F : Type*} [MonoidHomClass F β γ] (f : F) (hf : UniformInducing f) :
+    UniformGroup β where
+  uniformContinuous_div := by
+    simp_rw [hf.uniformContinuous_iff, Function.comp_def, map_div]
+    exact uniformContinuous_div.comp (hf.uniformContinuous.prod_map hf.uniformContinuous)
+
+@[to_additive]
+protected theorem UniformGroup.comap {γ : Type*} [Group γ] {u : UniformSpace γ} [UniformGroup γ]
+    {F : Type*} [MonoidHomClass F β γ] (f : F) : @UniformGroup β (u.comap f) _ :=
+  letI : UniformSpace β := u.comap f; UniformInducing.uniformGroup f ⟨rfl⟩
+#align uniform_group_comap UniformGroup.comap
+#align uniform_add_group_comap UniformAddGroup.comap
 
 end LatticeOps
 
+namespace Subgroup
+
+@[to_additive]
+instance uniformGroup (S : Subgroup α) : UniformGroup S := .comap S.subtype
+#align subgroup.uniform_group Subgroup.uniformGroup
+#align add_subgroup.uniform_add_group AddSubgroup.uniformAddGroup
+
+end Subgroup
+
 section
 
 variable (α)