diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean
index 6ffb2a121b1f5b..8b361b40dc6528 100644
--- a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean
+++ b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean
@@ -81,9 +81,9 @@ instance : IsDiscreteValuationRing (v.adicCompletionIntegers K) where
       ZeroMemClass.coe_zero, Subtype.forall, Valuation.mem_valuationSubring_iff, not_forall,
       exists_prop]
     obtain ⟨π, hπ⟩ := v.valuation_exists_uniformizer K
-    use π
+    use (WithVal.equiv (v.valuation K)).symm π
     simp [hπ, ← exp_zero, -exp_neg,
-          ← (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰).map_eq_zero_iff]
+      ← (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰).map_eq_zero_iff]
 
 end DVR
 
@@ -130,8 +130,8 @@ variable {K : Type*} [Field K] [NumberField K] (v : HeightOneSpectrum (𝓞 K))
 open RingOfIntegers.HeightOneSpectrum
 
 /-- The embedding of a number field inside its completion with respect to `v`. -/
-noncomputable def FinitePlace.embedding : WithVal (v.valuation K) →+* adicCompletion K v :=
-  UniformSpace.Completion.coeRingHom
+noncomputable def FinitePlace.embedding : K →+* adicCompletion K v :=
+  UniformSpace.Completion.coeRingHom.comp (WithVal.equiv (v.valuation K)).symm
 
 theorem FinitePlace.embedding_apply (x : K) : embedding v x = ↑x := rfl
 
@@ -167,7 +167,7 @@ noncomputable def FinitePlace.mk (v : HeightOneSpectrum (𝓞 K)) : FinitePlace
   ⟨place (embedding v), ⟨v, rfl⟩⟩
 
 lemma toNNReal_valued_eq_adicAbv (x : WithVal (v.valuation K)) :
-    toNNReal (absNorm_ne_zero v) (Valued.v x) = adicAbv v x := rfl
+    toNNReal (absNorm_ne_zero v) (Valued.v x) = adicAbv v (WithVal.equiv _ x) := rfl
 
 /-- A predicate singling out finite places among the absolute values on a number field `K`. -/
 def IsFinitePlace (w : AbsoluteValue K ℝ) : Prop :=
@@ -182,21 +182,22 @@ lemma isFinitePlace_iff (v : AbsoluteValue K ℝ) :
 
 /-- The norm of the image after the embedding associated to `v` is equal to the `v`-adic absolute
 value. -/
-theorem FinitePlace.norm_def (x : WithVal (v.valuation K)) : ‖embedding v x‖ = adicAbv v x := by
+theorem FinitePlace.norm_def (x : K) :
+    ‖embedding v x‖ = adicAbv v x := by
   simp [NormedField.toNorm, instNormedFieldValuedAdicCompletion, Valued.toNormedField, Valued.norm,
-    Valuation.RankOne.hom, embedding_apply, ← toNNReal_valued_eq_adicAbv]
+    Valuation.RankOne.hom, embedding_apply, adicAbv_def]
 
 /-- The norm of the image after the embedding associated to `v` is equal to the norm of `v` raised
 to the power of the `v`-adic valuation. -/
-theorem FinitePlace.norm_def' (x : WithVal (v.valuation K)) :
+theorem FinitePlace.norm_def' (x : K) :
     ‖embedding v x‖ = toNNReal (absNorm_ne_zero v) (v.valuation K x) := by
   rw [norm_def, adicAbv_def]
 
 /-- The norm of the image after the embedding associated to `v` is equal to the norm of `v` raised
 to the power of the `v`-adic valuation for integers. -/
-theorem FinitePlace.norm_def_int (x : 𝓞 (WithVal (v.valuation K))) :
+theorem FinitePlace.norm_def_int (x : 𝓞 K) :
     ‖embedding v x‖ = toNNReal (absNorm_ne_zero v) (v.intValuation x) := by
-  rw [norm_def, adicAbv_def, valuation_of_algebraMap]
+  simp [norm_def, adicAbv_def, valuation_of_algebraMap]
 
 /-- The `v`-adic absolute value satisfies the ultrametric inequality. -/
 theorem RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max (x y : K) :
@@ -213,18 +214,18 @@ theorem RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one (n : ℤ) : adic
 open FinitePlace
 
 /-- The `v`-adic norm of an integer is at most 1. -/
-theorem FinitePlace.norm_le_one (x : 𝓞 (WithVal (v.valuation K))) : ‖embedding v x‖ ≤ 1 := by
+theorem FinitePlace.norm_le_one (x : 𝓞 K) : ‖embedding v x‖ ≤ 1 := by
   rw [norm_def]
   exact v.adicAbv_coe_le_one (one_lt_absNorm_nnreal v) x
 
 /-- The `v`-adic norm of an integer is 1 if and only if it is not in the ideal. -/
-theorem FinitePlace.norm_eq_one_iff_notMem (x : 𝓞 (WithVal (v.valuation K))) :
+theorem FinitePlace.norm_eq_one_iff_notMem (x : 𝓞 K) :
     ‖embedding v x‖ = 1 ↔ x ∉ v.asIdeal := by
   rw [norm_def]
   exact v.adicAbv_coe_eq_one_iff (one_lt_absNorm_nnreal v) x
 
 /-- The `v`-adic norm of an integer is less than 1 if and only if it is in the ideal. -/
-theorem FinitePlace.norm_lt_one_iff_mem (x : 𝓞 (WithVal (v.valuation K))) :
+theorem FinitePlace.norm_lt_one_iff_mem (x : 𝓞 K) :
     ‖embedding v x‖ < 1 ↔ x ∈ v.asIdeal := by
   rw [norm_def]
   exact v.adicAbv_coe_lt_one_iff (one_lt_absNorm_nnreal v) x
@@ -350,7 +351,7 @@ lemma equivHeightOneSpectrum_symm_apply (v : HeightOneSpectrum (𝓞 K)) (x : K)
     (equivHeightOneSpectrum.symm v) x = ‖embedding v x‖ := rfl
 
 open Ideal in
-lemma embedding_mul_absNorm (v : HeightOneSpectrum (𝓞 K)) {x : 𝓞 (WithVal (v.valuation K))}
+lemma embedding_mul_absNorm (v : HeightOneSpectrum (𝓞 K)) {x : 𝓞 K}
     (h_x_nezero : x ≠ 0) : ‖embedding v x‖ * absNorm (v.maxPowDividing (span {x})) = 1 := by
   rw [maxPowDividing, map_pow, Nat.cast_pow, norm_def, adicAbv_def,
     WithZeroMulInt.toNNReal_neg_apply _
diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
index fb8a0d03861c08..f3e6c453edd405 100644
--- a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
+++ b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
@@ -416,7 +416,8 @@ theorem adicValued_apply {x : K} : v.adicValued.v x = v.valuation K x :=
   rfl
 
 @[simp]
-theorem adicValued_apply' (x : WithVal (v.valuation K)) : v.adicValued.v x = v.valuation K x :=
+theorem adicValued_apply' (x : WithVal (v.valuation K)) :
+    v.adicValued.v x = v.valuation K (WithVal.equiv _ x) :=
   rfl
 
 variable (K)
@@ -470,21 +471,14 @@ instance : Algebra S (v.adicCompletion K) where
   algebraMap := Completion.coeRingHom.comp (algebraMap _ _)
   commutes' r x := by
     induction x using Completion.induction_on with
-    | hp =>
-      exact isClosed_eq (continuous_mul_left _) (continuous_mul_right _)
-    | ih x =>
-      change (↑(algebraMap S (WithVal <| v.valuation K) r) : v.adicCompletion K) * x
-        = x * (↑(algebraMap S (WithVal <| v.valuation K) r) : v.adicCompletion K)
-      norm_cast
-      rw [Algebra.commutes]
+    | hp => exact isClosed_eq (continuous_mul_left _) (continuous_mul_right _)
+    | ih x => rw [mul_comm]
   smul_def' r x := by
     induction x using Completion.induction_on with
-    | hp =>
-      exact isClosed_eq (continuous_const_smul _) (continuous_mul_left _)
+    | hp => exact isClosed_eq (continuous_const_smul _) (continuous_mul_left _)
     | ih x =>
-      change _ = (↑(algebraMap S (WithVal <| v.valuation K) r) : v.adicCompletion K) * x
-      norm_cast
-      rw [← Algebra.smul_def]
+      simp [Algebra.smul_def, Completion.algebraMap_def, WithVal.algebraMap_apply,
+        Completion.coeRingHom]
 
 theorem coe_smul_adicCompletion (r : S) (x : WithVal (v.valuation K)) :
     (↑(r • x) : v.adicCompletion K) = r • (↑x : v.adicCompletion K) :=
@@ -526,7 +520,7 @@ instance : Algebra R (v.adicCompletionIntegers K) where
 
 @[simp]
 lemma algebraMap_adicCompletionIntegers_apply (r : R) :
-    algebraMap R (v.adicCompletionIntegers K) r = (algebraMap R K r : v.adicCompletion K) :=
+    algebraMap R (v.adicCompletionIntegers K) r = (algebraMap R K r : v.adicCompletion K) := by
   rfl
 
 instance [FaithfulSMul R K] : FaithfulSMul R (v.adicCompletionIntegers K) := by
@@ -539,14 +533,14 @@ open scoped algebraMap in -- to make the coercions from `R` fire
 /-- The valuation on the completion agrees with the global valuation on elements of the
 integer ring. -/
 theorem valuedAdicCompletion_eq_valuation (r : R) :
-    Valued.v (r : v.adicCompletion K) = v.valuation K r := by
-  convert Valued.valuedCompletion_apply (r : K)
+    Valued.v (r : v.adicCompletion K) = v.valuation K r :=
+  Valued.valuedCompletion_apply _
 
 variable {R K} in
 /-- The valuation on the completion agrees with the global valuation on elements of the field. -/
 theorem valuedAdicCompletion_eq_valuation' (k : K) :
-    Valued.v (k : v.adicCompletion K) = v.valuation K k := by
-  convert Valued.valuedCompletion_apply k
+    Valued.v (k : v.adicCompletion K) = v.valuation K k :=
+  Valued.valuedCompletion_apply _
 
 variable {R K} in
 open scoped algebraMap in -- to make the coercion from `R` fire
diff --git a/Mathlib/Topology/Algebra/Valued/WithVal.lean b/Mathlib/Topology/Algebra/Valued/WithVal.lean
index ea3df92b768948..fe1136834c6a7f 100644
--- a/Mathlib/Topology/Algebra/Valued/WithVal.lean
+++ b/Mathlib/Topology/Algebra/Valued/WithVal.lean
@@ -45,7 +45,7 @@ namespace WithVal
 
 section Instances
 
-variable {P S : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+variable {P S : Type*}
 
 instance [Ring R] (v : Valuation R Γ₀) : Ring (WithVal v) := inferInstanceAs (Ring R)
 
@@ -55,42 +55,60 @@ instance [Field R] (v : Valuation R Γ₀) : Field (WithVal v) := inferInstanceA
 
 instance [Ring R] (v : Valuation R Γ₀) : Inhabited (WithVal v) := ⟨0⟩
 
-instance [CommSemiring S] [CommRing R] [Algebra S R] (v : Valuation R Γ₀) :
-    Algebra S (WithVal v) := inferInstanceAs (Algebra S R)
+instance [Ring R] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+    {v : Valuation R Γ₀} : Preorder (WithVal v) := v.toPreorder
+
+end Instances
+
+section Ring
+
+variable [Ring R] (v : Valuation R Γ₀)
+
+/-- Canonical ring equivalence between `WithVal v` and `R`. -/
+def equiv : WithVal v ≃+* R := RingEquiv.refl _
+
+section AlgebraInstances
+
+variable {R Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
+variable [CommRing R] (v : Valuation R Γ₀)
+variable {P S : Type*}
+
+instance [Ring R] [SMul S R] (v : Valuation R Γ₀) : SMul S (WithVal v) where
+  smul s x := s • WithVal.equiv v x
+
+instance [CommSemiring S] [Algebra S R] (v : Valuation R Γ₀) : Algebra S (WithVal v) where
+  algebraMap := (WithVal.equiv v).symm.toRingHom.comp (algebraMap S R)
+  commutes' _ _ := mul_comm ..
+  smul_def' _ _ := by simp only [Algebra.smul_def, RingEquiv.toRingHom_eq_coe, RingHom.coe_comp,
+    RingHom.coe_coe, Function.comp_apply]; rfl
+
+theorem algebraMap_apply [CommSemiring S] [Algebra S R] (v : Valuation R Γ₀) (s : S) :
+    algebraMap S (WithVal v) s = (WithVal.equiv v).symm (algebraMap S R s) := rfl
 
 instance [CommRing S] [CommRing R] [Algebra S R] [IsFractionRing S R] (v : Valuation R Γ₀) :
     IsFractionRing S (WithVal v) := inferInstanceAs (IsFractionRing S R)
 
-instance [Ring R] [SMul S R] (v : Valuation R Γ₀) : SMul S (WithVal v) :=
-  inferInstanceAs (SMul S R)
+instance [Ring S] [Algebra R S] :
+    Algebra (WithVal v) S := Algebra.compHom S (WithVal.equiv v).toRingHom
+
+theorem algebraMap_apply' [Ring S] [Algebra R S] (x : WithVal v) :
+    algebraMap (WithVal v) S x = algebraMap R S (WithVal.equiv v x) := rfl
+
+instance [CommRing S] [CommRing R] [Algebra S R] [IsFractionRing S R] (v : Valuation R Γ₀) :
+    IsFractionRing S (WithVal v) := inferInstanceAs (IsFractionRing S R)
 
 instance [Ring R] [SMul P S] [SMul S R] [SMul P R] [IsScalarTower P S R] (v : Valuation R Γ₀) :
     IsScalarTower P S (WithVal v) :=
   inferInstanceAs (IsScalarTower P S R)
 
-variable [CommRing R] (v : Valuation R Γ₀)
-
-instance {S : Type*} [Ring S] [Algebra R S] :
-    Algebra (WithVal v) S := inferInstanceAs (Algebra R S)
-
-instance {S : Type*} [Ring S] [Algebra R S] (w : Valuation S Γ₀) :
-    Algebra R (WithVal w) := inferInstanceAs (Algebra R S)
-
-instance {P S : Type*} [Ring S] [Semiring P] [Module P R] [Module P S]
+instance [Ring S] [Semiring P] [Module P R] [Module P S]
     [Algebra R S] [IsScalarTower P R S] :
     IsScalarTower P (WithVal v) S := inferInstanceAs (IsScalarTower P R S)
 
 instance [Ring R] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
     {v : Valuation R Γ₀} : Preorder (WithVal v) := v.toPreorder
 
-end Instances
-
-section Ring
-
-variable [Ring R] (v : Valuation R Γ₀)
-
-/-- Canonical ring equivalence between `WithVal v` and `R`. -/
-def equiv : WithVal v ≃+* R := RingEquiv.refl _
+end AlgebraInstances
 
 /-- Canonical valuation on the `WithVal v` type synonym. -/
 def valuation : Valuation (WithVal v) Γ₀ := v.comap (equiv v)
@@ -152,8 +170,9 @@ variable {R : Type*} [Ring R] (v : Valuation R Γ₀)
 /-- The completion of a field with respect to a valuation. -/
 abbrev Completion := UniformSpace.Completion (WithVal v)
 
-instance : Coe R v.Completion :=
-  inferInstanceAs <| Coe (WithVal v) (UniformSpace.Completion (WithVal v))
+-- lower priority so that `Coe (WithVal v) v.Completion` uses `UniformSpace.Completion.instCoe`
+instance (priority := 99) : Coe R v.Completion where
+  coe r := (WithVal.equiv v).symm r
 
 section Equivalence
 
@@ -230,7 +249,8 @@ namespace NumberField.RingOfIntegers
 
 variable {K : Type*} [Field K] [NumberField K] (v : Valuation K Γ₀)
 
-instance : CoeHead (𝓞 (WithVal v)) (WithVal v) := inferInstanceAs (CoeHead (𝓞 K) K)
+instance : CoeHead (𝓞 (WithVal v)) (WithVal v) where
+  coe x := RingOfIntegers.val x
 
 instance : IsDedekindDomain (𝓞 (WithVal v)) := inferInstanceAs (IsDedekindDomain (𝓞 K))