diff --git a/Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean b/Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean
index 53e7e944072535..8e614833a3f079 100644
--- a/Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean
+++ b/Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean
@@ -73,19 +73,121 @@ theorem isometry_embedding_of_isReal (hv : v.IsReal) :
   AddMonoidHomClass.isometry_of_norm _ fun x ↦ by
     simpa using! v.norm_embedding_of_isReal hv (WithAbs.equiv v.1 x)
 
-/-- The completion of a number field at an infinite place. -/
-abbrev Completion := v.1.Completion
+instance : CompletableTopField (WithAbs v.1) :=
+  v.isometry_embedding.isUniformInducing.completableTopField
+
+/-- The completion of a number field at an infinite place, as a one-field structure wrapping the
+completion `v.1.Completion` of `K` at the underlying absolute value. -/
+structure Completion where
+  /-- Wrap an element of `v.1.Completion` into `v.Completion`. -/
+  ofCompletion ::
+  /-- The underlying element of `v.1.Completion`. -/
+  toCompletion : v.1.Completion
 
 namespace Completion
 
+/-- `Completion.toCompletion` and `Completion.ofCompletion` as an equivalence. -/
+@[simps]
+def equivCompletion : v.Completion ≃ v.1.Completion where
+  toFun := toCompletion
+  invFun := ofCompletion
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+instance : NormedField v.Completion := fast_instance% (equivCompletion v).normedField
+
+/-- `Completion.toCompletion` as a ring isomorphism onto the underlying completion. -/
+@[simps! apply]
+def equiv : v.Completion ≃+* v.1.Completion where
+  toEquiv := equivCompletion v
+  map_mul' _ _ := rfl
+  map_add' _ _ := rfl
+
+@[simp] lemma toCompletion_ofCompletion (x : v.1.Completion) :
+    toCompletion (ofCompletion x : v.Completion) = x := rfl
+
+@[simp] lemma ofCompletion_toCompletion (x : v.Completion) :
+    ofCompletion x.toCompletion = x := rfl
+
+@[ext] theorem ext {v : InfinitePlace K} {x y : v.Completion}
+    (h : x.toCompletion = y.toCompletion) : x = y := by
+  cases x; cases y; exact congrArg ofCompletion h
+
+theorem toCompletion_surjective : Function.Surjective (toCompletion (v := v)) :=
+  (equivCompletion v).surjective
+
+theorem ofCompletion_surjective : Function.Surjective (ofCompletion (v := v)) :=
+  (equivCompletion v).symm.surjective
+
+@[simp] lemma norm_toCompletion (x : v.Completion) : ‖x.toCompletion‖ = ‖x‖ := rfl
+
+@[simp] lemma norm_ofCompletion (x : v.1.Completion) :
+    ‖(ofCompletion x : v.Completion)‖ = ‖x‖ := rfl
+
+theorem isometry_toCompletion : Isometry (toCompletion (v := v)) :=
+  Isometry.of_dist_eq fun _ _ ↦ rfl
+
+/-- `Completion.toCompletion` as an isometry equivalence onto the underlying completion. -/
+def isometryEquivCompletion : v.Completion ≃ᵢ v.1.Completion where
+  toEquiv := equivCompletion v
+  isometry_toFun := isometry_toCompletion v
+
+theorem continuous_toCompletion : Continuous (toCompletion (v := v)) :=
+  (isometry_toCompletion v).continuous
+
+theorem continuous_ofCompletion : Continuous (ofCompletion (v := v)) :=
+  (isometryEquivCompletion v).symm.continuous
+
+instance : CompleteSpace v.Completion :=
+  ((isometry_toCompletion v).isUniformInducing.completeSpace_congr
+    (toCompletion_surjective v)).mpr inferInstance
+
+instance : Inhabited v.Completion := ⟨0⟩
+
+/-- Coercion of an element of `WithAbs v.1` into the completion. -/
+instance : Coe (WithAbs v.1) v.Completion where
+  coe x := ofCompletion (x : v.1.Completion)
+
+/-- Coercion of an element of `K` into the completion. -/
+instance : Coe K v.Completion where
+  coe k := ofCompletion (k : v.1.Completion)
+
+@[simp] lemma coe_toCompletion (x : WithAbs v.1) :
+    (↑x : v.Completion).toCompletion = (x : v.1.Completion) := rfl
+
+theorem continuous_coe : Continuous ((↑) : WithAbs v.1 → v.Completion) :=
+  (continuous_ofCompletion v).comp (UniformSpace.Completion.continuous_coe _)
+
+theorem denseRange_coe : DenseRange ((↑) : WithAbs v.1 → v.Completion) :=
+  (ofCompletion_surjective v).denseRange.comp UniformSpace.Completion.denseRange_coe
+    (continuous_ofCompletion v)
+
+/-- Induction on the completion of a number field at an infinite place: a closed property that
+holds on the image of `K` holds everywhere. -/
+@[elab_as_elim]
+theorem induction_on {p : v.Completion → Prop} (x : v.Completion) (hp : IsClosed {x | p x})
+    (ih : ∀ a : WithAbs v.1, p a) : p x :=
+  UniformSpace.Completion.induction_on (p := fun y ↦ p (ofCompletion y)) x.toCompletion
+    (hp.preimage (continuous_ofCompletion v)) ih
+
+section Algebra
+
+variable (R : Type*) [CommSemiring R] [Algebra R (WithAbs v.1)]
+  [UniformContinuousConstSMul R (WithAbs v.1)]
+
+instance : Algebra R v.Completion := fast_instance% (equivCompletion v).algebra R
+
+theorem algebraMap_toCompletion (r : R) :
+    (algebraMap R v.Completion r).toCompletion = algebraMap R v.1.Completion r := rfl
+
+end Algebra
+
+@[simp] theorem algebraMap_apply (k : K) : algebraMap K v.Completion k = (k : v.Completion) := rfl
 
 lemma norm_coe (x : WithAbs v.1) :
     ‖(x : v.Completion)‖ = v (WithAbs.equiv v.1 x) :=
   UniformSpace.Completion.norm_coe x
 
-instance : CompletableTopField (WithAbs v.1) :=
-  v.isometry_embedding.isUniformInducing.completableTopField
-
 example : NormedField v.Completion := inferInstance
 example : Algebra K v.Completion := inferInstance
 example : IsTopologicalRing v.Completion := inferInstance
@@ -93,8 +195,8 @@ example : IsTopologicalRing v.Completion := inferInstance
 /-- The coercion from the rationals to its completion along an infinite place is `Rat.cast`. -/
 lemma WithAbs.ratCast_equiv (v : InfinitePlace ℚ) (x : WithAbs v.1) :
     Rat.cast (WithAbs.equiv _ x) = (x : v.Completion) :=
-  (eq_ratCast (UniformSpace.Completion.coeRingHom.comp
-    (WithAbs.equiv v.1).symm.toRingHom) _).symm
+  (eq_ratCast ((equiv v).symm.toRingHom.comp (UniformSpace.Completion.coeRingHom.comp
+    (WithAbs.equiv v.1).symm.toRingHom)) _).symm
 
 lemma Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) :
     ‖(x : v.Completion)‖ = |x| := by
@@ -104,14 +206,16 @@ lemma Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) :
 
 /-- The completion of a number field at an infinite place is locally compact. -/
 instance locallyCompactSpace : LocallyCompactSpace (v.Completion) :=
-  AbsoluteValue.Completion.locallyCompactSpace v.isometry_embedding
+  letI := AbsoluteValue.Completion.locallyCompactSpace v.isometry_embedding
+  (isometryEquivCompletion v).toHomeomorph.isClosedEmbedding.locallyCompactSpace
 
 /-- The embedding associated to an infinite place extended to an embedding `v.Completion →+* ℂ`. -/
-def extensionEmbedding : v.Completion →+* ℂ := v.isometry_embedding.extensionHom
+def extensionEmbedding : v.Completion →+* ℂ :=
+  v.isometry_embedding.extensionHom.comp (equiv v).toRingHom
 
 /-- The embedding `K →+* ℝ` associated to a real infinite place extended to `v.Completion →+* ℝ`. -/
 def extensionEmbeddingOfIsReal {v : InfinitePlace K} (hv : IsReal v) : v.Completion →+* ℝ :=
-  (v.isometry_embedding_of_isReal hv).extensionHom
+  (v.isometry_embedding_of_isReal hv).extensionHom.comp (equiv v).toRingHom
 
 @[simp]
 theorem extensionEmbedding_coe (x : WithAbs v.1) :
@@ -123,31 +227,34 @@ theorem extensionEmbeddingOfIsReal_coe {v : InfinitePlace K} (hv : IsReal v) (x
     extensionEmbeddingOfIsReal hv x = embedding_of_isReal hv (WithAbs.equiv v.1 x) :=
   (v.isometry_embedding_of_isReal hv).extensionHom_coe _
 
-open UniformSpace.Completion in
-@[simp]
-theorem extensionEmbeddingOfIsReal_apply {v : InfinitePlace K} (hv : IsReal v) (x : v.Completion) :
-    (extensionEmbeddingOfIsReal hv x : ℂ) = extensionEmbedding v x := by
-  refine UniformSpace.Completion.induction_on x ?_ (by simp)
-  exact isClosed_eq (Continuous.comp' (by fun_prop) continuous_extension) continuous_extension
-
 /-- The embedding `v.Completion →+* ℂ` is an isometry. -/
 theorem isometry_extensionEmbedding : Isometry (extensionEmbedding v) :=
-  v.isometry_embedding.completion_extension
+  v.isometry_embedding.completion_extension.comp (isometry_toCompletion v)
 
 /-- The embedding `v.Completion →+* ℝ` at a real infinite place is an isometry. -/
 theorem isometry_extensionEmbeddingOfIsReal {v : InfinitePlace K} (hv : IsReal v) :
     Isometry (extensionEmbeddingOfIsReal hv) :=
-  (v.isometry_embedding_of_isReal hv).completion_extension
+  (v.isometry_embedding_of_isReal hv).completion_extension.comp (isometry_toCompletion v)
+
+@[simp]
+theorem extensionEmbeddingOfIsReal_apply {v : InfinitePlace K} (hv : IsReal v) (x : v.Completion) :
+    (extensionEmbeddingOfIsReal hv x : ℂ) = extensionEmbedding v x := by
+  induction x using induction_on with
+  | hp =>
+    exact isClosed_eq
+      (Complex.continuous_ofReal.comp (isometry_extensionEmbeddingOfIsReal hv).continuous)
+      (isometry_extensionEmbedding v).continuous
+  | ih a => simp
 
 /-- The embedding `v.Completion →+* ℂ` has closed image inside `ℂ`. -/
 theorem isClosed_image_extensionEmbedding : IsClosed (Set.range (extensionEmbedding v)) :=
-  v.isometry_embedding.completion_extension.isClosedEmbedding.isClosed_range
+  (isometry_extensionEmbedding v).isClosedEmbedding.isClosed_range
 
 /-- The embedding `v.Completion →+* ℝ` associated to a real infinite place has closed image
 inside `ℝ`. -/
 theorem isClosed_image_extensionEmbeddingOfIsReal {v : InfinitePlace K} (hv : IsReal v) :
     IsClosed (Set.range (extensionEmbeddingOfIsReal hv)) :=
-  (v.isometry_embedding_of_isReal hv).completion_extension.isClosedEmbedding.isClosed_range
+  (isometry_extensionEmbeddingOfIsReal hv).isClosedEmbedding.isClosed_range
 
 theorem subfield_ne_real_of_isComplex {v : InfinitePlace K} (hv : IsComplex v) :
     (extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange := by
@@ -211,13 +318,18 @@ def isometryEquivRealOfIsReal {v : InfinitePlace K} (hv : IsReal v) : v.Completi
 variable {L : Type*} [Field L] [Algebra K L] (w : InfinitePlace L) {v}
   [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion]
 
-set_option backward.isDefEq.respectTransparency false in
+omit [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] in
+theorem coe_algebraMap (x : WithAbs v.1) :
+    algebraMap (WithAbs v.1) w.Completion x = ↑(algebraMap (WithAbs v.1) (WithAbs w.1) x) := by
+  apply ext
+  rw [algebraMap_toCompletion]
+  exact UniformSpace.Completion.algebraMap_def (WithAbs w.1) (WithAbs v.1) x
+
 @[simp]
 theorem algebraMap_coe (x : WithAbs v.1) :
-    algebraMap v.Completion w.Completion x = algebraMap (WithAbs v.1) (WithAbs w.1) x := by
-  have := IsScalarTower.algebraMap_apply (WithAbs v.1) v.Completion w.Completion x
-  rw [algebraMap_def] at this
-  simp [this, algebraMap_def, Algebra.algebraMap_self]
+    algebraMap v.Completion w.Completion x = algebraMap (WithAbs v.1) (WithAbs w.1) x :=
+  (IsScalarTower.algebraMap_apply (WithAbs v.1) v.Completion w.Completion x).symm.trans
+    (coe_algebraMap w x)
 
 end Completion
 
@@ -240,8 +352,9 @@ theorem liesOver_extensionEmbedding [ContinuousSMul v.Completion w.Completion]
     ext x
     induction x using induction_on
     · exact isClosed_eq
-        (continuous_extension.comp (continuous_algebraMap v.Completion w.Completion))
-        continuous_extension
+        ((isometry_extensionEmbedding w).continuous.comp
+          (continuous_algebraMap v.Completion w.Completion))
+        (isometry_extensionEmbedding v).continuous
     · simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply,
         ← ComplexEmbedding.LiesOver.over w.embedding v.embedding]
 
@@ -252,8 +365,9 @@ theorem liesOver_conjugate_extensionEmbedding [ContinuousSMul v.Completion w.Com
     ext x
     induction x using induction_on
     · simpa using! isClosed_eq (.comp (by fun_prop)
-        (continuous_extension.comp <| continuous_algebraMap v.Completion w.Completion))
-        continuous_extension
+          ((isometry_extensionEmbedding w).continuous.comp <|
+            continuous_algebraMap v.Completion w.Completion))
+        (isometry_extensionEmbedding v).continuous
     · simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply,
         ← ComplexEmbedding.LiesOver.over (conjugate w.embedding) v.embedding]
 
diff --git a/Mathlib/NumberTheory/NumberField/Completion/LiesOverInstances.lean b/Mathlib/NumberTheory/NumberField/Completion/LiesOverInstances.lean
index 505f6f53fb1e66..61bd2a56112998 100644
--- a/Mathlib/NumberTheory/NumberField/Completion/LiesOverInstances.lean
+++ b/Mathlib/NumberTheory/NumberField/Completion/LiesOverInstances.lean
@@ -21,23 +21,39 @@ public section
 
 namespace NumberField.LiesOver
 
-open UniformSpace.Completion InfinitePlace
+open InfinitePlace InfinitePlace.Completion
 
 variable {K L : Type*} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L}
 variable [w.1.LiesOver v.1]
 
+/-- The ring homomorphism `v.Completion →+* w.Completion` induced by `algebraMap K L`, when `w`
+lies over `v`. -/
+noncomputable def completionMap : v.Completion →+* w.Completion :=
+  ((Completion.equiv w).symm.toRingHom.comp
+    (LiesOver.isometry_algebraMap w v).mapRingHom).comp (Completion.equiv v).toRingHom
+
+theorem continuous_completionMap : Continuous (completionMap (v := v) (w := w)) :=
+  (continuous_ofCompletion w).comp <|
+    UniformSpace.Completion.continuous_map.comp (continuous_toCompletion v)
+
+theorem completionMap_coe (x : WithAbs v.1) :
+    completionMap (x : v.Completion) = ((algebraMap (WithAbs v.1) (WithAbs w.1) x : WithAbs w.1) :
+      w.Completion) :=
+  Completion.ext <| (LiesOver.isometry_algebraMap w v).mapRingHom_coe x
+
 /-- If `w` lies over `v`, then `w.Completion` is a `v.Completion`-algebra. -/
-noncomputable scoped instance : Algebra v.Completion w.Completion :=
-  (LiesOver.isometry_algebraMap w v).mapRingHom.toAlgebra
+noncomputable scoped instance : Algebra v.Completion w.Completion := completionMap.toAlgebra
 
 scoped instance : IsScalarTower K v.Completion w.Completion :=
   .of_algebraMap_eq fun x ↦ by
-    simp_rw [RingHom.algebraMap_toAlgebra, UniformSpace.Completion.algebraMap_def,
-      Isometry.mapRingHom_coe]
+    have h : algebraMap K v.Completion x = ((WithAbs.toAbs v.1 x : WithAbs v.1) : v.Completion) :=
+      rfl
+    rw [RingHom.algebraMap_toAlgebra, h, completionMap_coe]
+    apply Completion.ext
+    rw [Completion.algebraMap_toCompletion, UniformSpace.Completion.algebraMap_def]
     simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply]
 
 scoped instance : ContinuousSMul v.Completion w.Completion where
-  continuous_smul := (UniformSpace.Completion.continuous_map.comp continuous_fst).mul
-    (Continuous.comp continuous_id continuous_snd)
+  continuous_smul := (continuous_completionMap.comp continuous_fst).mul continuous_snd
 
 end NumberField.LiesOver
diff --git a/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean b/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean
index 1813f5a678c2f4..a1cd977f3b3738 100644
--- a/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean
+++ b/Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean
@@ -102,9 +102,8 @@ theorem mixedEmbedding_eq_algebraMap_comp {x : K} :
 The number field $K$ is dense in the infinite adele ring $\prod_v K_v$.
 -/
 theorem denseRange_algebraMap [NumberField K] : DenseRange <| algebraMap K (InfiniteAdeleRing K) :=
-  (DenseRange.piMap fun _ => UniformSpace.Completion.denseRange_coe).comp
-    (InfinitePlace.denseRange_algebraMap_pi K)
-      (.piMap fun _ => UniformSpace.Completion.continuous_coe _)
+  (DenseRange.piMap fun v => Completion.denseRange_coe v).comp
+    (InfinitePlace.denseRange_algebraMap_pi K) (.piMap fun v => Completion.continuous_coe v)
 
 /-- The norm on the infinite adele ring is given by the product of the normalized norms
 across infinite places. The normalized norm is the real norm at real places and the