Theorem: infinity_of_primes₆ (FormalBook/Chapter_01.lean)

State before:
⊢ Tendsto (fun n => ∑ p ∈ filter (fun p => p.Prime) (range n), 1 / ↑p) atTop atTop
Tactic:
sorry
State after:
no goals