CH2.Phi_star.poles_simple

@[blueprint  "Phi-star-poles-simple"  (title := "$\\Phi^{\\pm,\\ast}_\\nu$ poles simple")  (statement := /--  The poles of $$\Phi^{\pm,\ast}_\nu(z)$$ are all simple.  -/)  (proof := /-- This follows from the definition of $\Phi^{\pm,\ast}_\nu$ and the properties of the $B^\pm$ function. -/)  (latexEnv := "lemma")]theorem Phi_star.poles_simple (ν ε : ℝ) (hν : ν > 0) (z : ℂ) :    meromorphicOrderAt (Phi_star ν ε) z = -1 ↔ ∃ n : ℤ, n ≠ 0 ∧ z = n - I * ν / (2 * π) := by  constructor  · exact fun h ↦ (Phi_star.poles ν ε hν z).mp (h ▸ by decide)  · rintro ⟨n, hn, rfl⟩    set z₀ := (n : ℂ) - I * ν / (2 * π)    have hsub : MeromorphicAt (· - z₀) z₀ := by fun_prop    have hf : MeromorphicAt (Phi_star ν ε) z₀ := by fun_prop    have heq : (fun z ↦ (z - z₀) * Phi_star ν ε z) =ᶠ[nhdsWithin z₀ {z₀}ᶜ] ((· - z₀) * Phi_star ν ε) :=      Filter.Eventually.of_forall fun _ ↦ rfl    have hord₀ : meromorphicOrderAt ((· - z₀) * Phi_star ν ε) z₀ = 0 := by      rw [← tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero (hsub.mul hf)]      exact ⟨_, by simp [hn, pi_ne_zero], (Phi_star.residue ν ε hν n hn).congr' heq⟩    have hord₁ : meromorphicOrderAt (· - z₀) z₀ = (1 : ℤ) := by      rw [meromorphicOrderAt_eq_int_iff hsub]      exact ⟨1, analyticAt_const, one_ne_zero, by simp⟩    rw [meromorphicOrderAt_mul hsub hf, hord₁] at hord₀    obtain ⟨m, hm⟩ := WithTop.ne_top_iff_exists.mp      (by rintro h; simp [h] at hord₀ : meromorphicOrderAt (Phi_star ν ε) z₀ ≠ ⊤)    rw [← hm] at hord₀ ⊢    have h1 : ((1 : ℤ) + m : WithTop ℤ) = (1 + m : ℤ) := by push_cast; ring_nf    rw [h1] at hord₀    have : 1 + m = 0 := by exact_mod_cast hord₀    change (m : WithTop ℤ) = (-1 : ℤ); congr 1; omega