CH2.Phi_cancel

@[blueprint  "Phi-cancel"  (title := "$\\Phi^{\\circ}_\\nu \\pm \\Phi^{\\ast}_\\nu$ pole cancellation")  (statement := /--  $\Phi^{\sigma, \circ}_\nu(z) \pm \Phi^{\sigma, \ast}_\nu(z)$ is regular at $\pm 1 - i \nu / 2 \pi$.  -/)  (proof := /-- The residues cancel out. -/)  (latexEnv := "lemma")  (discussion := 1074)]theorem Phi_cancel (ν ε σ : ℝ) (hν : ν > 0) (hσ : |σ| = 1) :    meromorphicOrderAt (fun z ↦ Phi_circ ν ε z + σ * Phi_star ν ε z) ((σ : ℂ) - I * ν / (2 * π)) ≥ 0 := by  have hσ : σ = 1 ∨ σ = -1 := by grind  obtain ⟨n, rfl, hn_cases⟩ : ∃ n : ℤ, σ = n ∧ n ≠ 0 := by    rcases hσ with h | h    · exact ⟨1, by exact_mod_cast h, one_ne_zero⟩    · exact ⟨-1, by exact_mod_cast h, by norm_num⟩  set z₀ : ℂ := n - I * ν / (2 * π)  set f := fun z ↦ Phi_circ ν ε z + n * Phi_star ν ε z  have h_mero_f : MeromorphicAt f z₀ := by fun_prop [CH2.Phi_circ]  have h_tendsto_zero : (nhdsWithin z₀ {z₀}ᶜ).Tendsto (fun z ↦ (z - z₀) * f z) (nhds 0) := by    convert Filter.Tendsto.add (Phi_circ.residue ν ε hν n)      (Filter.Tendsto.const_mul (n : ℂ) (Phi_star.residue ν ε hν n hn_cases)) using 1    · ext z; ring    · ring_nf      suffices h : (0 : ℂ) = I * (↑π)⁻¹ * (1 / 2) + I * (↑π)⁻¹ * (n : ℂ) ^ 2 * (-1 / 2) by exact congr_arg nhds h      have hn_sq : (n : ℂ) ^ 2 = 1 := by        exact_mod_cast sq_eq_one_iff.mpr hσ      simp only [hn_sq]      ring  rw [tendsto_zero_iff_meromorphicOrderAt_pos (by fun_prop)] at h_tendsto_zero  change 0 < meromorphicOrderAt ((· - z₀) * f) z₀ at h_tendsto_zero  rw [meromorphicOrderAt_mul (by fun_prop) h_mero_f] at h_tendsto_zero  rw [show meromorphicOrderAt (· - z₀) z₀ = (1 : ℤ) from    (meromorphicOrderAt_eq_int_iff (by fun_prop)).mpr ⟨1, analyticAt_const, one_ne_zero, by simp⟩] at h_tendsto_zero  change (0 : WithTop ℤ) ≤ meromorphicOrderAt f z₀  cases h_ord : meromorphicOrderAt f z₀ <;> simp_all  norm_cast at h_tendsto_zero  omega