Kadiri.riemannZeta_ne_zero_of_re_nonpos_im_ne_zero

lemma riemannZeta_ne_zero_of_re_nonpos_im_ne_zero {z : ℂ}    (hre : z.re ≤ 0) (him : z.im ≠ 0) : riemannZeta z ≠ 0 := by  set w : ℂ := 1 - z with hw  have hw_im : w.im ≠ 0 := by rw [hw]; simp [him]  have hw_re : 1 ≤ w.re := by rw [hw]; simp; linarith  have hcos : Complex.cos (↑Real.pi * w / 2) ≠ 0 := by    rw [Complex.cos_ne_zero_iff]    intro k hk    have hleft : (↑Real.pi * w / 2).im ≠ 0 := by      rw [show (↑Real.pi * w / 2).im = Real.pi * w.im / 2 by        simp [div_eq_mul_inv, mul_assoc]]      exact div_ne_zero (mul_ne_zero Real.pi_ne_zero hw_im) two_ne_zero    have hright : (((2 * (k : ℂ) + 1) * (Real.pi : ℂ) / 2).im) = 0 := by      simp [div_eq_mul_inv, mul_assoc]    exact hleft (by rw [hk, hright])  have hres := riemannZeta_one_sub_ne_zero_of_one_le_re hw_re hcos  rwa [show (1 : ℂ) - w = z by rw [hw]; ring] at hres