Complex.tsum_one_div_natCast_add_add_one_sq_le

lemma tsum_one_div_natCast_add_add_one_sq_le {N : ℕ} (hN : 1 ≤ N) :    ∑' i : ℕ, 1 / (((i + N : ℕ) : ℝ) + 1) ^ 2 ≤ (N : ℝ)⁻¹ := by  have hNR : (1 : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN  have hpos : ∀ i : ℕ, (0 : ℝ) < (i : ℝ) + N := fun i => by    have : (0 : ℝ) ≤ i := Nat.cast_nonneg i    linarith  set u : ℕ → ℝ := fun i => ((i : ℝ) + N)⁻¹ with hu_def  have h0 : Tendsto u atTop (𝓝 0) := by    apply Filter.Tendsto.inv_tendsto_atTop    exact tendsto_atTop_add_const_right atTop _ tendsto_natCast_atTop_atTop  have hdiff : ∀ i : ℕ, u i - u (i + 1) = (((i : ℝ) + N) * ((i : ℝ) + 1 + N))⁻¹ := by    intro i    simp only [hu_def]    have h1 : ((i : ℝ) + N) ≠ 0 := (hpos i).ne'    have h2 : ((i : ℝ) + 1 + N) ≠ 0 := by      have := hpos i      intro h      linarith    push_cast    rw [inv_sub_inv h1 h2]    have e1 : (i : ℝ) + 1 + N - ((i : ℝ) + N) = 1 := by ring    rw [e1, one_div]  have hsumu : Summable (fun i : ℕ => u i - u (i + 1)) := by    apply Summable.of_nonneg_of_le (f := fun i : ℕ => 1 / ((i : ℝ) + 1) ^ 2) ?_ ?_      summable_one_div_natCast_add_one_sq    · intro i      rw [hdiff i]      positivity    · intro i      rw [hdiff i, ← one_div]      apply one_div_le_one_div_of_le (by positivity)      have h3 : (0 : ℝ) ≤ i := Nat.cast_nonneg i      nlinarith  have htel := hasSum_sub_succ_of_tendsto_zero h0 hsumu  have hu0 : u 0 = (N : ℝ)⁻¹ := by    simp only [hu_def]    norm_num  have hsumL : Summable (fun i : ℕ => 1 / (((i + N : ℕ) : ℝ) + 1) ^ 2) :=    (summable_nat_add_iff N).mpr summable_one_div_natCast_add_one_sq  have hcomp : ∀ i : ℕ, 1 / (((i + N : ℕ) : ℝ) + 1) ^ 2 ≤ u i - u (i + 1) := by    intro i    rw [hdiff i, ← one_div]    have h3 : (0 : ℝ) ≤ i := Nat.cast_nonneg i    have h4 : (0 : ℝ) < ((i : ℝ) + N) * ((i : ℝ) + 1 + N) := by      have := hpos i      nlinarith    push_cast    apply one_div_le_one_div_of_le h4    nlinarith  calc ∑' i : ℕ, 1 / (((i + N : ℕ) : ℝ) + 1) ^ 2      ≤ ∑' i : ℕ, (u i - u (i + 1)) := hsumL.tsum_le_tsum hcomp htel.summable    _ = u 0 := htel.tsum_eq    _ = (N : ℝ)⁻¹ := hu0