logDeriv_poles_eq_divisor_support

theorem logDeriv_poles_eq_divisor_support    {f : ℂ → ℂ} {R : Set ℂ}    (hf : MeromorphicOn f R) (hlog : MeromorphicOn (logDeriv f) R)    (hfinite_order : ∀ p ∈ R, meromorphicOrderAt f p ≠ ⊤) :    R ∩ {p | meromorphicOrderAt (logDeriv f) p < 0} =      (MeromorphicOn.divisor f R).support := by  classical  let D := MeromorphicOn.divisor f R  ext p  constructor  · intro hp    rcases hp with ⟨hpR, hpneg⟩    obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp (hfinite_order p hpR)    by_cases hn0 : n = 0    · have hord0 : meromorphicOrderAt f p = (0 : WithTop ℤ) := by        simpa [hn0] using hn.symm      have hnonneg :=        logDeriv_meromorphicOrderAt_nonneg_of_order_zero (hf p hpR) (hlog p hpR) hord0      exact False.elim (not_lt_of_ge hnonneg hpneg)    · have hpD_ne : D p ≠ 0 := by        change (MeromorphicOn.divisor f R) p ≠ 0        rw [MeromorphicOn.divisor_apply hf hpR, ← hn]        simp [hn0]      simp [D, Function.mem_support, hpD_ne]  · intro hpD    have hpR : p ∈ R := (MeromorphicOn.divisor f R).supportWithinDomain hpD    have hpD_ne : D p ≠ 0 := by      simpa [D, Function.mem_support] using hpD    change (MeromorphicOn.divisor f R) p ≠ 0 at hpD_ne    rw [MeromorphicOn.divisor_apply hf hpR] at hpD_ne    obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp (hfinite_order p hpR)    have hn0 : n ≠ 0 := by      intro hn0      exact hpD_ne (by rw [← hn]; simp [hn0])    have hneg_one :=      logDeriv_meromorphicOrderAt_eq_neg_one_of_order_ne_zero (hf p hpR) (hlog p hpR)        hn.symm hn0    refine ⟨hpR, ?_⟩    change meromorphicOrderAt (logDeriv f) p < 0    rw [hneg_one]    exact WithTop.coe_lt_coe.2 (by norm_num : (-1 : ℤ) < 0)