Kadiri.riemannZeta_eventually_ne_zero_punctured_nontrivialZero

lemma riemannZeta_eventually_ne_zero_punctured_nontrivialZero (rho : NontrivialZeros) :    ∀ᶠ z in nhdsWithin (rho : ℂ) ({(rho : ℂ)}ᶜ), riemannZeta z ≠ 0 := by  have hmem_compl_one : (rho : ℂ) ∈ ({1} : Set ℂ)ᶜ := by    simpa [Set.mem_compl_iff] using nontrivialZero_ne_one rho  have hdisj : Disjoint (nhdsWithin (rho : ℂ) ({(rho : ℂ)}ᶜ))      (𝓟 (({1} : Set ℂ)ᶜ \ riemannZeta.zeroesᶜ)) := by    exact (mem_codiscreteWithin.mp riemannZeta.zeroes_codiscreteWithin_compl_one)      (rho : ℂ) hmem_compl_one  have hnot_zeroes : (({1} : Set ℂ)ᶜ \ riemannZeta.zeroesᶜ)ᶜ ∈      nhdsWithin (rho : ℂ) ({(rho : ℂ)}ᶜ) :=    Filter.disjoint_principal_right.mp hdisj  have heventually_compl_one : ∀ᶠ z in nhdsWithin (rho : ℂ) ({(rho : ℂ)}ᶜ),      z ∈ ({1} : Set ℂ)ᶜ := by    exact nhdsWithin_le_nhds (isOpen_compl_singleton.mem_nhds hmem_compl_one)  filter_upwards [hnot_zeroes, heventually_compl_one] with z hznot hz_compl_one hzero  have hz_zero : z ∈ riemannZeta.zeroes := by    simpa [riemannZeta.zeroes] using hzero  exact hznot ⟨hz_compl_one, by simpa using hz_zero⟩