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 : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
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))
insert :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers (Insert.insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (Insert.insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ if Nat.Prime p then Insert.insert p ({p ∈ s | Nat.Prime p}) else {p ∈ s | Nat.Prime p},
        ∑' (n : ℕ), f (p ^ n))
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers (Insert.insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (Insert.insert p s)) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ Insert.insert p s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))

Tactic:
rw [filter_insert]

Premises used: Finset.filter_insert
-- 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)‖
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))
pos :
  ∀ (hpp : Nat.Prime p),
    (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
      HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
        (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
neg :
  ∀ (hpp : ¬Nat.Prime p),
    (Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
      HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
        (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ 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 ∈ if Nat.Prime p then insert p ({p ∈ s | Nat.Prime p}) else {p ∈ s | Nat.Prime p}, ∑' (n : ℕ), f (p ^ n))

Tactic:
split_ifs with hpp
-- 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)‖
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))
hpp : Nat.Prime p
pos : Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖
pos₁ :
  HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
    (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ 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 : ℕ))
      (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))

Tactic:
constructor
-- 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)‖
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))
hpp : Nat.Prime p
pos : Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1) * f (↑x.2 : ℕ)‖
⊢ Summable (α := ℝ) fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖

Tactic:
simp only [← (equivProdNatFactoredNumbers hpp hp).summable_iff, Function.comp_def,
          equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]

Premises used: Nat.factoredNumbers.map_prime_pow_mul, Nat.equivProdNatFactoredNumbers, Function.comp_def, Equiv.summable_iff, Nat.equivProdNatFactoredNumbers_apply'
-- 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)‖
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))
hpp : Nat.Prime p
⊢ Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1) * f (↑x.2 : ℕ)‖

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

Premises used: HMul.hMul, Summable.of_nonneg_of_le, Prod.fst, HPow.hPow, norm_mul_le, Subtype.val, Prod.snd, norm_nonneg
-- 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)‖
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))
hpp : Nat.Prime p
pos : Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1)‖ * ‖f (↑x.2 : ℕ)‖
⊢ Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1) * f (↑x.2 : ℕ)‖

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

Premises used: Summable.of_nonneg_of_le, norm_nonneg
-- 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)‖
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))
hpp : Nat.Prime p
pos : LE.le (α := ℕ → ℝ) 0 fun (n : ℕ) ↦ ‖f (p ^ n)‖
pos₁ : LE.le (α := (↑(factoredNumbers s) : Type) → ℝ) 0 fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖
⊢ Summable (α := ℝ) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ ‖f (p ^ x.1)‖ * ‖f (↑x.2 : ℕ)‖

Tactic:
apply Summable.mul_of_nonneg (hsum hpp) ih.1

Premises used: Summable.mul_of_nonneg, And.left
-- 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)‖
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))
hpp : Nat.Prime p
⊢ LE.le (α := ℕ → ℝ) 0 fun (n : ℕ) ↦ ‖f (p ^ n)‖

Tactic:
fun n ↦ norm_nonneg _

Premises used: HPow.hPow, norm_nonneg
-- 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)‖
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))
hpp : Nat.Prime p
⊢ LE.le (α := ℕ → ℝ) 0 fun (n : ℕ) ↦ ‖f (p ^ n)‖

Tactic:
exact fun n ↦ norm_nonneg _

Premises used: norm_nonneg
-- 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)‖
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))
hpp : Nat.Prime p
⊢ LE.le (α := (↑(factoredNumbers s) : Type) → ℝ) 0 fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖

Tactic:
fun n ↦ norm_nonneg _

Premises used: Subtype.val, norm_nonneg
-- 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)‖
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))
hpp : Nat.Prime p
⊢ LE.le (α := (↑(factoredNumbers s) : Type) → ℝ) 0 fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖

Tactic:
exact fun n ↦ norm_nonneg _

Premises used: norm_nonneg
-- 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)‖
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))
hpp : Nat.Prime p
⊢ p ∉ {p ∈ s | Nat.Prime p}

Tactic:
have hp' : p ∉ {p ∈ s | p.Prime} := mt (mem_of_mem_filter p) hp
-- 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)‖
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))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
pos :
  HasSum
    (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
      f
        (↑((equivProdNatFactoredNumbers hpp hp :
                (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
              x) :
          ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))
⊢ HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (insert p s)) : Type)) ↦ f (↑m : ℕ))
    (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))

Tactic:
rw [prod_insert hp', ← (equivProdNatFactoredNumbers hpp hp).hasSum_iff, Function.comp_def]

Premises used: Finset.prod_insert, Equiv.hasSum_iff, Nat.equivProdNatFactoredNumbers, Function.comp_def
-- 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)‖
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))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
h :
  ∀ (x : ℕ × (↑(factoredNumbers s) : Type)),
    f
      (↑((equivProdNatFactoredNumbers hpp hp :
              (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
            x) :
        ℕ)
| HasSum
    (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
      f
        (↑((equivProdNatFactoredNumbers hpp hp :
                (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
              x) :
          ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))

Tactic:
enter [1, x]
-- 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)‖
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))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
x : ℕ × (↑(factoredNumbers s) : Type)
h : f (p ^ x.1) * f (↑x.2 : ℕ)
| f
    (↑((equivProdNatFactoredNumbers hpp hp :
            (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
          x) :
      ℕ)

Tactic:
rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]

Premises used: Nat.factoredNumbers.map_prime_pow_mul, Nat.equivProdNatFactoredNumbers_apply'
-- 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)‖
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))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
h : ∀ (x : ℕ × (↑(factoredNumbers s) : Type)), f (p ^ x.1) * f (↑x.2 : ℕ)
| HasSum
    (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
      f
        (↑((equivProdNatFactoredNumbers hpp hp :
                (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
              x) :
          ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))

Tactic:
enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]

Premises used: Nat.factoredNumbers.map_prime_pow_mul, Nat.equivProdNatFactoredNumbers_apply'
-- 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)‖
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))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
pos :
  HasSum (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ f (p ^ x.1) * f (↑x.2 : ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))
⊢ HasSum
    (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦
      f
        (↑((equivProdNatFactoredNumbers hpp hp :
                (a : ℕ × (↑(factoredNumbers s) : Type)) → (↑(factoredNumbers (insert p s)) : Type))
              x) :
          ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))

Tactic:
conv =>
          enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]

Premises used: Nat.factoredNumbers.map_prime_pow_mul, Nat.equivProdNatFactoredNumbers_apply'
-- 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)‖
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))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
⊢ T3Space R

Tactic:
have : T3Space R := instT3Space
-- 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)‖
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))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
this : T3Space R
pos : Summable.{u_1, 0} (α := R) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ f (p ^ x.1) * f (↑x.2 : ℕ)
⊢ HasSum (fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ f (p ^ x.1) * f (↑x.2 : ℕ))
    (HMul.hMul (α := R) (∑' (n : ℕ), f (p ^ n)) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n)))

Tactic:
apply (hsum hpp).of_norm.hasSum.mul ih.2

Premises used: Summable.of_norm, And.right, Summable.hasSum, HasSum.mul
-- 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)‖
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))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
this : T3Space R
⊢ Summable.{u_1, 0} (α := R) fun (x : ℕ × (↑(factoredNumbers s) : Type)) ↦ f (p ^ x.1) * f (↑x.2 : ℕ)

Tactic:
apply summable_mul_of_summable_norm (hsum hpp) ih.1

Premises used: summable_mul_of_summable_norm, And.left
-- 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)‖
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))
hpp : ¬Nat.Prime p
neg neg₁ neg₂ neg₃ :
  (Summable (α := ℝ) fun (m : (↑(factoredNumbers s) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers s) : Type)) ↦ f (↑m : ℕ))
      (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ 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 : ℕ))
      (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n))

Tactic:
rwa [factoredNumbers_insert s hpp]

Premises used: Nat.factoredNumbers_insert
-- 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)‖
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))
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.insert p s)) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
      HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers (Insert.insert p s)) : Type)) ↦ f (↑m : ℕ))
        (∏ p ∈ Insert.insert p s 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))

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]

Premises used: Finset.prod_empty, Insert.insert, Summable.of_nonneg_of_le, Finset.filter_true_of_mem, Finset.notMem_empty, Function.comp_def, Finset.filter_insert, forall_const, Nat.factoredNumbers_empty, Nat.equivProdNatFactoredNumbers_apply', norm_nonneg, IsEmpty.forall_iff
-- 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‖
s : Finset ℕ
⊢ Eq.{u_1 + 1} (α := R) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
    (∑' (m : (↑(factoredNumbers s) : Type)), f (↑m : ℕ))

Tactic:
(summable_and_hasSum_factoredNumbers_prod_filter_prime_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, Eq.symm, EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum