awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
refine_1 : ∀ (x : ℝ) (hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < (↑x : EReal)), LSeriesSummable f (↑x : ℂ)
refine_2 : ∀ (x : ℝ) (hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < (↑x : EReal)), LSeriesSummable g (↑x : ℂ)
⊢ abscissaOfAbsConv (F f g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

Tactic:
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun x hx ↦ hF ?_ ?_

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < (↑x : EReal)
⊢ LSeriesSummable f (↑x : ℂ)

Tactic:
LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ (le_max_left ..).trans_lt hx

Premises used: Eq.rec, LSeriesSummable_of_abscissaOfAbsConv_lt_re, Complex.ofReal_re, Eq.symm, le_max_left, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < (↑x : EReal)
⊢ LSeriesSummable f (↑x : ℂ)

Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ (le_max_left ..).trans_lt hx

Premises used: LSeriesSummable_of_abscissaOfAbsConv_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < (↑x : EReal)
⊢ LSeriesSummable g (↑x : ℂ)

Tactic:
LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ (le_max_right ..).trans_lt hx

Premises used: le_max_right, Eq.rec, LSeriesSummable_of_abscissaOfAbsConv_lt_re, Complex.ofReal_re, Eq.symm, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.LSeries.Convergence
Goal:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < (↑x : EReal)
⊢ LSeriesSummable g (↑x : ℂ)

Tactic:
exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ (le_max_right ..).trans_lt hx

Premises used: LSeriesSummable_of_abscissaOfAbsConv_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Zero R
f f' : ℕ → R
h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
h₁ :
  ∀ (x : ℕ), Eq (α := R) ((toArithmeticFunction f : (a : ℕ) → R) x : R) ((toArithmeticFunction f' : (a : ℕ) → R) x : R)
⊢ Eq (α := ArithmeticFunction R) (toArithmeticFunction f) (toArithmeticFunction f')

Tactic:
ext
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Zero R
f f' : ℕ → R
h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
x : ℕ
⊢ Eq (α := R) ((toArithmeticFunction f : (a : ℕ) → R) x : R) ((toArithmeticFunction f' : (a : ℕ) → R) x : R)

Tactic:
simp_all [toArithmeticFunction]

Premises used: toArithmeticFunction
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Zero R
f : ArithmeticFunction R
h : ∀ (n : ℕ), Eq (α := R) ((toArithmeticFunction (⇑f : (a : ℕ) → R) : (a : ℕ) → R) n : R) ((f : (a : ℕ) → R) n : R)
⊢ toArithmeticFunction (⇑f : (a : ℕ) → R) = f

Tactic:
ext n
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Zero R
f : ArithmeticFunction R
n : ℕ
⊢ Eq (α := R) ((toArithmeticFunction (⇑f : (a : ℕ) → R) : (a : ℕ) → R) n : R) ((f : (a : ℕ) → R) n : R)

Tactic:
simp +contextual [toArithmeticFunction]

Premises used: toArithmeticFunction
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Semiring R
f f' g g' : ℕ → R
hf : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
hg : ∀ {n : ℕ}, n ≠ 0 → g n = g' n
⊢ f ⍟ g = f' ⍟ g'

Tactic:
simp [convolution, toArithmeticFunction_congr hf, toArithmeticFunction_congr hg]

Premises used: LSeries.convolution, toArithmeticFunction_congr
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Semiring R
f g : ArithmeticFunction R
⊢ Eq (α := ℕ → R) ((⇑f : (a : ℕ) → R) ⍟ (⇑g : (a : ℕ) → R)) (⇑(f * g) : (a : ℕ) → R)

Tactic:
simp [convolution]

Premises used: LSeries.convolution
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Semiring R
f g : ℕ → R
h : ∀ (n : ℕ), (f ⍟ g) n = ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2
⊢ f ⍟ g = fun (n : ℕ) ↦ ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2

Tactic:
ext n
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Semiring R
f g : ℕ → R
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ (if p.2 = 0 then 0 else if p.1 = 0 then 0 else f p.1 * g p.2) = f p.1 * g p.2

Tactic:
simp [ne_zero_of_mem_divisorsAntidiagonal hp]

Premises used: Nat.ne_zero_of_mem_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Semiring R
f g : ℕ → R
n : ℕ
⊢ (f ⍟ g) n = ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2

Tactic:
simpa [convolution, toArithmeticFunction] using
    Finset.sum_congr rfl fun p hp ↦ by simp [ne_zero_of_mem_divisorsAntidiagonal hp]

Premises used: toArithmeticFunction, LSeries.convolution, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
R : Type u_1
inst : Semiring R
f g : ℕ → R
⊢ (f ⍟ g) 0 = 0

Tactic:
simp [convolution_def]

Premises used: LSeries.convolution_def
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
inl : term (f ⍟ g) s 0 = ∑ p ∈ divisorsAntidiagonal 0, term f s p.1 * term g s p.2
inr : ∀ (hn : n ≠ 0), term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s 0 = ∑ p ∈ divisorsAntidiagonal 0, term f s p.1 * term g s p.2

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
inr :
  Eq (α := ℂ) (∑ i ∈ n.divisorsAntidiagonal, f i.1 * g i.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2)
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Tactic:
rw [term_of_ne_zero hn, convolution_def, Finset.sum_div]

Premises used: LSeries.convolution_def, LSeries.term_of_ne_zero, Finset.sum_div
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℂ) (∑ i ∈ n.divisorsAntidiagonal, f i.1 * g i.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2)

Tactic:
Finset.sum_congr rfl fun p hp ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
inr :
  ∀ (p : ℕ × ℕ) (hp : p ∈ n.divisorsAntidiagonal),
    f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
⊢ Eq (α := ℂ) (∑ i ∈ n.divisorsAntidiagonal, f i.1 * g i.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s)
    (∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2)

Tactic:
refine Finset.sum_congr rfl fun p hp ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ p.1 ≠ 0

Tactic:
have ⟨hp₁, hp₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
⊢ p.2 ≠ 0

Tactic:
have ⟨hp₁, hp₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
inr : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 / HPow.hPow (α := ℂ) (↑p.1 : ℂ) s * term g s p.2
inr₁ :
  f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    f p.1 / HPow.hPow (α := ℂ) (↑p.1 : ℂ) s * (g p.2 / HPow.hPow (α := ℂ) (↑p.2 : ℂ) s)
inr₂ :
  f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    f p.1 * (g p.2 / HPow.hPow (α := ℂ) (↑p.2 : ℂ) s / HPow.hPow (α := ℂ) (↑p.1 : ℂ) s)
inr₃ :
  f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    f p.1 * (g p.2 / (HPow.hPow (α := ℂ) (↑p.2 : ℂ) s * HPow.hPow (α := ℂ) (↑p.1 : ℂ) s))
inr₄ :
  f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s =
    f p.1 * g p.2 / (HPow.hPow (α := ℂ) (↑p.2 : ℂ) s * HPow.hPow (α := ℂ) (↑p.1 : ℂ) s)
inr₅ : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 * g p.2 / HMul.hMul (α := ℂ) (↑p.2 : ℂ) (↑p.1 : ℂ) ^ s
inr₆ : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑(p.2 * p.1) : ℂ) s
inr₇ : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑(p.1 * p.2) : ℂ) s
inr₈ inr₉ : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2

Tactic:
rw [term_of_ne_zero hp₁, term_of_ne_zero hp₂, mul_comm_div, div_div, ← mul_div_assoc,
    ← natCast_mul_natCast_cpow, ← cast_mul, mul_comm p.2, (mem_divisorsAntidiagonal.mp hp).1]

Premises used: Complex.natCast_mul_natCast_cpow, mul_div_assoc, Nat.mem_divisorsAntidiagonal, LSeries.term_of_ne_zero, Nat.cast_mul, And.left, mul_comm_div, Iff.mp, mul_comm, div_div, Prod.snd
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
h :
  ∀ (n : ℕ),
    term (f ⍟ g) s n =
      ∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n}) : Type)),
        term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2
⊢ term (f ⍟ g) s = fun (n : ℕ) ↦
    ∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n}) : Type)),
      term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2

Tactic:
ext n
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h :
  term (f ⍟ g) s 0 =
    ∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) : Type)),
      term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2
h₁ :
  ∀ (hn : n ≠ 0),
    term (f ⍟ g) s n =
      ∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n}) : Type)),
        term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2
⊢ term (f ⍟ g) s n =
    ∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n}) : Type)),
      term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s 0 =
    ∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) : Type)),
      term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2

Tactic:
(term_zero ..).trans ?_

Premises used: Eq.trans, LSeries.term_zero
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
h :
  ∀ (x : ℕ × ℕ),
    Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x ↔
      x ∈ SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}
⊢ preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0} =
    SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}

Tactic:
ext
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
x : ℕ × ℕ
⊢ Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x ↔
    x ∈ SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
⊢ preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0} =
    SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}

Tactic:
have hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0} := by
      ext
      simp
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
hS :
  preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0} =
    SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}
fst snd : ℕ
hp : Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) (fst, snd)
inl :
  ∀ (hp : Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) (0, snd)),
    term f s
          (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                  Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (0, snd)
                  hp) :
              ℕ × ℕ).1 *
        term g s
          (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                  Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (0, snd)
                  hp) :
              ℕ × ℕ).2 =
      0
inr :
  ∀ (hp : Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) (fst, 0)),
    term f s
          (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                  Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (fst, 0)
                  hp) :
              ℕ × ℕ).1 *
        term g s
          (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                  Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (fst, 0)
                  hp) :
              ℕ × ℕ).2 =
      0
⊢ term f s
        (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (fst, snd)
                hp) :
            ℕ × ℕ).1 *
      term g s
        (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (fst, snd)
                hp) :
            ℕ × ℕ).2 =
    0

Tactic:
rcases hS ▸ hp with ⟨rfl, -⟩ | ⟨-, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
hS :
  preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0} =
    SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}
snd : ℕ
hp : Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) (0, snd)
⊢ term f s
        (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (0, snd)
                hp) :
            ℕ × ℕ).1 *
      term g s
        (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (0, snd)
                hp) :
            ℕ × ℕ).2 =
    0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
hS :
  preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0} =
    SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}
fst : ℕ
hp : Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) (fst, 0)
⊢ term f s
        (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (fst, 0)
                hp) :
            ℕ × ℕ).1 *
      term g s
        (↑(Subtype.mk (p := fun (x : ℕ × ℕ) ↦
                Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) x) (fst, 0)
                hp) :
            ℕ × ℕ).2 =
    0

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
hS :
  preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0} =
    SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}
⊢ ∀ (p : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) : Type)),
    term f s (↑p : ℕ × ℕ).1 * term g s (↑p : ℕ × ℕ).2 = 0

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
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
hS :
  preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0} =
    SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}
this :
  ∀ (p : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) : Type)),
    term f s (↑p : ℕ × ℕ).1 * term g s (↑p : ℕ × ℕ).2 = 0
⊢ Eq (α := ℂ) 0
    (∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) : Type)),
      term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2)

Tactic:
simp [this]
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
h :
  ∀ (x : ℕ × ℕ),
    Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n}) x ↔
      x ∈ (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))
⊢ preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n} = (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))

Tactic:
ext
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ × ℕ
⊢ Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n}) x ↔
    x ∈ (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
h :
  term (f ⍟ g) s n =
    ∑' (b : (↑(↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) : Type)), term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2
h₁ : term (f ⍟ g) s n = ∑ x ∈ n.divisorsAntidiagonal, term f s x.1 * term g s x.2
h₂ h₃ :
  Eq (α := ℂ) (∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2)
    (∑ x ∈ n.divisorsAntidiagonal, term f s x.1 * term g s x.2)
⊢ term (f ⍟ g) s n =
    ∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n}) : Type)),
      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]

Premises used: HMul.hMul, Nat.divisorsAntidiagonal, LSeries.term_convolution, Prod.fst, LSeries.term, Prod.snd, Finset.tsum_subtype'
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ Summable (α := ℂ) fun (x : ℕ × ℕ) ↦ term f s x.1 * term g s x.2

Tactic:
have hsum := summable_mul_of_summable_norm hf.summable.norm hg.summable.norm
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
hsum : Summable (α := ℂ) fun (x : ℕ × ℕ) ↦ term f s x.1 * term g s x.2
⊢ LSeriesHasSum (f ⍟ g) s (a * b)

Tactic:
simpa only [LSeriesHasSum, term_convolution'] using (hf.mul hg hsum).tsum_fiberwise _

Premises used: LSeries.term_convolution', LSeriesHasSum, HasSum.mul, HasSum.tsum_fiberwise
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ L (f ⍟ g) s = L f s * L g s

Tactic:
(LSeriesHasSum.convolution hf.LSeriesHasSum hg.LSeriesHasSum).LSeries_eq

Premises used: LSeriesHasSum.convolution, LSeriesSummable.LSeriesHasSum, LSeriesHasSum.LSeries_eq
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
hf : abscissaOfAbsConv f < (↑s.re : EReal)
hg : abscissaOfAbsConv g < (↑s.re : EReal)
⊢ L (f ⍟ g) s = L f s * L g s

Tactic:
LSeries_convolution' (LSeriesSummable_of_abscissaOfAbsConv_lt_re hf)
    (LSeriesSummable_of_abscissaOfAbsConv_lt_re hg)

Premises used: LSeries_convolution', LSeriesSummable_of_abscissaOfAbsConv_lt_re
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeriesSummable (f ⍟ g) s

Tactic:
(LSeriesHasSum.convolution hf.LSeriesHasSum hg.LSeriesHasSum).LSeriesSummable

Premises used: LSeriesHasSum.convolution, LSeriesSummable.LSeriesHasSum, LSeriesHasSum.LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ℕ → ℂ
⊢ abscissaOfAbsConv (f ⍟ g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

Tactic:
abscissaOfAbsConv_binop_le LSeriesSummable.convolution f g

Premises used: LSeries.abscissaOfAbsConv_binop_le, LSeriesSummable.convolution
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ArithmeticFunction ℂ
s a b : ℂ
hf : LSeriesHasSum (fun (n : ℕ) ↦ (f : (a : ℕ) → ℂ) n) s a
hg : LSeriesHasSum (fun (n : ℕ) ↦ (g : (a : ℕ) → ℂ) n) s b
⊢ LSeriesHasSum (fun (n : ℕ) ↦ (f * g : (a : ℕ) → ℂ) n) s (a * b)

Tactic:
coe_mul f g ▸ hf.convolution hg

Premises used: LSeriesHasSum.convolution, ArithmeticFunction.coe_mul, Eq.rec
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ArithmeticFunction ℂ
s : ℂ
hf : LSeriesSummable (fun (n : ℕ) ↦ (f : (a : ℕ) → ℂ) n) s
hg : LSeriesSummable (fun (n : ℕ) ↦ (g : (a : ℕ) → ℂ) n) s
⊢ L (fun (n : ℕ) ↦ (f * g : (a : ℕ) → ℂ) n) s =
    L (fun (n : ℕ) ↦ (f : (a : ℕ) → ℂ) n) s * L (fun (n : ℕ) ↦ (g : (a : ℕ) → ℂ) n) s

Tactic:
coe_mul f g ▸ LSeries_convolution' hf hg

Premises used: ArithmeticFunction.coe_mul, Eq.rec, LSeries_convolution'
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ArithmeticFunction ℂ
s : ℂ
hf : (abscissaOfAbsConv fun (n : ℕ) ↦ (f : (a : ℕ) → ℂ) n) < (↑s.re : EReal)
hg : (abscissaOfAbsConv fun (n : ℕ) ↦ (g : (a : ℕ) → ℂ) n) < (↑s.re : EReal)
⊢ L (fun (n : ℕ) ↦ (f * g : (a : ℕ) → ℂ) n) s =
    L (fun (n : ℕ) ↦ (f : (a : ℕ) → ℂ) n) s * L (fun (n : ℕ) ↦ (g : (a : ℕ) → ℂ) n) s

Tactic:
coe_mul f g ▸ LSeries_convolution hf hg

Premises used: ArithmeticFunction.coe_mul, Eq.rec, LSeries_convolution
-- Module: Mathlib.NumberTheory.LSeries.Convolution
Goal:
f g : ArithmeticFunction ℂ
s : ℂ
hf : LSeriesSummable (fun (n : ℕ) ↦ (f : (a : ℕ) → ℂ) n) s
hg : LSeriesSummable (fun (n : ℕ) ↦ (g : (a : ℕ) → ℂ) n) s
⊢ LSeriesSummable (fun (n : ℕ) ↦ (f * g : (a : ℕ) → ℂ) n) s

Tactic:
coe_mul f g ▸ hf.convolution hg

Premises used: ArithmeticFunction.coe_mul, Eq.rec, LSeriesSummable.convolution
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
n : ℕ
s : ℂ
inl : HasDerivAt (fun (z : ℂ) ↦ term f z 0) (-term (logMul f) s 0) s
inr : ∀ (hn : n ≠ 0), HasDerivAt (fun (z : ℂ) ↦ term f z n) (-term (logMul f) s n) s
⊢ HasDerivAt (fun (z : ℂ) ↦ term f z n) (-term (logMul f) s n) s

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
s : ℂ
⊢ HasDerivAt (fun (z : ℂ) ↦ term f z 0) (-term (logMul f) s 0) s

Tactic:
simp [hasDerivAt_const]

Premises used: hasDerivAt_const
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
inr :
  HasDerivAt (fun (z : ℂ) ↦ f n * HPow.hPow (α := ℂ) (↑n : ℂ) (-z))
    (f n * (-log (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-s))) s
⊢ HasDerivAt (fun (z : ℂ) ↦ term f z n) (-term (logMul f) s n) s

Tactic:
simp_rw [term_of_ne_zero hn, ← neg_div, ← neg_mul, mul_comm, mul_div_assoc, div_eq_mul_inv,
    ← cpow_neg]

Premises used: neg_div, mul_div_assoc, LSeries.term_of_ne_zero, Complex.cpow_neg, div_eq_mul_inv, mul_comm, neg_mul
-- Module: Mathlib.NumberTheory.LSeries.Deriv
Goal:
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (↑n : ℂ) (-z)) (-log (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) (-s)) s

Tactic:
simpa only [mul_comm, ← mul_neg_one (log n), ← mul_assoc]
    using (hasDerivAt_neg' s).const_cpow (Or.inl <| Nat.cast_ne_zero.mpr hn)

Premises used: Iff.mpr, Complex.log, hasDerivAt_neg', mul_assoc, Nat.cast, mul_comm, Or.inl, mul_neg_one, HasDerivAt.const_cpow, Nat.cast_ne_zero