tendsto_sub_mul_neg_zeta_logDeriv

theorem tendsto_sub_mul_neg_zeta_logDeriv {p : ℂ} {m : ℤ}    (hm : meromorphicOrderAt riemannZeta p = m) :    Tendsto (fun z ↦ (z - p) * (-deriv riemannZeta z / riemannZeta z)) (𝓝[≠] p) (𝓝 (-(m:ℂ))) := by  obtain ⟨g, hg_an, hg_ne, hg_eq⟩ :=    (meromorphicOrderAt_eq_int_iff (meromorphicAt_riemannZeta p)).1 hm  have hderiv := deriv_zpow_mul_eventuallyEq g hg_an hg_eq  have hgne : ∀ᶠ z in 𝓝[≠] p, g z ≠ 0 :=    (hg_an.continuousAt.eventually_ne hg_ne).filter_mono nhdsWithin_le_nhds  have heq : (fun z ↦ (z - p) * (-deriv riemannZeta z / riemannZeta z))      =ᶠ[𝓝[≠] p] fun z ↦ (-((m : ℂ) * g z + (z - p) * deriv g z)) / g z := by    filter_upwards [hg_eq, hderiv, self_mem_nhdsWithin, hgne] with z hz hdz hz_ne hgz    have hzp : z - p ≠ 0 := sub_ne_zero.mpr hz_ne    rw [hz, hdz]; simp only [Pi.mul_apply, smul_eq_mul, zpow_sub_one₀ hzp]; field_simp  refine Tendsto.congr' heq.symm ?_  have tg : Tendsto g (𝓝[≠] p) (𝓝 (g p)) := hg_an.continuousAt.tendsto.mono_left nhdsWithin_le_nhds  have tg' : Tendsto (deriv g) (𝓝[≠] p) (𝓝 (deriv g p)) :=    hg_an.deriv.continuousAt.tendsto.mono_left nhdsWithin_le_nhds  have tzp : Tendsto (fun z : ℂ ↦ z - p) (𝓝[≠] p) (𝓝 0) :=    tendsto_nhdsWithin_of_tendsto_nhds (by      have : Tendsto (fun z : ℂ ↦ z - p) (𝓝 p) (𝓝 (p - p)) := Continuous.tendsto (by fun_prop) p      simpa using this)  have hnum : Tendsto (fun z ↦ (m : ℂ) * g z + (z - p) * deriv g z) (𝓝[≠] p)      (𝓝 ((m : ℂ) * g p)) := by    simpa using (tendsto_const_nhds.mul tg).add (tzp.mul tg')  have hlim := (hnum.neg).div tg hg_ne  rwa [show -((m : ℂ) * g p) / g p = -(m : ℂ) by field_simp] at hlim