[Merged by Bors] - feat(Topology/UniformSpace/AbstractCompletion):add comparison lemma

Mathlib/Topology/UniformSpace/AbstractCompletion.lean

@@ -283,6 +283,29 @@
   pkg'.uniformContinuous_compare pkg
 #align abstract_completion.uniform_continuous_compare_equiv_symm AbstractCompletion.uniformContinuous_compareEquiv_symm
 
+/-Let `f : α → β` be a continuous function between a uniform space `α` and a regular topological
+space `γ`, and let `pkg, pkg'` be two abstract completions of `α`. Then
+if for every point `a : pkg` the filter `f.map (coe⁻¹ (𝓝 a))` obtained by pushing forward with `f`
+the preimage in `α` of `𝓝 a` tends to `𝓝 (f.extend a : β)`, then the comparison map
+between `pkg` and `pkg'` composed with the extension of `f` to `pkg`` coincides with the
+extension of `f` to `pkg'` -/
+theorem CompareComp_Compare (γ : Type*) [TopologicalSpace γ] extend_compare_extend
+  [T3Space γ] (f : α → γ) (cont_f : Continuous f) :
+  let _ := pkg.uniformStruct.toTopologicalSpace
+  let _ := pkg'.uniformStruct.toTopologicalSpace
+  (_ : ∀ a : pkg.space,
+    Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.denseInducing.extend f) a))) →
+    pkg.denseInducing.extend f ∘ pkg'.compare pkg = pkg'.denseInducing.extend f := by
+  let _ := pkg'.uniformStruct
+  let _ := pkg.uniformStruct
+  intro _ _ h
+  have : ∀ x : α, (pkg.denseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by
+    simp only [Function.comp_apply, compare_coe, DenseInducing.extend_eq _ cont_f, implies_true]
+  apply (DenseInducing.extend_unique (AbstractCompletion.denseInducing _) this
+    (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous )).symm
+  apply DenseInducing.continuous_extend
+  exact fun a => ⟨(pkg.denseInducing.extend f) a, h a⟩
+
 end Compare
 
 section Prod