-- Mathlib/NumberTheory/LSeries/Convolution.lean
/-- We give an expression of the `LSeries.term` of the convolution of two functions
in terms of an a priori infinite sum over all pairs `(k, m)` with `k * m = n`
(the set we sum over is infinite when `n = 0`). This is the version needed for the
proof that `L (f ⍟ g) = L f * L g`. -/
lemma term_convolution' (f g : ℕ → ℂ) (s : ℂ) :
    term (f ⍟ g) s = fun n ↦
      ∑' (b : (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {n}), term f s b.val.1 * term g s b.val.2

Proof state:
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s = fun n => ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2

Tactic:
ext n

Result:
case h
f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f ⍟ g) s n = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2

Proof state:
case h.inl
f g : ℕ → ℂ
s : ℂ
hS : (fun p => p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
this : ∀ (p : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑p).1 * term g s (↑p).2 = 0
⊢ 0 = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2

Tactic:
simp [this]

Result:
no goals

Proof state:
case h
f g : ℕ → ℂ
s : ℂ
x✝ : ℕ × ℕ
⊢ x✝ ∈ (fun p => p.1 * p.2) ⁻¹' {0} ↔ x✝ ∈ {0} ×ˢ univ ∪ univ ×ˢ {0}

Tactic:
simp [Nat.mul_eq_zero, -singleton_prod, -prod_singleton]

Result:
no goals

Proof state:
case mk.mk
f g : ℕ → ℂ
s : ℂ
hS : (fun p => p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
fst✝ snd✝ : ℕ
hp : (fst✝, snd✝) ∈ (fun p => p.1 * p.2) ⁻¹' {0}
⊢ term f s (↑⟨(fst✝, snd✝), hp⟩).1 * term g s (↑⟨(fst✝, snd✝), hp⟩).2 = 0

Tactic:
rcases hS ▸ hp with ⟨rfl, -⟩ | ⟨-, rfl⟩ <;> simp

Result:
no goals

Proof state:
case h
f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f ⍟ g) s n = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case h.inl
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s 0 = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2

case h.inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2

Proof state:
case h.inl
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s 0 = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2

Tactic:
refine (term_zero ..).trans ?_

Result:
case h.inl
f g : ℕ → ℂ
s : ℂ
⊢ 0 = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2

Proof state:
case h
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
x✝ : ℕ × ℕ
⊢ x✝ ∈ (fun p => p.1 * p.2) ⁻¹' {n} ↔ x✝ ∈ ↑n.divisorsAntidiagonal

Tactic:
simp [hn]

Result:
no goals

Proof state:
case h.inl
f g : ℕ → ℂ
s : ℂ
⊢ 0 = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2

Tactic:
have hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0} := by
  ext
  simp [Nat.mul_eq_zero, -singleton_prod, -prod_singleton]

Result:
case h.inl
f g : ℕ → ℂ
s : ℂ
hS : (fun p => p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
⊢ 0 = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2

Proof state:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ (fun p => p.1 * p.2) ⁻¹' {n} = ↑n.divisorsAntidiagonal

Tactic:
ext

Result:
case h
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
x✝ : ℕ × ℕ
⊢ x✝ ∈ (fun p => p.1 * p.2) ⁻¹' {n} ↔ x✝ ∈ ↑n.divisorsAntidiagonal

Proof state:
case h.inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2

Tactic:
rw [show (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {n} = n.divisorsAntidiagonal by ext; simp [hn],
  Finset.tsum_subtype' n.divisorsAntidiagonal fun p ↦ term f s p.1 * term g s p.2,
  term_convolution f g s n]

Result:
no goals

Proof state:
f g : ℕ → ℂ
s : ℂ
⊢ (fun p => p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}

Tactic:
ext

Result:
case h
f g : ℕ → ℂ
s : ℂ
x✝ : ℕ × ℕ
⊢ x✝ ∈ (fun p => p.1 * p.2) ⁻¹' {0} ↔ x✝ ∈ {0} ×ˢ univ ∪ univ ×ˢ {0}

Proof state:
case h.inl
f g : ℕ → ℂ
s : ℂ
hS : (fun p => p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
⊢ 0 = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2

Tactic:
have : ∀ p : (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {0}, term f s p.val.1 * term g s p.val.2 = 0 := by
  rintro ⟨⟨_, _⟩, hp⟩
  rcases hS ▸ hp with ⟨rfl, -⟩ | ⟨-, rfl⟩ <;> simp

Result:
case h.inl
f g : ℕ → ℂ
s : ℂ
hS : (fun p => p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
this : ∀ (p : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑p).1 * term g s (↑p).2 = 0
⊢ 0 = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2

Proof state:
f g : ℕ → ℂ
s : ℂ
hS : (fun p => p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
⊢ ∀ (p : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑p).1 * term g s (↑p).2 = 0

Tactic:
rintro ⟨⟨_, _⟩, hp⟩

Result:
case mk.mk
f g : ℕ → ℂ
s : ℂ
hS : (fun p => p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
fst✝ snd✝ : ℕ
hp : (fst✝, snd✝) ∈ (fun p => p.1 * p.2) ⁻¹' {0}
⊢ term f s (↑⟨(fst✝, snd✝), hp⟩).1 * term g s (↑⟨(fst✝, snd✝), hp⟩).2 = 0