diff --git a/Mathlib.lean b/Mathlib.lean
index 0e396ddb49beb..da7c1291c00ed 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -246,6 +246,7 @@ import Mathlib.Analysis.Normed.Group.BallSphere
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.Analysis.Normed.Group.Completion
 import Mathlib.Analysis.Normed.Group.Hom
+import Mathlib.Analysis.Normed.Group.HomCompletion
 import Mathlib.Analysis.Normed.Group.InfiniteSum
 import Mathlib.Analysis.Normed.Group.Seminorm
 import Mathlib.Analysis.NormedSpace.IndicatorFunction
diff --git a/Mathlib/Analysis/Normed/Group/Hom.lean b/Mathlib/Analysis/Normed/Group/Hom.lean
index 1cbb514e304fb..b8ba7232697f4 100644
--- a/Mathlib/Analysis/Normed/Group/Hom.lean
+++ b/Mathlib/Analysis/Normed/Group/Hom.lean
@@ -84,12 +84,15 @@ variable {V V₁ V₂ V₃ : Type _} [SeminormedAddCommGroup V] [SeminormedAddCo
 
 variable {f g : NormedAddGroupHom V₁ V₂}
 
+/-- A Lipschitz continuous additive homomorphism is a normed additive group homomorphism. -/
+def ofLipschitz (f : V₁ →+ V₂) {K : ℝ≥0} (h : LipschitzWith K f) : NormedAddGroupHom V₁ V₂ :=
+  f.mkNormedAddGroupHom K fun x ↦ by simpa only [map_zero, dist_zero_right] using h.dist_le_mul x 0
+
 -- porting note: moved this declaration up so we could get a `FunLike` instance sooner.
-instance toAddMonoidHomClass : AddMonoidHomClass (NormedAddGroupHom V₁ V₂) V₁ V₂
-    where
+instance toAddMonoidHomClass : AddMonoidHomClass (NormedAddGroupHom V₁ V₂) V₁ V₂ where
   coe := toFun
   coe_injective' := fun f g h => by cases f; cases g; congr
-  map_add f := (AddMonoidHom.mk' f.toFun f.map_add').map_add
+  map_add f := f.map_add'
   map_zero f := (AddMonoidHom.mk' f.toFun f.map_add').map_zero
 
 /-- Helper instance for when there are too many metavariables to apply `FunLike.coeFun` directly. -/
@@ -304,6 +307,12 @@ theorem mkNormedAddGroupHom_norm_le (f : V₁ →+ V₂) {C : ℝ} (hC : 0 ≤ C
   opNorm_le_bound _ hC h
 #align normed_add_group_hom.mk_normed_add_group_hom_norm_le NormedAddGroupHom.mkNormedAddGroupHom_norm_le
 
+/-- If a bounded group homomorphism map is constructed from a group homomorphism via the constructor
+`NormedAddGroupHom.ofLipschitz`, then its norm is bounded by the bound given to the constructor. -/
+theorem ofLipschitz_norm_le (f : V₁ →+ V₂) {K : ℝ≥0} (h : LipschitzWith K f) :
+    ‖ofLipschitz f h‖ ≤ K :=
+  mkNormedAddGroupHom_norm_le f K.coe_nonneg _
+
 /-- If a bounded group homomorphism map is constructed from a group homomorphism
 via the constructor `AddMonoidHom.mkNormedAddGroupHom`, then its norm is bounded by the bound
 given to the constructor or zero if this bound is negative. -/
@@ -802,9 +811,7 @@ def range : AddSubgroup V₂ :=
   f.toAddMonoidHom.range
 #align normed_add_group_hom.range NormedAddGroupHom.range
 
-theorem mem_range (v : V₂) : v ∈ f.range ↔ ∃ w, f w = v := by
-  rw [range, AddMonoidHom.mem_range]
-  rfl
+theorem mem_range (v : V₂) : v ∈ f.range ↔ ∃ w, f w = v := Iff.rfl
 #align normed_add_group_hom.mem_range NormedAddGroupHom.mem_range
 
 @[simp]
diff --git a/Mathlib/Analysis/Normed/Group/HomCompletion.lean b/Mathlib/Analysis/Normed/Group/HomCompletion.lean
new file mode 100644
index 0000000000000..5bfa90995c840
--- /dev/null
+++ b/Mathlib/Analysis/Normed/Group/HomCompletion.lean
@@ -0,0 +1,237 @@
+/-
+Copyright (c) 2021 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot
+
+! This file was ported from Lean 3 source module analysis.normed.group.hom_completion
+! leanprover-community/mathlib commit 17ef379e997badd73e5eabb4d38f11919ab3c4b3
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.Normed.Group.Hom
+import Mathlib.Analysis.Normed.Group.Completion
+
+/-!
+# Completion of normed group homs
+
+Given two (semi) normed groups `G` and `H` and a normed group hom `f : NormedAddGroupHom G H`,
+we build and study a normed group hom
+`f.completion  : NormedAddGroupHom (completion G) (completion H)` such that the diagram
+
+```
+                   f
+     G       ----------->     H
+
+     |                        |
+     |                        |
+     |                        |
+     V                        V
+
+completion G -----------> completion H
+            f.completion
+```
+
+commutes. The map itself comes from the general theory of completion of uniform spaces, but here
+we want a normed group hom, study its operator norm and kernel.
+
+The vertical maps in the above diagrams are also normed group homs constructed in this file.
+
+## Main definitions and results:
+
+* `NormedAddGroupHom.completion`: see the discussion above.
+* `NormedAddCommGroup.toCompl : NormedAddGroupHom G (completion G)`: the canonical map from
+  `G` to its completion, as a normed group hom
+* `NormedAddGroupHom.completion_toCompl`: the above diagram indeed commutes.
+* `NormedAddGroupHom.norm_completion`: `‖f.completion‖ = ‖f‖`
+* `NormedAddGroupHom.ker_le_ker_completion`: the kernel of `f.completion` contains the image of
+  the kernel of `f`.
+* `NormedAddGroupHom.ker_completion`: the kernel of `f.completion` is the closure of the image of
+  the kernel of `f` under an assumption that `f` is quantitatively surjective onto its image.
+* `NormedAddGroupHom.extension` : if `H` is complete, the extension of
+  `f : NormedAddGroupHom G H` to a `NormedAddGroupHom (completion G) H`.
+-/
+
+
+noncomputable section
+
+open Set NormedAddGroupHom UniformSpace
+
+section Completion
+
+variable {G : Type _} [SeminormedAddCommGroup G] {H : Type _} [SeminormedAddCommGroup H]
+  {K : Type _} [SeminormedAddCommGroup K]
+
+/-- The normed group hom induced between completions. -/
+def NormedAddGroupHom.completion (f : NormedAddGroupHom G H) :
+    NormedAddGroupHom (Completion G) (Completion H) :=
+  .ofLipschitz (f.toAddMonoidHom.completion f.continuous) f.lipschitz.completion_map
+#align normed_add_group_hom.completion NormedAddGroupHom.completion
+
+theorem NormedAddGroupHom.completion_def (f : NormedAddGroupHom G H) (x : Completion G) :
+    f.completion x = Completion.map f x :=
+  rfl
+#align normed_add_group_hom.completion_def NormedAddGroupHom.completion_def
+
+@[simp]
+theorem NormedAddGroupHom.completion_coe_to_fun (f : NormedAddGroupHom G H) :
+    (f.completion : Completion G → Completion H) = Completion.map f := rfl
+#align normed_add_group_hom.completion_coe_to_fun NormedAddGroupHom.completion_coe_to_fun
+
+-- porting note: `@[simp]` moved to the next lemma
+theorem NormedAddGroupHom.completion_coe (f : NormedAddGroupHom G H) (g : G) :
+    f.completion g = f g :=
+  Completion.map_coe f.uniformContinuous _
+#align normed_add_group_hom.completion_coe NormedAddGroupHom.completion_coe
+
+@[simp]
+theorem NormedAddGroupHom.completion_coe' (f : NormedAddGroupHom G H) (g : G) :
+    Completion.map f g = f g :=
+  f.completion_coe g
+
+/-- Completion of normed group homs as a normed group hom. -/
+@[simps]
+def normedAddGroupHomCompletionHom :
+    NormedAddGroupHom G H →+ NormedAddGroupHom (Completion G) (Completion H) where
+  toFun := NormedAddGroupHom.completion
+  map_zero' := toAddMonoidHom_injective AddMonoidHom.completion_zero
+  map_add' f g := toAddMonoidHom_injective <|
+    f.toAddMonoidHom.completion_add g.toAddMonoidHom f.continuous g.continuous
+#align normed_add_group_hom_completion_hom normedAddGroupHomCompletionHom
+#align normed_add_group_hom_completion_hom_apply normedAddGroupHomCompletionHom_apply
+
+@[simp]
+theorem NormedAddGroupHom.completion_id :
+    (NormedAddGroupHom.id G).completion = NormedAddGroupHom.id (Completion G) := by
+  ext x
+  rw [NormedAddGroupHom.completion_def, NormedAddGroupHom.coe_id, Completion.map_id]
+  rfl
+#align normed_add_group_hom.completion_id NormedAddGroupHom.completion_id
+
+theorem NormedAddGroupHom.completion_comp (f : NormedAddGroupHom G H) (g : NormedAddGroupHom H K) :
+    g.completion.comp f.completion = (g.comp f).completion := by
+  ext x
+  rw [NormedAddGroupHom.coe_comp, NormedAddGroupHom.completion_def,
+    NormedAddGroupHom.completion_coe_to_fun, NormedAddGroupHom.completion_coe_to_fun,
+    Completion.map_comp g.uniformContinuous f.uniformContinuous]
+  rfl
+#align normed_add_group_hom.completion_comp NormedAddGroupHom.completion_comp
+
+theorem NormedAddGroupHom.completion_neg (f : NormedAddGroupHom G H) :
+    (-f).completion = -f.completion :=
+  map_neg (normedAddGroupHomCompletionHom : NormedAddGroupHom G H →+ _) f
+#align normed_add_group_hom.completion_neg NormedAddGroupHom.completion_neg
+
+theorem NormedAddGroupHom.completion_add (f g : NormedAddGroupHom G H) :
+    (f + g).completion = f.completion + g.completion :=
+  normedAddGroupHomCompletionHom.map_add f g
+#align normed_add_group_hom.completion_add NormedAddGroupHom.completion_add
+
+theorem NormedAddGroupHom.completion_sub (f g : NormedAddGroupHom G H) :
+    (f - g).completion = f.completion - g.completion :=
+  map_sub (normedAddGroupHomCompletionHom : NormedAddGroupHom G H →+ _) f g
+#align normed_add_group_hom.completion_sub NormedAddGroupHom.completion_sub
+
+@[simp]
+theorem NormedAddGroupHom.zero_completion : (0 : NormedAddGroupHom G H).completion = 0 :=
+  normedAddGroupHomCompletionHom.map_zero
+#align normed_add_group_hom.zero_completion NormedAddGroupHom.zero_completion
+
+/-- The map from a normed group to its completion, as a normed group hom. -/
+@[simps] -- porting note: added `@[simps]`
+def NormedAddCommGroup.toCompl : NormedAddGroupHom G (Completion G) where
+  toFun := (↑)
+  map_add' := Completion.toCompl.map_add
+  bound' := ⟨1, by simp [le_refl]⟩
+#align normed_add_comm_group.to_compl NormedAddCommGroup.toCompl
+
+open NormedAddCommGroup
+
+theorem NormedAddCommGroup.norm_toCompl (x : G) : ‖toCompl x‖ = ‖x‖ :=
+  Completion.norm_coe x
+#align normed_add_comm_group.norm_to_compl NormedAddCommGroup.norm_toCompl
+
+theorem NormedAddCommGroup.denseRange_toCompl : DenseRange (toCompl : G → Completion G) :=
+  Completion.denseInducing_coe.dense
+#align normed_add_comm_group.dense_range_to_compl NormedAddCommGroup.denseRange_toCompl
+
+@[simp]
+theorem NormedAddGroupHom.completion_toCompl (f : NormedAddGroupHom G H) :
+    f.completion.comp toCompl = toCompl.comp f := by ext x; simp
+#align normed_add_group_hom.completion_to_compl NormedAddGroupHom.completion_toCompl
+
+@[simp]
+theorem NormedAddGroupHom.norm_completion (f : NormedAddGroupHom G H) : ‖f.completion‖ = ‖f‖ :=
+  le_antisymm (ofLipschitz_norm_le _ _) <| opNorm_le_bound _ (norm_nonneg _) fun x => by
+    simpa using f.completion.le_opNorm x
+#align normed_add_group_hom.norm_completion NormedAddGroupHom.norm_completion
+
+theorem NormedAddGroupHom.ker_le_ker_completion (f : NormedAddGroupHom G H) :
+    (toCompl.comp <| incl f.ker).range ≤ f.completion.ker := by
+  rintro _ ⟨⟨g, h₀ : f g = 0⟩, rfl⟩
+  simp [h₀, mem_ker, Completion.coe_zero]
+#align normed_add_group_hom.ker_le_ker_completion NormedAddGroupHom.ker_le_ker_completion
+
+theorem NormedAddGroupHom.ker_completion {f : NormedAddGroupHom G H} {C : ℝ}
+    (h : f.SurjectiveOnWith f.range C) :
+    (f.completion.ker : Set <| Completion G) = closure (toCompl.comp <| incl f.ker).range := by
+  refine le_antisymm ?_ (closure_minimal f.ker_le_ker_completion f.completion.isClosed_ker)
+  rintro hatg (hatg_in : f.completion hatg = 0)
+  rw [SeminormedAddCommGroup.mem_closure_iff]
+  intro ε ε_pos
+  rcases h.exists_pos with ⟨C', C'_pos, hC'⟩
+  rcases exists_pos_mul_lt ε_pos (1 + C' * ‖f‖) with ⟨δ, δ_pos, hδ⟩
+  obtain ⟨_, ⟨g : G, rfl⟩, hg : ‖hatg - g‖ < δ⟩ :=
+    SeminormedAddCommGroup.mem_closure_iff.mp (Completion.denseInducing_coe.dense hatg) δ δ_pos
+  obtain ⟨g' : G, hgg' : f g' = f g, hfg : ‖g'‖ ≤ C' * ‖f g‖⟩ := hC' (f g) (mem_range_self _ g)
+  have mem_ker : g - g' ∈ f.ker := by rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]
+  refine ⟨_, ⟨⟨g - g', mem_ker⟩, rfl⟩, ?_⟩
+  have : ‖f g‖ ≤ ‖f‖ * δ
+  calc ‖f g‖ ≤ ‖f‖ * ‖hatg - g‖ := by simpa [hatg_in] using f.completion.le_opNorm (hatg - g)
+    _ ≤ ‖f‖ * δ := mul_le_mul_of_nonneg_left hg.le (norm_nonneg f)
+  calc ‖hatg - ↑(g - g')‖ = ‖hatg - g + g'‖ := by rw [Completion.coe_sub, sub_add]
+    _ ≤ ‖hatg - g‖ + ‖(g' : Completion G)‖ := norm_add_le _ _
+    _ = ‖hatg - g‖ + ‖g'‖ := by rw [Completion.norm_coe]
+    _ < δ + C' * ‖f g‖ := add_lt_add_of_lt_of_le hg hfg
+    _ ≤ δ + C' * (‖f‖ * δ) := add_le_add_left (mul_le_mul_of_nonneg_left this C'_pos.le) _
+    _ < ε := by simpa only [add_mul, one_mul, mul_assoc] using hδ
+#align normed_add_group_hom.ker_completion NormedAddGroupHom.ker_completion
+
+end Completion
+
+section Extension
+
+variable {G : Type _} [SeminormedAddCommGroup G]
+
+variable {H : Type _} [SeminormedAddCommGroup H] [SeparatedSpace H] [CompleteSpace H]
+
+/-- If `H` is complete, the extension of `f : NormedAddGroupHom G H` to a
+`NormedAddGroupHom (completion G) H`. -/
+def NormedAddGroupHom.extension (f : NormedAddGroupHom G H) : NormedAddGroupHom (Completion G) H :=
+  .ofLipschitz (f.toAddMonoidHom.extension f.continuous) <|
+    let _ := MetricSpace.ofT0PseudoMetricSpace H
+    f.lipschitz.completion_extension
+#align normed_add_group_hom.extension NormedAddGroupHom.extension
+
+theorem NormedAddGroupHom.extension_def (f : NormedAddGroupHom G H) (v : G) :
+    f.extension v = Completion.extension f v :=
+  rfl
+#align normed_add_group_hom.extension_def NormedAddGroupHom.extension_def
+
+@[simp]
+theorem NormedAddGroupHom.extension_coe (f : NormedAddGroupHom G H) (v : G) : f.extension v = f v :=
+  AddMonoidHom.extension_coe _ f.continuous _
+#align normed_add_group_hom.extension_coe NormedAddGroupHom.extension_coe
+
+theorem NormedAddGroupHom.extension_coe_to_fun (f : NormedAddGroupHom G H) :
+    (f.extension : Completion G → H) = Completion.extension f :=
+  rfl
+#align normed_add_group_hom.extension_coe_to_fun NormedAddGroupHom.extension_coe_to_fun
+
+theorem NormedAddGroupHom.extension_unique (f : NormedAddGroupHom G H)
+    {g : NormedAddGroupHom (Completion G) H} (hg : ∀ v, f v = g v) : f.extension = g := by
+  ext v
+  rw [NormedAddGroupHom.extension_coe_to_fun,
+    Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]
+#align normed_add_group_hom.extension_unique NormedAddGroupHom.extension_unique
+
+end Extension
diff --git a/Mathlib/Topology/MetricSpace/Completion.lean b/Mathlib/Topology/MetricSpace/Completion.lean
index a781553a65f45..b763e95a5654a 100644
--- a/Mathlib/Topology/MetricSpace/Completion.lean
+++ b/Mathlib/Topology/MetricSpace/Completion.lean
@@ -169,8 +169,7 @@ protected theorem uniformity_dist : 𝓤 (Completion α) = ⨅ ε > 0, 𝓟 { p
 #align uniform_space.completion.uniformity_dist UniformSpace.Completion.uniformity_dist
 
 /-- Metric space structure on the completion of a pseudo_metric space. -/
-instance : MetricSpace (Completion α)
-    where
+instance : MetricSpace (Completion α) where
   dist_self := Completion.dist_self
   eq_of_dist_eq_zero := Completion.eq_of_dist_eq_zero _ _
   dist_comm := Completion.dist_comm
@@ -191,3 +190,25 @@ protected theorem edist_eq (x y : α) : edist (x : Completion α) y = edist x y
 #align uniform_space.completion.edist_eq UniformSpace.Completion.edist_eq
 
 end UniformSpace.Completion
+
+open UniformSpace Completion NNReal
+
+theorem LipschitzWith.completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β}
+    {K : ℝ≥0} (h : LipschitzWith K f) : LipschitzWith K (Completion.extension f) :=
+  LipschitzWith.of_dist_le_mul fun x y => induction_on₂ x y
+    (isClosed_le (by continuity) (by continuity)) <| by
+      simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul
+
+theorem LipschitzWith.completion_map [PseudoMetricSpace β] {f : α → β} {K : ℝ≥0}
+    (h : LipschitzWith K f) : LipschitzWith K (Completion.map f) :=
+  one_mul K ▸ (coe_isometry.lipschitz.comp h).completion_extension
+
+theorem Isometry.completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β}
+    (h : Isometry f) : Isometry (Completion.extension f) :=
+  Isometry.of_dist_eq fun x y => induction_on₂ x y
+    (isClosed_eq (by continuity) (by continuity)) fun _ _ ↦ by
+      simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]
+
+theorem Isometry.completion_map [PseudoMetricSpace β] {f : α → β}
+    (h : Isometry f) : Isometry (Completion.map f) :=
+  (coe_isometry.comp h).completion_extension
diff --git a/Mathlib/Topology/UniformSpace/Completion.lean b/Mathlib/Topology/UniformSpace/Completion.lean
index c9f0e115ab948..19ef2512961fa 100644
--- a/Mathlib/Topology/UniformSpace/Completion.lean
+++ b/Mathlib/Topology/UniformSpace/Completion.lean
@@ -546,6 +546,7 @@ theorem uniformContinuous_extension : UniformContinuous (Completion.extension f)
   cPkg.uniformContinuous_extend
 #align uniform_space.completion.uniform_continuous_extension UniformSpace.Completion.uniformContinuous_extension
 
+@[continuity]
 theorem continuous_extension : Continuous (Completion.extension f) :=
   cPkg.continuous_extend
 #align uniform_space.completion.continuous_extension UniformSpace.Completion.continuous_extension
@@ -588,6 +589,7 @@ theorem uniformContinuous_map : UniformContinuous (Completion.map f) :=
   cPkg.uniformContinuous_map cPkg f
 #align uniform_space.completion.uniform_continuous_map UniformSpace.Completion.uniformContinuous_map
 
+@[continuity]
 theorem continuous_map : Continuous (Completion.map f) :=
   cPkg.continuous_map cPkg f
 #align uniform_space.completion.continuous_map UniformSpace.Completion.continuous_map