-- Mathlib/NumberTheory/EulerProduct/Basic.lean
theorem eulerProduct (hsum : Summable (‖f ·‖)) (hf₀ : f 0 = 0) :
    Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, ∑' e, f (p ^ e)) atTop (𝓝 (∑' n, f n))

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
this :
  Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
let F : ℕ → R := fun p ↦ ∑' (e : ℕ), f (p ^ e)

Result:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
this :
  Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
F : ℕ → R := fun p => ∑' (e : ℕ), f (p ^ e)
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
this :
  Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
F : ℕ → R := fun p => ∑' (e : ℕ), f (p ^ e)
H : ∀ (n : ℕ), ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator F i = ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
simpa only [F, H]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
this :
  Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
F : ℕ → R := fun p => ∑' (e : ℕ), f (p ^ e)
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
have H (n : ℕ) : ∏ i ∈ range n, Set.mulIndicator {p | Nat.Prime p} F i =
                   ∏ p ∈ primesBelow n, ∑' (e : ℕ), f (p ^ e) :=
  prod_mulIndicator_eq_prod_filter (range n) (fun _ ↦ F) (fun _ ↦ {p | Nat.Prime p}) id

Result:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
this :
  Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
F : ℕ → R := fun p => ∑' (e : ℕ), f (p ^ e)
H : ∀ (n : ℕ), ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator F i = ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
have := (eulerProduct_hasProd_mulIndicator hf₁ hmul hsum hf₀).tendsto_prod_nat

Result:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
this :
  Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))