A limit of a series

Stream: Is there code for X?

[Michael Stoll]

I managed to produce a proof of the following:

import Mathlib

open Filter Set Topology in
lemma partialZetaSum_inv_tendsto_zero_of_not_summable {A : Set ℕ}
    (hA : ¬ Summable (indicator A fun n : ℕ ↦ 1 / (n : ℝ))) :
    Tendsto (fun s : ℝ ↦ (∑' n, indicator A (fun n ↦ (n : ℝ) ^ (-s)) n)⁻¹) (𝓝[>] 1) (𝓝 0) := by
  sorry

but it is perhaps a bit clumsy (I'm going back to epsilons and deltas), and I was wondering if there is a more elegant way using the filter machinery. Any suggestions?