CH2.meromorphicOrderAt_cosh_ne_top

lemma meromorphicOrderAt_cosh_ne_top (z : ℂ) : meromorphicOrderAt Complex.cosh z ≠ ⊤ := by  intro h_top  have h_p : ∀ᶠ x in nhdsWithin z {z}ᶜ, Complex.cosh x = 0 :=    meromorphicOrderAt_eq_top_iff.mp h_top  have h_val : Complex.cosh z = 0 := tendsto_nhds_unique    (Complex.continuous_cosh.continuousAt.tendsto.mono_left nhdsWithin_le_nhds)    (Filter.EventuallyEq.tendsto h_p)  have h_nhds : (fun x => Complex.cosh x) =ᶠ[nhds z] (fun _ => (0 : ℂ)) := by    rw [eventually_nhdsWithin_iff] at h_p    filter_upwards [h_p] with x hx    exact if hxz : x = z then hxz ▸ h_val else hx hxz  have h_sinh : Complex.sinh z = 0 := by    simpa [deriv_const, (Complex.hasDerivAt_cosh z).deriv] using h_nhds.deriv_eq  exact absurd h_sinh (Complex.sinh_ne_zero_of_cosh_zero h_val)