CH2.Phi_star.analyticAt_of_not_pole_nz

theorem Phi_star.analyticAt_of_not_pole_nz (ν ε : ℝ) (z : ℂ) (h_not_pole : ∀ n : ℤ, n ≠ 0 → z ≠ n - I * ν / (2 * π)) :    AnalyticAt ℂ (Phi_star ν ε) z := by  set w : ℂ := -2 * π * I * z + ν  have hB_an : AnalyticAt ℂ (B ε) w := by    apply analyticAt_B    intro n hn hw    apply h_not_pole (-n) (by simp [hn])    have : z = ↑(-n) - I * ν / (2 * π) := by      have h1 : -2 * π * I * z = 2 * π * I * n - ν := by linear_combination hw      replace h1 := congr_arg (fun x ↦ x / (-2 * π * I)) h1      rw [mul_div_cancel_left₀ _ (by simp [pi_ne_zero, I_ne_zero] : -2 * π * I ≠ 0)] at h1      rw [h1]      field_simp [pi_ne_zero, I_ne_zero]      ring_nf      simp [I_sq]    exact this  unfold Phi_star; fun_prop (disch := exact [hB_an.comp (by fun_prop), by simp [w]; fun_prop])