-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- The following statement says that summing over `s`-factored numbers such that
`s` contains `primesBelow N` for large enough `N` gets us arbitrarily close to the sum
over all natural numbers (assuming `f` is summable and `f 0 = 0`; the latter since
`0` is not `s`-factored). -/
lemma norm_tsum_factoredNumbers_sub_tsum_lt (hsum : Summable f) (hf₀ : f 0 = 0) {ε : ℝ}
    (εpos : 0 < ε) :
    ∃ N : ℕ, ∀ s : Finset ℕ, primesBelow N ≤ s →
      ‖(∑' m : ℕ, f m) - ∑' m : factoredNumbers s, f m‖ < ε

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
⊢ ∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Tactic:
obtain ⟨N, hN⟩ :=
  summable_iff_nat_tsum_vanishing.mp hsum (Metric.ball 0 ε) <| Metric.ball_mem_nhds 0 εpos

Result:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ Metric.ball 0 ε
⊢ ∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Proof state:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ Metric.ball 0 ε
⊢ ∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Tactic:
simp_rw [mem_ball_zero_iff] at hN

Result:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
⊢ ∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Proof state:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
s : Finset ℕ
hs : N.primesBelow ≤ s
⊢ ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Tactic:
have := hN _ <| factoredNumbers_compl hs

Result:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
s : Finset ℕ
hs : N.primesBelow ≤ s
this : ‖∑' (n : ↑((factoredNumbers s)ᶜ \ {0})), f ↑n‖ < ε
⊢ ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Proof state:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
s : Finset ℕ
hs : N.primesBelow ≤ s
this : ‖∑' (n : ↑((factoredNumbers s)ᶜ \ {0})), f ↑n‖ < ε
⊢ ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Tactic:
rwa [← tsum_subtype_add_tsum_subtype_compl hsum (factoredNumbers s),
  add_sub_cancel_left, tsum_eq_tsum_diff_singleton (factoredNumbers s)ᶜ hf₀]

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
⊢ ∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Tactic:
refine ⟨N, fun s hs ↦ ?_⟩

Result:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
s : Finset ℕ
hs : N.primesBelow ≤ s
⊢ ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε