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
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)
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))
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
simpa only [F, H]
-- 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
⊢ Eq.{u_1 + 1} (α := R) (∏' (p : Primes), ∑' (e : ℕ), f ((↑p : ℕ) ^ e)) (∑' (n : ℕ), f n)

Tactic:
(eulerProduct_hasProd hf₁ hmul hsum hf₀).tprod_eq

Premises used: EulerProduct.eulerProduct_hasProd, HasProd.tprod_eq
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
inst_1 : CompleteSpace R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := R) ((f : (a : ℕ) → R) x : R)
⊢ HasProd.{u_1, 0} (α := R) (fun (p : Primes) ↦ ∑' (e : ℕ), (f : (a : ℕ) → R) ((↑p : ℕ) ^ e))
    (∑' (n : ℕ), (f : (a : ℕ) → R) n)

Tactic:
eulerProduct_hasProd hf.1 hf.2 hsum f.map_zero

Premises used: EulerProduct.eulerProduct_hasProd, ArithmeticFunction.map_zero, And.right, And.left
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
inst_1 : CompleteSpace R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := R) ((f : (a : ℕ) → R) x : R)
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∏ p ∈ n.primesBelow, ∑' (e : ℕ), (f : (a : ℕ) → R) (p ^ e)) atTop
    (𝓝 (∑' (n : ℕ), (f : (a : ℕ) → R) n))

Tactic:
eulerProduct hf.1 hf.2 hsum f.map_zero

Premises used: EulerProduct.eulerProduct, ArithmeticFunction.map_zero, And.right, And.left
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
inst_1 : CompleteSpace R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := R) ((f : (a : ℕ) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) (∏' (p : Primes), ∑' (e : ℕ), (f : (a : ℕ) → R) ((↑p : ℕ) ^ e))
    (∑' (n : ℕ), (f : (a : ℕ) → R) n)

Tactic:
eulerProduct_tprod hf.1 hf.2 hsum f.map_zero

Premises used: EulerProduct.eulerProduct_tprod, ArithmeticFunction.map_zero, And.right, And.left
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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)
simp :
  (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹ =
    ∑' (e : ℕ), HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) e
⊢ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹ = ∑' (e : ℕ), (f : (a : ℕ) → F) (p ^ e)

Tactic:
simp only [map_pow]

Premises used: map_pow
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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

Tactic:
(tsum_geometric_of_norm_lt_one <| summable_geometric_iff_norm_lt_one.mp ?_).symm

Premises used: tsum_geometric_of_norm_lt_one, Iff.mp, summable_geometric_iff_norm_lt_one, Eq.symm
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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)
refine : Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n
⊢ (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹ =
    ∑' (e : ℕ), HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) e

Tactic:
refine (tsum_geometric_of_norm_lt_one <| summable_geometric_iff_norm_lt_one.mp ?_).symm

Premises used: tsum_geometric_of_norm_lt_one, Iff.mp, summable_geometric_iff_norm_lt_one, Eq.symm
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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

Tactic:
Summable.of_norm ?_

Premises used: Summable.of_norm
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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)
refine : Summable (α := ℝ) fun (a : ℕ) ↦ ‖HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) a‖
⊢ Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n

Tactic:
refine Summable.of_norm ?_

Premises used: Summable.of_norm
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 (α := ℝ) fun (a : ℕ) ↦ ‖HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) a‖

Tactic:
simpa only [Function.comp_def, map_pow]
    using hsum.comp_injective <| Nat.pow_right_injective hp.one_lt

Premises used: Nat.Prime.one_lt, map_pow, Function.comp_def, Nat.pow_right_injective, Summable.comp_injective
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
⊢ ∀ {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
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
⊢ Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)

Tactic:
prod_congr rfl fun p hp ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
refine :
  ∀ (p : ℕ) (hp : p ∈ {p ∈ s | Nat.Prime p}),
    ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n) = (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹
⊢ Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)

Tactic:
refine prod_congr rfl fun p hp ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
p : ℕ
hp : p ∈ {p ∈ s | Nat.Prime p}
simp :
  ∑' (n : ℕ), HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n =
    (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹
⊢ ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n) = (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹

Tactic:
simp only [map_pow]

Premises used: map_pow
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
p : ℕ
hp : p ∈ {p ∈ s | Nat.Prime p}
⊢ ∑' (n : ℕ), HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n =
    (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹

Tactic:
tsum_geometric_of_norm_lt_one <| h (mem_filter.mp hp).2

Premises used: tsum_geometric_of_norm_lt_one, And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
p : ℕ
hp : p ∈ {p ∈ s | Nat.Prime p}
⊢ ∑' (n : ℕ), HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n =
    (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹

Tactic:
exact tsum_geometric_of_norm_lt_one <| h (mem_filter.mp hp).2

Premises used: tsum_geometric_of_norm_lt_one, And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
⊢ Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)

Tactic:
have H₁ :
      ∏ p ∈ s with p.Prime, ∑' n : ℕ, f (p ^ n) = ∏ p ∈ s with p.Prime, (1 - f p)⁻¹ := by
    refine prod_congr rfl fun p hp ↦ ?_
    simp only [map_pow]
    exact tsum_geometric_of_norm_lt_one <| h (mem_filter.mp hp).2
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
p : ℕ
hp : Nat.Prime p
simp : Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) (p ^ n) : F)

Tactic:
simp only [map_pow]

Premises used: map_pow
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
p : ℕ
hp : Nat.Prime p
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n‖

Tactic:
Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_pow_le ..) ?_

Premises used: norm_pow_le, Summable.of_nonneg_of_le, HPow.hPow, DFunLike.coe, norm_nonneg
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
p : ℕ
hp : Nat.Prime p
refine : Summable (HPow.hPow (norm (E := F) ((f : (a : ℕ) → F) p : F)))
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n‖

Tactic:
refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_pow_le ..) ?_

Premises used: Summable.of_nonneg_of_le, norm_nonneg
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
p : ℕ
hp : Nat.Prime p
⊢ Summable (HPow.hPow (norm (E := F) ((f : (a : ℕ) → F) p : F)))

Tactic:
summable_geometric_iff_norm_lt_one.mpr <| (norm_norm (f p)).symm ▸ h hp

Premises used: Iff.mpr, Eq.rec, norm_norm, summable_geometric_iff_norm_lt_one, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
p : ℕ
hp : Nat.Prime p
⊢ Summable (HPow.hPow (norm (E := F) ((f : (a : ℕ) → F) p : F)))

Tactic:
exact summable_geometric_iff_norm_lt_one.mpr <| (norm_norm (f p)).symm ▸ h hp

Premises used: Iff.mpr, summable_geometric_iff_norm_lt_one
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
⊢ ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) (p ^ n) : F)

Tactic:
have H₂ : ∀ {p : ℕ}, p.Prime → Summable fun n ↦ ‖f (p ^ n)‖ := by
    intro p hp
    simp only [map_pow]
    refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_pow_le ..) ?_
    exact summable_geometric_iff_norm_lt_one.mpr <| (norm_norm (f p)).symm ▸ h hp
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
H₂ : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) (p ^ n) : F)
⊢ (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))⁻¹)

Tactic:
H₁ ▸ summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum f.map_one hmul H₂ s

Premises used: Eq.rec, MonoidHom.map_one, EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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 ℕ
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)
H₁ :
  Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), (f : (a : ℕ) → F) (p ^ n))
    (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
H₂ : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ norm (E := F) ((f : (a : ℕ) → F) (p ^ n) : F)
⊢ (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))⁻¹)

Tactic:
exact H₁ ▸ summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum f.map_one hmul H₂ s
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
s : Finset ℕ
⊢ Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (∑' (m : (↑(factoredNumbers s) : Type)), (f : (a : ℕ) → F) (↑m : ℕ))

Tactic:
(summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric ?_ s).2.tsum_eq.symm

Premises used: EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric, HasSum.tsum_eq, And.right, Eq.symm
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
s : Finset ℕ
refine : ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1
⊢ Eq.{u_1 + 1} (α := F) (∏ p ∈ s with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (∑' (m : (↑(factoredNumbers s) : Type)), (f : (a : ℕ) → F) (↑m : ℕ))

Tactic:
refine (summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric ?_ s).2.tsum_eq.symm

Premises used: EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric, HasSum.tsum_eq, And.right, Eq.symm
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
s : Finset ℕ
⊢ ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1

Tactic:
fun {_} hp ↦ hsum.norm_lt_one hp.one_lt

Premises used: Nat.Prime.one_lt, Summable.norm_lt_one
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
s : Finset ℕ
⊢ ∀ {p : ℕ}, Nat.Prime p → norm (E := F) ((f : (a : ℕ) → F) p : F) < 1

Tactic:
exact fun {_} hp ↦ hsum.norm_lt_one hp.one_lt

Premises used: Summable.norm_lt_one
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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
N : ℕ
rw :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ norm (E := F) ((f : (a : ℕ) → F) (↑m : ℕ) : F)) ∧
    HasSum.{u_1, 0} (α := F) (fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ (f : (a : ℕ) → F) (↑m : ℕ))
      (∏ p ∈ range N with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
⊢ (Summable (α := ℝ) fun (m : (↑N.smoothNumbers : Type)) ↦ norm (E := F) ((f : (a : ℕ) → F) (↑m : ℕ) : F)) ∧
    HasSum.{u_1, 0} (α := F) (fun (m : (↑N.smoothNumbers : Type)) ↦ (f : (a : ℕ) → F) (↑m : ℕ))
      (∏ p ∈ N.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)

Tactic:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]

Premises used: Nat.smoothNumbers_eq_factoredNumbers, Nat.primesBelow
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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
N : ℕ
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ norm (E := F) ((f : (a : ℕ) → F) (↑m : ℕ) : F)) ∧
    HasSum.{u_1, 0} (α := F) (fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ (f : (a : ℕ) → F) (↑m : ℕ))
      (∏ p ∈ range N with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)

Tactic:
summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric h _

Premises used: EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
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
N : ℕ
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ norm (E := F) ((f : (a : ℕ) → F) (↑m : ℕ) : F)) ∧
    HasSum.{u_1, 0} (α := F) (fun (m : (↑(factoredNumbers (range N)) : Type)) ↦ (f : (a : ℕ) → F) (↑m : ℕ))
      (∏ p ∈ range N with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)

Tactic:
exact summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric h _

Premises used: EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
N : ℕ
rw :
  Eq.{u_1 + 1} (α := F)
    (∏ p ∈ range N with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (∑' (m : (↑(factoredNumbers (range N)) : Type)), (f : (a : ℕ) → F) (↑m : ℕ))
⊢ Eq.{u_1 + 1} (α := F) (∏ p ∈ N.primesBelow, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (∑' (m : (↑N.smoothNumbers : Type)), (f : (a : ℕ) → F) (↑m : ℕ))

Tactic:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]

Premises used: Nat.smoothNumbers_eq_factoredNumbers, Nat.primesBelow
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
N : ℕ
⊢ Eq.{u_1 + 1} (α := F)
    (∏ p ∈ range N with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (∑' (m : (↑(factoredNumbers (range N)) : Type)), (f : (a : ℕ) → F) (↑m : ℕ))

Tactic:
prod_filter_prime_geometric_eq_tsum_factoredNumbers hsum _

Premises used: EulerProduct.prod_filter_prime_geometric_eq_tsum_factoredNumbers
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedField F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
N : ℕ
⊢ Eq.{u_1 + 1} (α := F)
    (∏ p ∈ range N with Nat.Prime p, (HSub.hSub (α := F) (β := F) (1 : F) ((f : (a : ℕ) → F) p : F))⁻¹)
    (∑' (m : (↑(factoredNumbers (range N)) : Type)), (f : (a : ℕ) → F) (↑m : ℕ))

Tactic:
exact prod_filter_prime_geometric_eq_tsum_factoredNumbers hsum _

Premises used: EulerProduct.prod_filter_prime_geometric_eq_tsum_factoredNumbers