Kadiri.summable_re_one_div_at_zeros

theorem summable_re_one_div_at_zeros (s : ℂ) :    Summable (fun ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ) ↦      (1 / (s - ρ.val)).re) := by  have htail : Summable (fun ρ : NontrivialZeros ↦      (|s.re| + 1) * (|(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ))) :=    (summable_zeroImagSquareTail_shifted_unconditional s).mul_left _  refine Summable.of_norm_bounded_eventually htail ?_  rw [Filter.eventually_cofinite]  apply Set.Finite.subset (nontrivialZeros_shifted_abs_im_lt_one_finite s)  intro ρ hbad  rw [Set.mem_setOf_eq] at hbad ⊢  by_contra hsmall  have him : 1 ≤ |(s - (ρ : ℂ)).im| := le_of_not_gt hsmall  have him0 : (s - (ρ : ℂ)).im ≠ 0 := by    intro h    rw [h] at him    norm_num at him  have hw0 : s - (ρ : ℂ) ≠ 0 := by    intro h    apply him0    rw [h]    rfl  have hre : (ρ : ℂ).re ∈ Set.Ioo (0 : ℝ) 1 := ρ.property.1  have hre_bound : |(s - (ρ : ℂ)).re| ≤ |s.re| + 1 := by    rw [Complex.sub_re]    calc |s.re - (ρ : ℂ).re| ≤ |s.re| + |(ρ : ℂ).re| := abs_sub _ _      _ ≤ |s.re| + 1 := by          rw [abs_of_pos hre.1]          linarith [hre.2]  have hdiv_re : (1 / (s - (ρ : ℂ))).re =      (s - (ρ : ℂ)).re / Complex.normSq (s - (ρ : ℂ)) := by    rw [Complex.div_re]    simp  have hns : (s - (ρ : ℂ)).im ^ 2 ≤ Complex.normSq (s - (ρ : ℂ)) := by    rw [Complex.normSq_apply]    nlinarith [mul_self_nonneg (s - (ρ : ℂ)).re]  have him2 : (0 : ℝ) < (s - (ρ : ℂ)).im ^ 2 := by positivity  have hnpos : (0 : ℝ) < Complex.normSq (s - (ρ : ℂ)) := Complex.normSq_pos.2 hw0  apply hbad  rw [Real.norm_eq_abs, hdiv_re, abs_div, abs_of_nonneg (Complex.normSq_nonneg _)]  calc |(s - (ρ : ℂ)).re| / Complex.normSq (s - (ρ : ℂ))      ≤ (|s.re| + 1) / Complex.normSq (s - (ρ : ℂ)) := by gcongr    _ ≤ (|s.re| + 1) / (s - (ρ : ℂ)).im ^ 2 := by        gcongr    _ = (|s.re| + 1) * (|(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ)) := by        rw [inv_pow, sq_abs, div_eq_mul_inv]