∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (AbsoluteValue K ℝ)]
  (v : NumberField.InfinitePlace K), Multiset.count (↑v) (NumberField.multisetInfinitePlace K) = v.mult