∀ (L : Type u_1) [inst : Field L] (Γ₀ : Type u_2) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne] (x y : L),
  ↑(NNReal.mk ((fun x y => Valued.v.norm (x - y)) x y) ⋯) = ENNReal.ofReal (Valued.v.norm (x - y))