∀ (K : Type u_1) [inst : Field K] {f : NumberField.InfinitePlace K → NNReal} [inst_1 : NumberField K]
  {w₁ : NumberField.InfinitePlace K} (B : NNReal),
  (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → f w ≠ 0) →
    ∃ g, (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w, g w ^ w.mult = B