CH2.sinh_ne_zero_of_not_pole

lemma sinh_ne_zero_of_not_pole {ν : ℝ} {z : ℂ} (h_not_pole : ∀ n : ℤ, z ≠ n - I * ν / (2 * π)) :    Complex.sinh ((-2 * π * I * z + ν) / 2) ≠ 0 := by  intro h  obtain ⟨k, hk⟩ := (sinh_zero_iff _).mp h  have h_z : z = ↑(-k) - I * ν / (2 * π) := by    calc z = (2 * π * I * z) / (2 * π * I) := by field_simp [pi_ne_zero, I_ne_zero]      _ = (ν - (-2 * π * I * z + ν)) / (2 * π * I) := by ring      _ = (ν - 2 * ((-2 * π * I * z + ν) / 2)) / (2 * π * I) := by ring      _ = (ν - 2 * (k * π * I)) / (2 * π * I) := by rw [hk]      _ = ν / (2 * π * I) - (2 * k * π * I) / (2 * π * I) := by field_simp [pi_ne_zero, I_ne_zero]      _ = -I * ν / (2 * π) - k := by field_simp [pi_ne_zero, I_ne_zero]; ring_nf; simp [I_sq]      _ = ↑(-k) - I * ν / (2 * π) := by simp; ring  exact h_not_pole (-k) h_z