-- Mathlib/NumberTheory/EulerProduct/Basic.lean
theorem eulerProduct_completely_multiplicative {f : ℕ →*₀ F} (hsum : Summable (‖f ·‖)) :
    Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, (1 - f p)⁻¹) atTop (𝓝 (∑' n, f n))

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

Tactic:
have H' : {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) =
            {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' e : ℕ, f (p ^ e)) :=
  Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum

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

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

Tactic:
simpa only [← H, H'] using this

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x => ‖f x‖
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
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, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
have H (n : ℕ) : ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p =
                   ∏ p ∈ primesBelow n, (1 - f p)⁻¹ :=
  prod_mulIndicator_eq_prod_filter
    (range n) (fun _ ↦ fun p ↦ (1 - f p)⁻¹) (fun _ ↦ {p | Nat.Prime p}) id

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

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x => ‖f x‖
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x => ‖f x‖
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x => ‖f x‖
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
have := (eulerProduct_hasProd_mulIndicator f.map_one hmul hsum f.map_zero).tendsto_prod_nat

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x => ‖f x‖
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
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, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))