∀ (L : Type u_1) [inst : Field L] (Γ₀ : Type u_2) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne],
  Valued.toNormedField L Γ₀ =
    { norm := Valued.norm, toField := inferInstance, dist := fun x y => Valued.norm (x - y), dist_self := ⋯,
      dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯, toUniformSpace := val.toUniformSpace, uniformity_dist := ⋯,
      cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯, norm_mul := ⋯ }