awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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)‖
s : Finset ℕ
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
have empty : (Summable (α := ℝ) fun (m : (↑(factoredNumbers ∅) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
  HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers ∅) : Type)) ↦ f (↑m : ℕ))
    (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
Tactic: induction s using Finset.induction with
  | empty =>
    rw [factoredNumbers_empty]
    simp only [notMem_empty, IsEmpty.forall_iff, forall_const, filter_true_of_mem, prod_empty]
    exact ⟨(Set.finite_singleton 1).summable (‖f ·‖), hf₁ ▸ hasSum_singleton 1 f⟩
  | insert p s hp ih =>
    rw [filter_insert]
    split_ifs with hpp
    · constructor
      · simp only [← (equivProdNatFactoredNumbers hpp hp).summable_iff, Function.comp_def,
          equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
        refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_mul_le ..) ?_
        apply Summable.mul_of_nonneg (hsum hpp) ih.1 <;> exact fun n ↦ norm_nonneg _
      · have hp' : p ∉ {p ∈ s | p.Prime} := mt (mem_of_mem_filter p) hp
        rw [prod_insert hp', ← (equivProdNatFactoredNumbers hpp hp).hasSum_iff, Function.comp_def]
        conv =>
          enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
        have : T3Space R := instT3Space -- speeds up the following
        apply (hsum hpp).of_norm.hasSum.mul ih.2
        -- `exact summable_mul_of_summable_norm (hsum hpp) ih.1` gives a time-out
        apply summable_mul_of_summable_norm (hsum hpp) ih.1
    · rwa [factoredNumbers_insert s hpp]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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)‖
s : Finset ℕ
empty :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers ∅) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers ∅) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
have insert : ∀ (p : ℕ) (s : Finset ℕ) (hp : p ∉ s)
  (ih :
    (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
      HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
        (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))),
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ insert p s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
Tactic: induction s using Finset.induction with
  | empty =>
    rw [factoredNumbers_empty]
    simp only [notMem_empty, IsEmpty.forall_iff, forall_const, filter_true_of_mem, prod_empty]
    exact ⟨(Set.finite_singleton 1).summable (‖f ·‖), hf₁ ▸ hasSum_singleton 1 f⟩
  | insert p s hp ih =>
    rw [filter_insert]
    split_ifs with hpp
    · constructor
      · simp only [← (equivProdNatFactoredNumbers hpp hp).summable_iff, Function.comp_def,
          equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
        refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_mul_le ..) ?_
        apply Summable.mul_of_nonneg (hsum hpp) ih.1 <;> exact fun n ↦ norm_nonneg _
      · have hp' : p ∉ {p ∈ s | p.Prime} := mt (mem_of_mem_filter p) hp
        rw [prod_insert hp', ← (equivProdNatFactoredNumbers hpp hp).hasSum_iff, Function.comp_def]
        conv =>
          enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
        have : T3Space R := instT3Space -- speeds up the following
        apply (hsum hpp).of_norm.hasSum.mul ih.2
        -- `exact summable_mul_of_summable_norm (hsum hpp) ih.1` gives a time-out
        apply summable_mul_of_summable_norm (hsum hpp) ih.1
    · rwa [factoredNumbers_insert s hpp]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
⊢ ∃ (N : ℕ),
    ∀ (s : Finset ℕ),
      N.primesBelow ≤ s →
        ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
have 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 : ℕ))‖ < ε
Tactic: obtain ⟨N, hN⟩ :=
    summable_iff_nat_tsum_vanishing.mp hsum (Metric.ball 0 ε) <| Metric.ball_mem_nhds 0 εpos
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
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 : ℕ))
⊢ ∃ (N : ℕ),
    ∀ (s : Finset ℕ),
      N.primesBelow ≤ s →
        ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
have hN₁ : ∀ t ⊆ {n : ℕ | N ≤ n}, norm.{u_1} (E := R) (∑' (n : (↑t : Type)), f (↑n : ℕ)) < ε
Tactic: simp_rw [mem_ball_zero_iff] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 : ℕ))‖ < ε
have refine : ∀ (s : Finset ℕ) (hs : N.primesBelow ≤ s),
  ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
Tactic: refine ⟨N, fun s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
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
⊢ ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
have this : norm.{u_1} (E := R) (∑' (n : (↑((factoredNumbers s)ᶜ \ {0}) : Type)), f (↑n : ℕ)) < ε
Tactic: have := hN _ <| factoredNumbers_compl hs
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 : ℕ)) < ε
⊢ ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
have rwa : ‖HAdd.hAdd (α := R) (∑' (x : (↑(factoredNumbers s) : Type)), f (↑x : ℕ))
        (∑' (x : (↑(factoredNumbers s)ᶜ : Type)), f (↑x : ℕ)) -
      ∑' (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₀]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 : ℕ)‖ <
    ε
⊢ ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ < ε
have rwa₁ : norm.{u_1} (E := R) (∑' (x : (↑(factoredNumbers s)ᶜ : Type)), f (↑x : ℕ)) < ε
Tactic: rwa [← hsum.tsum_subtype_add_tsum_subtype_compl (factoredNumbers s),
    add_sub_cancel_left, tsum_eq_tsum_diff_singleton (factoredNumbers s)ᶜ hf₀]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 : (↑N.smoothNumbers : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑N.smoothNumbers : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n))
have 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))
Tactic: rw [smoothNumbers_eq_factoredNumbers, primesBelow]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε
have enter : ∀ (N₀ N : ℕ), N ≥ N₀ → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε
Tactic: enter [1, N₀, N]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 : ℕ
| N ≥ N₀ → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε
have rw : N ≥ N₀ → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε
Tactic: rw [smoothNumbers_eq_factoredNumbers]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε
have enter : ∀ (N₀ N : ℕ),
  N ≥ N₀ → ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε
Tactic: enter [1, N₀, N]; rw [smoothNumbers_eq_factoredNumbers]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑N.smoothNumbers : Type)), f (↑m : ℕ))‖ < ε
have conv : ∃ (N₀ : ℕ),
  ∀ N ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε
Tactic: conv => enter [1, N₀, N]; rw [smoothNumbers_eq_factoredNumbers]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 ≥ N₀, ‖HSub.hSub (α := R) (∑' (m : ℕ), f m) (∑' (m : (↑(factoredNumbers (range N)) : Type)), f (↑m : ℕ))‖ < ε
have 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 : ℕ))‖ < ε
Tactic: obtain ⟨N₀, hN₀⟩ := norm_tsum_factoredNumbers_sub_tsum_lt hsum hf₀ εpos
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 : ℕ))‖ < ε
have refine : ∀ (N : ℕ) (hN : N ≥ N₀) (p : ℕ) (hp : p ∈ N₀.primesBelow), p ∈ range N
Tactic: refine ⟨N₀, fun N hN ↦ hN₀ (range N) fun p hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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)
⊢ HasProd.{u_1, 0} (α := R) (fun (p : Primes) ↦ ∑' (e : ℕ), f ((↑p : ℕ) ^ e)) (∑' (n : ℕ), f n)
have 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)
Tactic: change HasProd (F ∘ Subtype.val (p := (· ∈ {x | Nat.Prime x}))) _
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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)
⊢ 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)
have 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) <
        ε
Tactic: rw [hasProd_subtype_iff_mulIndicator, HasProd, SummationFilter.unconditional,
    Metric.tendsto_atTop]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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 : Finset ℕ),
    ∀ n ≥ N,
      dist.{u_1} (α := R) (∏ b ∈ n, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
          (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
        ε
have 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) <
        ε
Tactic: obtain ⟨N₀, hN₀⟩ := norm_tsum_factoredNumbers_sub_tsum_lt hsum.of_norm hf₀ hε
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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) <
        ε
have 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) <
    ε
Tactic: refine ⟨range N₀, fun s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
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₀
⊢ dist.{u_1} (α := R) (∏ b ∈ s, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
      (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
    ε
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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)
⊢ dist.{u_1} (α := R) (∏ b ∈ s, Set.mulIndicator {x : ℕ | Nat.Prime x} F b)
      (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n) <
    ε
have rw : ‖HSub.hSub (α := R) (∑'[{ filter := Filter.atTop : SummationFilter ℕ }] (n : ℕ), f n)
      (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))‖ <
  ε
Tactic: rw [this, dist_eq_norm, prod_filter_prime_tsum_eq_tsum_factoredNumbers hf₁ hmul hsum,
    norm_sub_rev]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
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) (Set.mulIndicator {p : ℕ | Nat.Prime p} fun (p : ℕ) ↦ ∑' (e : ℕ), f (p ^ e))
    (∑' (n : ℕ), f n)
have 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)
Tactic: rw [← hasProd_subtype_iff_mulIndicator]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
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 : ℕ) ↦ ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))
have 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))
Tactic: have := (eulerProduct_hasProd_mulIndicator hf₁ hmul hsum hf₀).tendsto_prod_nat
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
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)
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))
have H : ∀ (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
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
⊢ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹ = ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e)
have simp : (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹ =
  ∑' (e : ℕ), HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) e
Tactic: simp only [map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
⊢ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹ =
    ∑' (e : ℕ), HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) e
have refine : Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n
Tactic: refine (tsum_geometric_of_norm_lt_one <| summable_geometric_iff_norm_lt_one.mp ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (goal)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) x : F)
⊢ Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n
have refine : Summable (α := ℝ) fun (a : ℕ) ↦ ‖HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) a‖
Tactic: refine Summable.of_norm ?_
-- Lean 4 proof step from Mathlib.NumberTheory.EulerProduct.Basic (hypothesis)
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
s : Finset ℕ
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ norm (E := F) ((f : (a : ℕ) → F) (↑m : ℕ) : F)) ∧
    HasSum.{u_1, 0} (α := F) (fun (m : (↑(factoredNumbers s) : Type)) ↦ (f : (a : ℕ) → F) (↑m : ℕ))
      (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
have hmul : ∀ {m n : ℕ},
  m.Coprime n →
    (f : (a : ℕ) → F) (m * n) = HMul.hMul (α := F) (β := F) ((f : (a : ℕ) → F) m : F) ((f : (a : ℕ) → F) n : F)
Tactic: have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n