∀ (L : Type u_1) [inst : Field L] (Γ₀ : Type u_2) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne], ⇑NormedField.valuation = ⇑(Valuation.RankOne.hom Valued.v) ∘ ⇑Valued.v