chore(Topology/Algebra/Valued/NormedValued): rely on TC IsUltrametricDist instead of explicit arg (#17561)

Before, we had
```
[hK : NormedField K] (h : IsNonarchimedean (norm : K → ℝ))
```
Now we use `[hK : NormedField K] [IsUltrametricDist K]` to convert between ultrametrically normed fields and valued fields.
This allows the instance to be a scoped instance instead of a def, since `IsUltrametricDist` is a class on the type, as opposed to a plain prop about the norm of the type.
The instance is scoped because otherwise, one gets a TC loop.

Author: pechersky

Mathlib/Topology/Algebra/Valued/NormedValued.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: María Inés de Frutos-Fernández
 -/
 import Mathlib.Analysis.Normed.Field.Basic
-import Mathlib.Analysis.Normed.Group.Uniform
+import Mathlib.Analysis.Normed.Group.Ultra
 import Mathlib.RingTheory.Valuation.RankOne
 import Mathlib.Topology.Algebra.Valued.ValuationTopology
 
@@ -30,7 +30,9 @@ open Filter Set Valuation
 
 open scoped NNReal
 
-variable {K : Type*} [hK : NormedField K] (h : IsNonarchimedean (norm : K → ℝ))
+section
+
+variable {K : Type*} [hK : NormedField K] [IsUltrametricDist K]
 
 namespace NormedField
 
@@ -40,24 +42,35 @@ def valuation : Valuation K ℝ≥0 where
   map_zero'       := nnnorm_zero
   map_one'        := nnnorm_one
   map_mul'        := nnnorm_mul
-  map_add_le_max' := h
+  map_add_le_max' := IsUltrametricDist.norm_add_le_max
 
-theorem valuation_apply (x : K) : valuation h x = ‖x‖₊ := rfl
+@[simp]
+theorem valuation_apply (x : K) : valuation x = ‖x‖₊ := rfl
 
 /-- The valued field structure on a nonarchimedean normed field `K`, determined by the norm. -/
 def toValued : Valued K ℝ≥0 :=
   { hK.toUniformSpace,
     @NonUnitalNormedRing.toNormedAddCommGroup K _ with
-    v := valuation h
+    v := valuation
     is_topological_valuation := fun U => by
       rw [Metric.mem_nhds_iff]
       exact ⟨fun ⟨ε, hε, h⟩  =>
           ⟨Units.mk0 ⟨ε, le_of_lt hε⟩ (ne_of_gt hε), fun x hx ↦ h (mem_ball_zero_iff.mpr hx)⟩,
         fun ⟨ε, hε⟩ => ⟨(ε : ℝ), NNReal.coe_pos.mpr (Units.zero_lt _),
           fun x hx ↦ hε (mem_ball_zero_iff.mp hx)⟩⟩ }
 
+instance {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] :
+    Valuation.RankOne (valuation (K := K)) where
+  hom := .id _
+  strictMono' := strictMono_id
+  nontrivial' := (exists_one_lt_norm K).imp fun x h ↦ by
+    have h' : x ≠ 0 := norm_eq_zero.not.mp (h.gt.trans' (by simp)).ne'
+    simp [valuation_apply, ← NNReal.coe_inj, h.ne', h']
+
 end NormedField
 
+end
+
 namespace Valued
 
 variable {L : Type*} [Field L] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
@@ -126,4 +139,25 @@ def toNormedField : NormedField L :=
         exact ⟨fun a b hab => lt_of_lt_of_le hab (min_le_left _ _), fun a b hab =>
             lt_of_lt_of_le hab (min_le_right _ _)⟩ }
 
+-- When a field is valued, one inherits a `NormedField`.
+-- Scoped instance to avoid a typeclass loop or non-defeq topology or norms.
+scoped[Valued] attribute [instance] Valued.toNormedField
+scoped[NormedField] attribute [instance] NormedField.toValued
+
+section NormedField
+
+open scoped Valued
+
+protected lemma isNonarchimedean_norm : IsNonarchimedean ((‖·‖): L → ℝ) := Valued.norm_add_le
+
+instance : IsUltrametricDist L :=
+  ⟨fun x y z ↦ by
+    refine (Valued.norm_add_le (x - y) (y - z)).trans_eq' ?_
+    simp only [sub_add_sub_cancel]
+    rfl ⟩
+
+lemma coe_valuation_eq_rankOne_hom_comp_valuation : ⇑NormedField.valuation = hv.hom ∘ val.v := rfl
+
+end NormedField
+
 end Valued