CH2.CH2_lemma_4_2b

@[blueprint  "CH2-lemma-4-2b"  (title := "CH2 Lemma 4.2(b)")  (statement := /--If $|\Im z| \leq \frac{\pi}{2}$, then $|(z \coth z)'| \leq |z|$. -/)  (proof := /-- See previous. -/)  (latexEnv := "sublemma")  (discussion := 1234)]theorem CH2_lemma_4_2b (z : ℂ) (hz : |z.im| ≤ π / 2) : ‖deriv (fun z:ℂ ↦ z * coth z) z‖ ≤ ‖z‖ := by  set f := fun w : ℂ ↦ deriv (fun z : ℂ ↦ z * coth z) w  rcases eq_or_ne z 0 with rfl | hz_nz  · simp [deriv_z_coth_z_at_zero]  · let g := dslope f 0    have hg_bound : ‖g z‖ ≤ 1 := by      apply PhragmenLindelof.horizontal_strip (a := -(π / 2)) (b := π / 2) (C := 1) (f := g) (z := z) (hza := (abs_le.mp hz).1) (hzb := (abs_le.mp hz).2)      · have h_g_anal : AnalyticOn ℂ g {w | |w.im| < π} :=          analyticOn_dslope_deriv_z_coth_z_zero        constructor        · apply h_g_anal.differentiableOn.mono          intro w hw; simp only [Set.mem_preimage, Set.mem_Ioo, Set.mem_setOf_eq, abs_lt] at hw ⊢          constructor <;> linarith [Real.pi_pos]        · rw [Complex.closure_preimage_im, closure_Ioo (by linarith [Real.pi_pos])]          apply h_g_anal.continuousOn.mono          intro w hw; simp only [Set.mem_preimage, Set.mem_Icc, Set.mem_setOf_eq, abs_lt] at hw ⊢          constructor <;> linarith [Real.pi_pos]      · rcases deriv_z_coth_z_growth_bound_half_pi with ⟨c, hc, B, hO⟩        refine ⟨c, hc, B, hO.congr' ?_ (Filter.EventuallyEq.refl _ _)⟩        have h_nz : ∀ᶠ w : ℂ in Filter.comap (abs ∘ re) Filter.atTop ⊓ Filter.principal (im ⁻¹' Set.Ioo (-(π / 2)) (π / 2)), w ≠ 0 := by          rw [Filter.eventually_inf_principal]          filter_upwards [Filter.tendsto_comap.eventually (Filter.eventually_ge_atTop 1)] with w hw _          intro h; simp [h] at hw; linarith        filter_upwards [h_nz] with w hw        simp only [f, g, dslope_of_ne f hw, slope, deriv_z_coth_z_at_zero]        simp; ring_nf      · intro w hw        exact norm_dslope_deriv_z_coth_z_le_one_of_abs_im_eq w          (by rw [hw, abs_neg]; exact abs_of_pos (by linarith [Real.pi_pos]))      · intro w hw        exact norm_dslope_deriv_z_coth_z_le_one_of_abs_im_eq w          (by rw [hw]; exact abs_of_pos (by linarith [Real.pi_pos]))    have hg_eq : ‖g z‖ = ‖f z‖ / ‖z‖ := by      unfold g dslope; rw [Function.update_of_ne hz_nz]      unfold slope f      simp only [sub_zero, vsub_eq_sub, smul_eq_mul, deriv_z_coth_z_at_zero]      rw [← div_eq_inv_mul, norm_div]    simpa [f] using (div_le_one (norm_pos_iff.mpr hz_nz)).mp (hg_eq ▸ hg_bound)