meromorphicOrderAt_le_deriv_add_one

theorem meromorphicOrderAt_le_deriv_add_one {f : ℂ → ℂ} {x : ℂ}    (hf : MeromorphicAt f x) (hntop : meromorphicOrderAt f x ≠ ⊤) :    meromorphicOrderAt f x ≤ meromorphicOrderAt (deriv f) x + 1 := by  obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp hntop  obtain ⟨g, hg_an, hg_ne, hg_eq⟩ := (meromorphicOrderAt_eq_int_iff hf).1 hn.symm  have hh_an : AnalyticAt ℂ (fun z ↦ (n : ℂ) * g z + (z - x) * deriv g z) x :=    (analyticAt_const.mul hg_an).add ((analyticAt_id.sub analyticAt_const).mul hg_an.deriv)  have hzpow : MeromorphicAt (fun z : ℂ ↦ (z - x) ^ (n - 1)) x :=    ((analyticAt_id.sub analyticAt_const).meromorphicAt).zpow (n - 1)  have hzord : meromorphicOrderAt (fun z : ℂ ↦ (z - x) ^ (n - 1)) x = (↑(n - 1) : WithTop ℤ) := by    rw [show (fun z : ℂ ↦ (z - x) ^ (n - 1)) = (fun z : ℂ ↦ z - x) ^ (n - 1) from rfl]    exact meromorphicOrderAt_zpow_id_sub_const  rw [← hn, meromorphicOrderAt_congr (deriv_zpow_mul_eventuallyEq g hg_an hg_eq),    meromorphicOrderAt_mul hzpow hh_an.meromorphicAt, hzord, add_right_comm,    show (↑(n - 1) : WithTop ℤ) + 1 = ↑n by rw [← WithTop.coe_one, ← WithTop.coe_add]; norm_num]  exact le_add_of_nonneg_right hh_an.meromorphicOrderAt_nonneg