-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- We relate a finite product over primes in `s` to an infinite sum over `s`-factored numbers. -/
lemma summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum
    (hsum : ∀ {p : ℕ}, p.Prime → Summable (fun n : ℕ ↦ ‖f (p ^ n)‖)) (s : Finset ℕ) :
    Summable (fun m : factoredNumbers s ↦ ‖f m‖) ∧
      HasSum (fun m : factoredNumbers s ↦ f m)
        (∏ p ∈ s with p.Prime, ∑' n : ℕ, f (p ^ n))

Proof state:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
⊢ HasSum (fun x => f ↑((equivProdNatFactoredNumbers hpp hp) x))
    ((∑' (n : ℕ), f (p ^ n)) * ∏ x ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (x ^ n))

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

Result:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
⊢ HasSum (fun x => f (p ^ x.1) * f ↑x.2)
    ((∑' (n : ℕ), f (p ^ n)) * ∏ x ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (x ^ n))

Proof state:
case pos
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ (Summable fun m => ‖f ↑m‖) ∧
    HasSum (fun m => f ↑m) (∏ x ∈ insert p (filter (fun p => Nat.Prime p) s), ∑' (n : ℕ), f (x ^ n))

Tactic:
constructor

Result:
case pos.left
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable fun m => ‖f ↑m‖

case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ HasSum (fun m => f ↑m) (∏ x ∈ insert p (filter (fun p => Nat.Prime p) s), ∑' (n : ℕ), f (x ^ n))

Proof state:
case insert
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
⊢ (Summable fun m => ‖f ↑m‖) ∧
    HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) (insert p s), ∑' (n : ℕ), f (p ^ n))

Tactic:
rw [filter_insert]

Result:
case insert
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
⊢ (Summable fun m => ‖f ↑m‖) ∧
    HasSum (fun m => f ↑m)
      (∏ p ∈ if Nat.Prime p then insert p (filter (fun p => Nat.Prime p) s) else filter (fun p => Nat.Prime p) s,
        ∑' (n : ℕ), f (p ^ n))

Proof state:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
⊢ HasSum (fun m => f ↑m) (∏ x ∈ insert p (filter (fun p => Nat.Prime p) s), ∑' (n : ℕ), f (x ^ n))

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

Result:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
⊢ HasSum (fun x => f ↑((equivProdNatFactoredNumbers hpp hp) x))
    ((∑' (n : ℕ), f (p ^ n)) * ∏ x ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (x ^ n))

Proof state:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ HasSum (fun m => f ↑m) (∏ x ∈ insert p (filter (fun p => Nat.Prime p) s), ∑' (n : ℕ), f (x ^ n))

Tactic:
have hp' : p ∉ {p ∈ s | p.Prime} := mt (mem_of_mem_filter p) hp

Result:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : 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 => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ filter (fun p => Nat.Prime p) s
⊢ HasSum (fun m => f ↑m) (∏ x ∈ insert p (filter (fun p => Nat.Prime p) s), ∑' (n : ℕ), f (x ^ n))