awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
obtain :
  ∀ (N : ℕ)
    (hN : ∀ t ⊆ {n : ℕ | N ≤ n}, Membership.mem (γ := Set R) (Metric.ball 0 ε) (∑' (n : (↑t : Type)), f (↑n : ℕ))),
    ∃ (N : ℕ),
      ∀ (s : Finset ℕ),
        N.primesBelow ≤ s →
          ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
⊢ ∃ (N : ℕ),
    ∀ (s : Finset ℕ),
      N.primesBelow ≤ s →
        ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε

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

Premises used: Metric.ball, Metric.ball_mem_nhds, Iff.mp, OfNat.ofNat, summable_iff_nat_tsum_vanishing
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n : ℕ | N ≤ n}, Membership.mem (γ := Set R) (Metric.ball 0 ε) (∑' (n : (↑t : Type)), f (↑n : ℕ))
⊢ ∀ t ⊆ {n : ℕ | N ≤ n}, norm.{u_1} (E := R) (∑' (n : (↑t : Type)), f (↑n : ℕ)) < ε

Tactic:
simp_rw [mem_ball_zero_iff] at hN

Premises used: mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n : ℕ | N ≤ n}, norm.{u_1} (E := R) (∑' (n : (↑t : Type)), f (↑n : ℕ)) < ε
⊢ ∃ (N : ℕ),
    ∀ (s : Finset ℕ),
      N.primesBelow ≤ s →
        ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε

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

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n : ℕ | N ≤ n}, norm.{u_1} (E := R) (∑' (n : (↑t : Type)), f (↑n : ℕ)) < ε
refine :
  ∀ (s : Finset ℕ) (hs : N.primesBelow ≤ s),
    ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
⊢ ∃ (N : ℕ),
    ∀ (s : Finset ℕ),
      N.primesBelow ≤ s →
        ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε

Tactic:
refine ⟨N, fun s hs ↦ ?_⟩
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n : ℕ | N ≤ n}, norm.{u_1} (E := R) (∑' (n : (↑t : Type)), f (↑n : ℕ)) < ε
s : Finset ℕ
hs : N.primesBelow ≤ s
⊢ norm.{u_1} (E := R) (∑' (n : (↑((factoredNumbers s)ᶜ \ {0}) : Type)), f (↑n : ℕ)) < ε

Tactic:
have := hN _ <| factoredNumbers_compl hs
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n : ℕ | N ≤ n}, norm.{u_1} (E := R) (∑' (n : (↑t : Type)), f (↑n : ℕ)) < ε
s : Finset ℕ
hs : N.primesBelow ≤ s
this : norm.{u_1} (E := R) (∑' (n : (↑((factoredNumbers s)ᶜ \ {0}) : Type)), f (↑n : ℕ)) < ε
rwa :
  ‖HAdd.hAdd (α := R) (∑' (x : (↑(factoredNumbers s) : Type)), f (↑x : ℕ))
          (∑' (x : (↑(factoredNumbers s)ᶜ : Type)), f (↑x : ℕ)) -
        ∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ)‖ <
    ε
rwa₁ : norm.{u_1} (E := R) (∑' (x : (↑(factoredNumbers s)ᶜ : Type)), f (↑x : ℕ)) < ε
rwa₂ rwa₃ rwa₄ rwa₅ : norm.{u_1} (E := R) (∑' (a : (↑((factoredNumbers s)ᶜ \ {0}) : Type)), f (↑a : ℕ)) < ε
⊢ ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε

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

Premises used: add_sub_cancel_left, tsum_eq_tsum_diff_singleton, Compl.compl, Summable.tsum_subtype_add_tsum_subtype_compl, Nat.factoredNumbers
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
N : ℕ
rw :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ range N with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
⊢ (Summable (α := ℝ) fun (m : (↑N.smoothNumbers : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑N.smoothNumbers : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n))

Tactic:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]

Premises used: Nat.smoothNumbers_eq_factoredNumbers, Nat.primesBelow
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
N : ℕ
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ range N with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))

Tactic:
summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum hf₁ hmul hsum _

Premises used: EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
N : ℕ
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ range N with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))

Tactic:
exact summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum hf₁ hmul hsum _

Premises used: EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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‖
N : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n)) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))

Tactic:
(summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum hf₁ hmul
    (fun hp ↦ hsum.comp_injective <| Nat.pow_right_injective hp.one_lt) _).2.tsum_eq.symm

Premises used: Nat.Prime.one_lt, HasSum.tsum_eq, And.right, Nat.pow_right_injective, Summable.comp_injective, EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum, Eq.symm
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
enter :
  ∀ (N₀ N : ℕ), N ≥ N₀ → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε
| ∃ (N₀ : ℕ), ∀ N ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε

Tactic:
enter [1, N₀, N]
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ N : ℕ
rw : N ≥ N₀ → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε
| N ≥ N₀ → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε

Tactic:
rw [smoothNumbers_eq_factoredNumbers]

Premises used: Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
enter :
  ∀ (N₀ N : ℕ),
    N ≥ N₀ → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε
| ∃ (N₀ : ℕ), ∀ N ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε

Tactic:
enter [1, N₀, N]; rw [smoothNumbers_eq_factoredNumbers]

Premises used: Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
conv :
  ∃ (N₀ : ℕ),
    ∀ N ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε
⊢ ∃ (N₀ : ℕ), ∀ N ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε

Tactic:
conv => enter [1, N₀, N]; rw [smoothNumbers_eq_factoredNumbers]

Premises used: Nat.smoothNumbers_eq_factoredNumbers
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
obtain :
  ∀ (N₀ : ℕ)
    (hN₀ :
      ∀ (s : Finset ℕ),
        N₀.primesBelow ≤ s →
          ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε),
    ∃ (N₀ : ℕ),
      ∀ N ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε
⊢ ∃ (N₀ : ℕ),
    ∀ N ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε

Tactic:
obtain ⟨N₀, hN₀⟩ := norm_tsum_factoredNumbers_sub_tsum_lt hsum hf₀ εpos

Premises used: EulerProduct.norm_tsum_factoredNumbers_sub_tsum_lt
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
⊢ ∃ (N₀ : ℕ),
    ∀ N ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε

Tactic:
⟨N₀, fun N hN ↦ hN₀ (range N) fun p hp ↦ ?_⟩

Premises used: Finset.range, Exists.intro
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
refine : ∀ (N : ℕ) (hN : N ≥ N₀) (p : ℕ) (hp : p ∈ N₀.primesBelow), p ∈ range N
⊢ ∃ (N₀ : ℕ),
    ∀ N ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε

Tactic:
refine ⟨N₀, fun N hN ↦ hN₀ (range N) fun p hp ↦ ?_⟩
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
N : ℕ
hN : N ≥ N₀
p : ℕ
hp : p ∈ N₀.primesBelow
⊢ p ∈ range N

Tactic:
mem_range.mpr <| (lt_of_mem_primesBelow hp).trans_le hN

Premises used: Iff.mpr, Nat.lt_of_mem_primesBelow, Finset.mem_range, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
N : ℕ
hN : N ≥ N₀
p : ℕ
hp : p ∈ N₀.primesBelow
⊢ p ∈ range N

Tactic:
exact mem_range.mpr <| (lt_of_mem_primesBelow hp).trans_le hN

Premises used: Iff.mpr, Nat.lt_of_mem_primesBelow, Finset.mem_range, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
F : ℕ → R := fun (n : ℕ) ↦ ∑' (e : ℕ), f (n ^ e)
change :
  HasProd (β := { x : ℕ // Membership.mem (γ := Set ℕ) {x : ℕ | Nat.Prime x} x })
    (F ∘ Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {x : ℕ | Nat.Prime x} x)) (∑' (n : ℕ), f n)
⊢ HasProd.{u_1, 0} (α := R) (fun (p : Primes) ↦ ∑' (e : ℕ), f ((↑p : ℕ) ^ e)) (∑' (n : ℕ), f n)

Tactic:
change HasProd (F ∘ Subtype.val (p := (· ∈ {x | Nat.Prime x}))) _

Premises used: HasProd, Function.comp, Subtype.val, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
F : ℕ → R := fun (n : ℕ) ↦ ∑' (e : ℕ), f (n ^ e)
rw :
  ∀ ε > 0,
    ∃ (N : Finset ℕ),
      ∀ n ≥ N,
        dist.{u_1} (α := R) (∏ b ∈ n, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
            (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
          ε
⊢ HasProd (β := { x : ℕ // Membership.mem (γ := Set ℕ) {x : ℕ | Nat.Prime x} x })
    (F ∘ Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {x : ℕ | Nat.Prime x} x)) (∑' (n : ℕ), f n)

Tactic:
rw [hasProd_subtype_iff_mulIndicator, HasProd, SummationFilter.unconditional,
    Metric.tendsto_atTop]

Premises used: Metric.tendsto_atTop, hasProd_subtype_iff_mulIndicator, HasProd, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
F : ℕ → R := fun (n : ℕ) ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
obtain :
  ∀ (N₀ : ℕ)
    (hN₀ :
      ∀ (s : Finset ℕ),
        N₀.primesBelow ≤ s →
          ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε),
    ∃ (N : Finset ℕ),
      ∀ n ≥ N,
        dist.{u_1} (α := R) (∏ b ∈ n, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
            (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
          ε
⊢ ∃ (N : Finset ℕ),
    ∀ n ≥ N,
      dist.{u_1} (α := R) (∏ b ∈ n, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
          (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
        ε

Tactic:
obtain ⟨N₀, hN₀⟩ := norm_tsum_factoredNumbers_sub_tsum_lt hsum.of_norm hf₀ hε

Premises used: Summable.of_norm, EulerProduct.norm_tsum_factoredNumbers_sub_tsum_lt
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
F : ℕ → R := fun (n : ℕ) ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
⊢ ∃ (N : Finset ℕ),
    ∀ n ≥ N,
      dist.{u_1} (α := R) (∏ b ∈ n, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
          (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
        ε

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

Premises used: Finset.range, Exists.intro
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
F : ℕ → R := fun (n : ℕ) ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
refine :
  ∀ (s : Finset ℕ) (hs : s ≥ range N₀),
    dist.{u_1} (α := R) (∏ b ∈ s, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
        (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
      ε
⊢ ∃ (N : Finset ℕ),
    ∀ n ≥ N,
      dist.{u_1} (α := R) (∏ b ∈ n, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
          (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
        ε

Tactic:
refine ⟨range N₀, fun s hs ↦ ?_⟩
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
F : ℕ → R := fun (n : ℕ) ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
s : Finset ℕ
hs : s ≥ range N₀
⊢ Eq.{u_1 + 1} (α := R) (∏ p ∈ s, Set.mulIndicator {p : ℕ | Nat.Prime p} F p) (∏ p ∈ s with Nat.Prime p, F p)

Tactic:
have : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ s with p.Prime, F p :=
    prod_mulIndicator_eq_prod_filter s (fun _ ↦ F) _ id
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
F : ℕ → R := fun (n : ℕ) ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
s : Finset ℕ
hs : s ≥ range N₀
this : Eq.{u_1 + 1} (α := R) (∏ p ∈ s, Set.mulIndicator {p : ℕ | Nat.Prime p} F p) (∏ p ∈ s with Nat.Prime p, F p)
rw :
  ‖HSub.hSub (α := R) (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n)
        (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ <
    ε
⊢ dist.{u_1} (α := R) (∏ b ∈ s, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
      (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
    ε

Tactic:
rw [this, dist_eq_norm, prod_filter_prime_tsum_eq_tsum_factoredNumbers hf₁ hmul hsum,
    norm_sub_rev]

Premises used: dist_eq_norm, EulerProduct.prod_filter_prime_tsum_eq_tsum_factoredNumbers, norm_sub_rev
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
F : ℕ → R := fun (n : ℕ) ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
s : Finset ℕ
hs : s ≥ range N₀
this : Eq.{u_1 + 1} (α := R) (∏ p ∈ s, Set.mulIndicator {p : ℕ | Nat.Prime p} F p) (∏ p ∈ s with Nat.Prime p, F p)
⊢ ‖HSub.hSub (α := R) (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n)
        (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ <
    ε

Tactic:
hN₀ s fun p hp ↦ hs <| mem_range.mpr <| lt_of_mem_primesBelow hp

Premises used: Iff.mpr, Nat.lt_of_mem_primesBelow, Finset.mem_range, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
F : ℕ → R := fun (n : ℕ) ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ :
  ∀ (s : Finset ℕ),
    N₀.primesBelow ≤ s → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
s : Finset ℕ
hs : s ≥ range N₀
this : Eq.{u_1 + 1} (α := R) (∏ p ∈ s, Set.mulIndicator {p : ℕ | Nat.Prime p} F p) (∏ p ∈ s with Nat.Prime p, F p)
⊢ ‖HSub.hSub (α := R) (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n)
        (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ <
    ε

Tactic:
exact hN₀ s fun p hp ↦ hs <| mem_range.mpr <| lt_of_mem_primesBelow hp

Premises used: Iff.mpr, Nat.lt_of_mem_primesBelow, Finset.mem_range
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
rw :
  HasProd.{u_1, 0} (α := R) (β := (↑{p : ℕ | Nat.Prime p} : Type))
    ((fun (p : ℕ) ↦ ∑' (e : ℕ), f (p ^ e)) ∘
      Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {p : ℕ | Nat.Prime p} x))
    (∑' (n : ℕ), f n)
⊢ HasProd.{u_1, 0} (α := R) (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦ ∑' (e : ℕ), f (p ^ e))
    (∑' (n : ℕ), f n)

Tactic:
rw [← hasProd_subtype_iff_mulIndicator]

Premises used: hasProd_subtype_iff_mulIndicator
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
⊢ HasProd.{u_1, 0} (α := R) (β := (↑{p : ℕ | Nat.Prime p} : Type))
    ((fun (p : ℕ) ↦ ∑' (e : ℕ), f (p ^ e)) ∘
      Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {p : ℕ | Nat.Prime p} x))
    (∑' (n : ℕ), f n)

Tactic:
eulerProduct_hasProd hf₁ hmul hsum hf₀

Premises used: Nat.Prime, Set.Mem, EulerProduct.eulerProduct_hasProd, setOf, Nat.Primes, tsum
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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
⊢ HasProd.{u_1, 0} (α := R) (β := (↑{p : ℕ | Nat.Prime p} : Type))
    ((fun (p : ℕ) ↦ ∑' (e : ℕ), f (p ^ e)) ∘
      Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {p : ℕ | Nat.Prime p} x))
    (∑' (n : ℕ), f n)

Tactic:
exact eulerProduct_hasProd hf₁ hmul hsum hf₀

Premises used: EulerProduct.eulerProduct_hasProd
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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.{0, u_1} (β := R)
    (fun (n : ℕ) ↦ ∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} (fun (p : ℕ) ↦ ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))

Tactic:
have := (eulerProduct_hasProd_mulIndicator hf₁ hmul hsum hf₀).tendsto_prod_nat
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : 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.{0, u_1} (β := R)
    (fun (n : ℕ) ↦ ∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} (fun (p : ℕ) ↦ ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
F : ℕ → R := fun (p : ℕ) ↦ ∑' (e : ℕ), f (p ^ e)
⊢ ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R) (∏ i ∈ range n, Set.mulIndicator {p : ℕ | Nat.Prime p} F i)
      (∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e))

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