∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E},
  ValueDistribution.logCounting f ↑a₀ =
    Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor (fun x => f x - a₀) Set.univ)⁺