CH2.deriv_z_coth_z_bound_boundary

lemma deriv_z_coth_z_bound_boundary (x : ℝ) :    ‖deriv (fun z : ℂ ↦ z * coth z) (↑x + ↑(π / 4) * Complex.I)‖ < 1 := by  set z₀ := (↑x + ↑(π / 4) * Complex.I)  set f := fun z : ℂ ↦ z * coth z  have h_snz : Complex.sinh z₀ ≠ 0 := by    apply sinh_ne_zero_of_im    intro k    show z₀.im ≠ k * π    simp [z₀]    have : π ≠ 0 := Real.pi_pos.ne.symm    field_simp [this]    norm_cast    intro h    have : (k * 4 : ℤ) = (1 : ℤ) := by      norm_cast at h      ring_nf at h      exact_mod_cast h.symm    omega  have h_deriv_eq : deriv f z₀ = (Complex.sinh (2 * z₀) / 2 - z₀) / (Complex.sinh z₀ ^ 2) :=    deriv_z_coth_z_eq_alt z₀ h_snz  have h_normSq : ‖deriv f z₀‖^2 = 1 - (π * Real.cosh (2 * x) - π ^ 2 / 4 - 4 * x ^ 2) / (Real.cosh (2 * x) ^ 2) := by    rw [h_deriv_eq, norm_div, div_pow, Complex.sq_norm, Complex.sq_norm]    have h_snz_normSq : Complex.normSq (Complex.sinh z₀) = Real.cosh (2 * x) / 2 := by      rw [← Complex.sq_norm, normSq_sinh]      have : z₀.re = x := by simp [z₀]      have : z₀.im = π / 4 := by simp [z₀]      rw [this, ‹z₀.re = x›, Real.sin_pi_div_four]      have : (√2 / 2 : ℝ) ^ 2 = 1 / 2 := by        rw [div_pow, Real.sq_sqrt (by positivity)]        norm_num      rw [this, Real.sinh_sq, Real.cosh_two_mul, Real.cosh_sq' x]      field_simp; ring    have h_num : Complex.sinh (2 * z₀) / 2 - z₀ = -x + (Real.cosh (2 * x) / 2 - π / 4) * Complex.I := by      rw [show 2 * z₀ = ↑(2 * x) + ↑(π / 2) * Complex.I by simp [z₀]; ring,          Complex.sinh_add, Complex.sinh_mul_I, Complex.cosh_mul_I]      norm_cast      rw [Real.cos_pi_div_two, Real.sin_pi_div_two]      simp [z₀]; ring    rw [h_num, pow_two, Complex.normSq_mul, h_snz_normSq]    rw [show -↑x + (↑(Real.cosh (2 * x)) / 2 - ↑π / 4) * Complex.I =             ↑(-x) + ↑(Real.cosh (2 * x) / 2 - π / 4) * Complex.I by push_cast; simp,        Complex.normSq_add_mul_I]    field_simp [(Real.cosh_pos (2 * x)).ne.symm]    ring  have h_pos : 0 < (π * Real.cosh (2 * x) - π ^ 2 / 4 - 4 * x ^ 2) := pi_cosh_two_mul_sub_bounds x  have h_normSq_lt : ‖deriv f z₀‖^2 < 1 := by    rw [h_normSq]; linarith [div_pos h_pos (by positivity : 0 < Real.cosh (2 * x) ^ 2)]  nlinarith [norm_nonneg (deriv f z₀), sq_nonneg (‖deriv f z₀‖)]