neg_one_le_meromorphicOrderAt_neg_zeta_logDeriv

theorem neg_one_le_meromorphicOrderAt_neg_zeta_logDeriv (z : ℂ) :    ((-1 : ℤ) : WithTop ℤ) ≤      meromorphicOrderAt (fun w ↦ -deriv riemannZeta w / riemannZeta w) z := by  set φ : ℂ → ℂ := fun w ↦ -deriv riemannZeta w / riemannZeta w with hφ  have hφmero : MeromorphicAt φ z :=    (meromorphicAt_riemannZeta z).deriv.neg.div (meromorphicAt_riemannZeta z)  have hntop := meromorphicOrderAt_riemannZeta_ne_top z  have hne : ∀ᶠ w in 𝓝[≠] z, riemannZeta w ≠ 0 :=    (meromorphicOrderAt_ne_top_iff_eventually_ne_zero (meromorphicAt_riemannZeta z)).1 hntop  have hmul_eq : (φ * riemannZeta) =ᶠ[𝓝[≠] z] fun w ↦ -deriv riemannZeta w := by    filter_upwards [hne] with w hw; simp only [hφ, Pi.mul_apply]; field_simp  have hkey : meromorphicOrderAt φ z + meromorphicOrderAt riemannZeta z      = meromorphicOrderAt (deriv riemannZeta) z := by    rw [← meromorphicOrderAt_mul hφmero (meromorphicAt_riemannZeta z),      meromorphicOrderAt_congr hmul_eq,      show (fun w ↦ -deriv riemannZeta w) = -(deriv riemannZeta) from rfl, ← meromorphicOrderAt_neg]  have hbound := meromorphicOrderAt_le_deriv_add_one (meromorphicAt_riemannZeta z) hntop  rw [← hkey] at hbound  have h2 : (0 : WithTop ℤ) ≤ meromorphicOrderAt φ z + 1 :=    (WithTop.add_le_add_iff_right hntop).1 (by rw [zero_add, add_right_comm]; exact hbound)  refine (WithTop.add_le_add_iff_right WithTop.one_ne_top).1 ?_  rw [show ((-1 : ℤ) : WithTop ℤ) + 1 = 0 by rw [← WithTop.coe_one, ← WithTop.coe_add]; norm_num]  exact h2