fix(Valuation/RankOne): replace abstract completion RankOne instance with concrete instances (#34834)

#26872 fixes the definition of `Valuation.RankOne` so that its order embedding into `NNReal` is a map from the range of the value group (the type `MonoidWithZeroHom.ValueGroup₀`). 

This causes problems with the instance `instRankOneCompletion` (PR'd recently #33594) because the value group of the completion no longer type checks as the value group of the base ring. This abstract instance was only introduced to combine the proofs of `(v.valuation K).RankOne` and its completion `Valued.v.RankOne`. So we separate them here as concrete separate instances to help with the `RankOne` refactor.

Author: smmercuri

Mathlib/NumberTheory/NumberField/FinitePlaces.lean

@@ -136,22 +136,23 @@ noncomputable def FinitePlace.embedding : WithVal (v.valuation K) →+* adicComp
 theorem FinitePlace.embedding_apply (x : K) : embedding v x = ↑x := rfl
 
 noncomputable instance : (v.valuation K).RankOne where
-  hom := {
-    toFun := toNNReal (absNorm_ne_zero v)
-    map_zero' := rfl
-    map_one' := rfl
-    map_mul' := map_mul (toNNReal (absNorm_ne_zero v))
-  }
+  hom := toNNReal (absNorm_ne_zero v)
   strictMono' := toNNReal_strictMono (one_lt_absNorm_nnreal v)
   exists_val_nontrivial := by
     rcases Submodule.exists_mem_ne_zero_of_ne_bot v.ne_bot with ⟨x, hx1, hx2⟩
     use x
     rw [valuation_of_algebraMap]
     exact ⟨v.intValuation_ne_zero _ hx2, ((intValuation_lt_one_iff_mem _ _).2 hx1).ne⟩
 
-@[deprecated Valuation.instRankOneCompletion (since := "2026-01-05")]
 noncomputable instance instRankOneValuedAdicCompletion :
-    Valuation.RankOne (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰) := inferInstance
+    Valuation.RankOne (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰) where
+  hom := toNNReal (absNorm_ne_zero v)
+  strictMono' := toNNReal_strictMono (one_lt_absNorm_nnreal v)
+  exists_val_nontrivial := by
+    rcases Submodule.exists_mem_ne_zero_of_ne_bot v.ne_bot with ⟨x, hx1, hx2⟩
+    use x
+    rw [valuedAdicCompletion_eq_valuation' v (x : K)]
+    simpa [valuation_of_algebraMap] using ⟨v.intValuation_ne_zero _ hx2, hx1⟩
 
 /-- The `v`-adic completion of `K` is a normed field. -/
 noncomputable instance instNormedFieldValuedAdicCompletion : NormedField (adicCompletion K v) :=

Mathlib/RingTheory/Valuation/RankOne.lean

@@ -114,16 +114,6 @@ instance [RankOne v] : IsNontrivial v where
 
 end RankOne
 
-instance instRankOneCompletion {K : Type*} [Field K] {Γ : Type*}
-    [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) [h : v.RankOne] :
-    (Valued.v : Valuation v.Completion Γ).RankOne where
-  hom := Valuation.RankOne.hom v
-  strictMono' := Valuation.RankOne.strictMono v
-  exists_val_nontrivial := by
-    rcases h.exists_val_nontrivial with ⟨x, hx1, hx2⟩
-    use (WithVal.equiv v).symm x
-    simp_all
-
 end Valuation
 
 section ValuativeRel