CH2.meromorphicOrderAt_coth_lt_zero_iff

lemma meromorphicOrderAt_coth_lt_zero_iff (z : ℂ) :    meromorphicOrderAt coth z < 0 ↔ Complex.sinh z = 0 := by  have h_coth_eq : coth = Complex.tanh⁻¹ := funext fun z => by unfold coth; simp [one_div]  have h_mero_tanh : MeromorphicAt Complex.tanh z := by fun_prop  have hne_top_tanh : meromorphicOrderAt Complex.tanh z ≠ ⊤ := by    apply (meromorphicOrderAt_ne_top_iff_eventually_ne_zero h_mero_tanh).mpr    have h_sinh_ne : ∀ᶠ x in nhdsWithin z {z}ᶜ, Complex.sinh x ≠ 0 :=      (meromorphicOrderAt_ne_top_iff_eventually_ne_zero Complex.analyticAt_sinh.meromorphicAt).mp        (meromorphicOrderAt_sinh_ne_top z)    have h_cosh_ne : ∀ᶠ x in nhdsWithin z {z}ᶜ, Complex.cosh x ≠ 0 :=      (meromorphicOrderAt_ne_top_iff_eventually_ne_zero Complex.analyticAt_cosh.meromorphicAt).mp        (meromorphicOrderAt_cosh_ne_top z)    filter_upwards [h_sinh_ne, h_cosh_ne] with x hs hc    rw [Complex.tanh_eq_sinh_div_cosh, div_ne_zero_iff]    exact ⟨hs, hc⟩  rw [h_coth_eq, meromorphicOrderAt_inv]  have h_neg_lt : -meromorphicOrderAt Complex.tanh z < 0 ↔      0 < meromorphicOrderAt Complex.tanh z := by    lift meromorphicOrderAt Complex.tanh z to ℤ using hne_top_tanh with a    norm_cast; omega  rw [h_neg_lt]  constructor  · intro h    by_cases hc : Complex.cosh z = 0    · exfalso      have hsinh_ne := Complex.sinh_ne_zero_of_cosh_zero hc      have hsinh_ord : meromorphicOrderAt Complex.sinh z = 0 := by        rw [← tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero (by fun_prop)]        exact ⟨_, hsinh_ne, Complex.analyticAt_sinh.continuousAt.continuousWithinAt⟩      have hcosh_ord : 0 < meromorphicOrderAt Complex.cosh z := by        rw [← tendsto_zero_iff_meromorphicOrderAt_pos (by fun_prop)]        exact hc ▸ Complex.analyticAt_cosh.continuousAt.continuousWithinAt      have hord_neg : meromorphicOrderAt Complex.tanh z < 0 := by        rw [show Complex.tanh = fun x => Complex.sinh x / Complex.cosh x from              funext Complex.tanh_eq_sinh_div_cosh]        push (disch := fun_prop) meromorphicOrderAt        rw [hsinh_ord]        lift meromorphicOrderAt Complex.cosh z to ℤ using meromorphicOrderAt_cosh_ne_top z with m hm        norm_cast at hcosh_ord ⊢; omega      exact absurd hord_neg (not_lt.mpr h.le)    · have hcts : ContinuousAt Complex.tanh z := by fun_prop (disch := exact hc)      have h_tendsto := (tendsto_zero_iff_meromorphicOrderAt_pos h_mero_tanh).mpr h      have hval : Complex.tanh z = 0 :=        tendsto_nhds_unique (hcts.tendsto.mono_left nhdsWithin_le_nhds) h_tendsto      rw [Complex.tanh_eq_sinh_div_cosh, div_eq_zero_iff] at hval      exact hval.resolve_right hc  · intro h    have hc : Complex.cosh z ≠ 0 := Complex.cosh_ne_zero_of_sinh_zero h    have hcts : ContinuousAt Complex.tanh z := by fun_prop (disch := exact hc)    have hval : Complex.tanh z = 0 := by rw [Complex.tanh_eq_sinh_div_cosh, h, zero_div]    rw [← tendsto_zero_iff_meromorphicOrderAt_pos h_mero_tanh]    convert hcts.tendsto.mono_left nhdsWithin_le_nhds using 1; simp [hval]