awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun (x : ℕ) ↦ (↑(f x) : ℂ)) < (↑x : EReal)
aux :
  term (fun (x : ℕ) ↦ (↑(f x) : ℂ)) (↑x : ℂ) = fun (n : ℕ) ↦
    (↑(if n = 0 then 0 else f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
this : Summable (α := ℝ) fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x
h₁ :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x_1 : ℕ |
        Membership.mem (γ := Set ℕ) {0}ᶜ x_1 →
          Membership.mem (γ := Set ℕ)
            {x_2 : ℕ |
              (fun (x_3 : ℕ) ↦
                  Eq (α := ℝ) ((fun (x_4 : ℕ) ↦ if x_4 = 0 then 0 else f x_4 / HPow.hPow (α := ℝ) (↑x_4 : ℝ) x) x_3)
                    ((fun (n : ℕ) ↦ f n / HPow.hPow (α := ℝ) (↑n : ℝ) x) x_3))
                x_2}
            x_1}
      a
⊢ Filter.EventuallyEq (β := ℝ) Filter.cofinite
    (fun (x_1 : ℕ) ↦ if x_1 = 0 then 0 else f x_1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) x) fun (n : ℕ) ↦
    f n / HPow.hPow (α := ℝ) (↑n : ℝ) x
have h₂ : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ) {0}ᶜ a →
    (if a = 0 then 0 else f a / HPow.hPow (α := ℝ) (↑a : ℝ) x) = f a / HPow.hPow (α := ℝ) (↑a : ℝ) x
Tactic: filter_upwards [(Set.finite_singleton 0).compl_mem_cofinite] with n hn
    using if_neg (by simpa using hn)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
Goal:
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
⊢ abscissaOfAbsConv (F f g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)
have refine_1 : ∀ (x : ℝ) (hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < (↑x : EReal)), LSeriesSummable f (↑x : ℂ)
Tactic: refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun x hx ↦ hF ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convergence (goal)
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 : ℂ)
⊢ abscissaOfAbsConv (F f g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)
have refine_2 : ∀ (x : ℝ) (hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < (↑x : EReal)), LSeriesSummable g (↑x : ℂ)
Tactic: refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun x hx ↦ hF ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
R : Type u_1
inst : Zero R
f f' : ℕ → R
h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
⊢ Eq (α := ArithmeticFunction R) (toArithmeticFunction f) (toArithmeticFunction f')
have h₁ : ∀ (x : ℕ), Eq (α := R) ((toArithmeticFunction f : (a : ℕ) → R) x : R) ((toArithmeticFunction f' : (a : ℕ) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
R : Type u_1
inst : Zero R
f : ArithmeticFunction R
⊢ toArithmeticFunction (⇑f : (a : ℕ) → R) = f
have h : ∀ (n : ℕ), Eq (α := R) ((toArithmeticFunction (⇑f : (a : ℕ) → R) : (a : ℕ) → R) n : R) ((f : (a : ℕ) → R) n : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
R : Type u_1
inst : Semiring R
f g : ℕ → R
⊢ f ⍟ g = fun (n : ℕ) ↦ ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2
have h : ∀ (n : ℕ), (f ⍟ g) n = ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2
have inl : term (f ⍟ g) s 0 = ∑ p ∈ divisorsAntidiagonal 0, term f s p.1 * term g s p.2
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
inl : term (f ⍟ g) s 0 = ∑ p ∈ divisorsAntidiagonal 0, 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
have inr : ∀ (hn : n ≠ 0), 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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2
have 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)
Tactic: rw [term_of_ne_zero hn, convolution_def, Finset.sum_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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)
have 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
Tactic: refine Finset.sum_congr rfl fun p hp ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (hypothesis)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
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
have hp₁ : p.1 ≠ 0
Tactic: have ⟨hp₁, hp₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (hypothesis)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have hp₂ : p.2 ≠ 0
Tactic: have ⟨hp₁, hp₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have inr : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 / HPow.hPow (α := ℂ) (↑p.1 : ℂ) s * 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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)
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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)
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have 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))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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))
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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)
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have inr₅ : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 * g p.2 / HMul.hMul (α := ℂ) (↑p.2 : ℂ) (↑p.1 : ℂ) ^ s
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have inr₆ : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑(p.2 * p.1) : ℂ) s
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have inr₇ : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑(p.1 * p.2) : ℂ) s
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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
⊢ f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = term f s p.1 * term g s p.2
have inr₈ : f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s = f p.1 * g p.2 / HPow.hPow (α := ℂ) (↑n : ℂ) s
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
⊢ 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
have 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
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
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
have 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
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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
⊢ 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
have 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
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
⊢ preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0} =
    SProd.sprod (α := Set ℕ) (β := Set ℕ) {0} univ ∪ SProd.sprod (α := Set ℕ) (β := Set ℕ) univ {0}
have 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}
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (hypothesis)
Goal:
f g : ℕ → ℂ
s : ℂ
⊢ Eq (α := ℂ) 0
    (∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) : Type)),
      term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2)
have hS : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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)
⊢ 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
have 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
Tactic: rcases hS ▸ hp with ⟨rfl, -⟩ | ⟨-, rfl⟩
Cleared hypotheses: fst, hp
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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
⊢ 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
have 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
Tactic: rcases hS ▸ hp with ⟨rfl, -⟩ | ⟨-, rfl⟩
Cleared hypotheses: snd, hp
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (hypothesis)
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}
⊢ Eq (α := ℂ) 0
    (∑' (b : (↑(preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {0}) : Type)),
      term f s (↑b : ℕ × ℕ).1 * term g s (↑b : ℕ × ℕ).2)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n} = (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))
have h : ∀ (x : ℕ × ℕ),
  Membership.mem (γ := Set (ℕ × ℕ)) (preimage (β := ℕ) (fun (p : ℕ × ℕ) ↦ p.1 * p.2) {n}) x ↔
    x ∈ (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
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
have h : term (f ⍟ g) s n =
  ∑' (b : (↑(↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Convolution (goal)
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
⊢ 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
have h₁ : term (f ⍟ g) s n = ∑ x ∈ n.divisorsAntidiagonal, term f s x.1 * term g s x.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]