awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have h : ∀ (hai : a i = 0),
  a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
Tactic: rcases hp i with hai | hpi
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
h :
  ∀ (hai : a i = 0),
    a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
      a i *
        @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have h₁ : ∀ (hpi : 0 < p i),
  a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
Tactic: rcases hp i with hai | hpi
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hai : a i = 0
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have h : 0 * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
  HMul.hMul (α := ℂ) 0
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ))
Tactic: rw [hai, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hai : a i = 0
h :
  0 * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    HMul.hMul (α := ℂ) 0
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ))
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have h₁ : 0 =
  HMul.hMul (α := ℂ) 0
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ))
Tactic: rw [hai, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hai : a i = 0
h :
  0 * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    HMul.hMul (α := ℂ) 0
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ))
h₁ :
  0 =
    HMul.hMul (α := ℂ) 0
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ))
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have h₂ : Eq (α := ℂ) 0 0
Tactic: rw [hai, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have this : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (s - 1) * cexp (-((↑(p i) : ℂ) * (↑t : ℂ)))) =
  (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s
Tactic: have := integral_cpow_mul_exp_neg_mul_Ioi hs hpi
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * cexp (-((↑(p i) : ℂ) * (↑t : ℂ)))) =
    (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have this₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)) =
  (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s
Tactic: simp_rw [← ofReal_mul, ← ofReal_neg, ← ofReal_exp, ← neg_mul (p i)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)) =
    (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have h : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * ((1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s)
Tactic: rw [this, one_div, inv_cpow _ _ (arg_ofReal_of_nonneg hpi.le ▸ pi_pos.ne), div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)) =
    (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s
h : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * ((1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s)
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have h₁ : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * ((↑(p i) : ℂ)⁻¹ ^ s * Complex.Gamma s)
Tactic: rw [this, one_div, inv_cpow _ _ (arg_ofReal_of_nonneg hpi.le ▸ pi_pos.ne), div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)) =
    (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s
h : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * ((1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s)
h₁ : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * ((↑(p i) : ℂ)⁻¹ ^ s * Complex.Gamma s)
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have h₂ : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * (((↑(p i) : ℂ) ^ s)⁻¹ * Complex.Gamma s)
Tactic: rw [this, one_div, inv_cpow _ _ (arg_ofReal_of_nonneg hpi.le ▸ pi_pos.ne), div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)) =
    (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s
h : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * ((1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s)
h₁ : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * ((↑(p i) : ℂ)⁻¹ ^ s * Complex.Gamma s)
h₂ : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * (((↑(p i) : ℂ) ^ s)⁻¹ * Complex.Gamma s)
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
have h₃ : a i * (((↑(p i) : ℂ) ^ s)⁻¹ * Complex.Gamma s) = a i * (((↑(p i) : ℂ) ^ s)⁻¹ * Complex.Gamma s)
Tactic: rw [this, one_div, inv_cpow _ _ (arg_ofReal_of_nonneg hpi.le ▸ pi_pos.ne), div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ @Integrable ℂ _ _ ℝ Real.measurableSpace
    ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i) (Measure.restrict volume (Ioi 0))
have convert_3 : ∀ (hai : a i = 0),
  @Integrable ℂ _ _ ℝ Real.measurableSpace
    ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i) (Measure.restrict volume (Ioi 0))
Tactic: rcases hp i with hai | hpi
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
convert_3 :
  ∀ (hai : a i = 0),
    @Integrable ℂ _ _ ℝ Real.measurableSpace
      ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i)
      (Measure.restrict volume (Ioi 0))
⊢ @Integrable ℂ _ _ ℝ Real.measurableSpace
    ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i) (Measure.restrict volume (Ioi 0))
have convert_3₁ : ∀ (hpi : 0 < p i),
  @Integrable ℂ _ _ ℝ Real.measurableSpace
    ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i) (Measure.restrict volume (Ioi 0))
Tactic: rcases hp i with hai | hpi
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
⊢ @Integrable ℂ _ _ ℝ Real.measurableSpace
    ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i) (Measure.restrict volume (Ioi 0))
have convert_3 : @Integrable ℂ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ a i * ((↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)))
  (Measure.restrict volume (Ioi 0))
Tactic: simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ a i * ((↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)))
    (Measure.restrict volume (Ioi 0))
have this : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
  (Ioi 0) volume
Tactic: have := Complex.GammaIntegral_convergent hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (Ioi 0) volume
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ a i * ((↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)))
    (Measure.restrict volume (Ioi 0))
have this₁ : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
Tactic: rw [← mul_zero (p i), ← integrableOn_Ioi_comp_mul_left_iff _ _ hpi] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ a i * ((↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)))
    (Measure.restrict volume (Ioi 0))
have convert_3 : ∀ (t : ℝ) (ht : 0 < t),
  1 / (↑(p i) : ℂ) ^ (s - 1) * ((↑(rexp (-(p i * t))) : ℂ) * (↑(p i * t) : ℂ) ^ (s - 1)) =
    (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)
Tactic: refine (IntegrableOn.congr_fun (this.const_mul (1 / p i ^ (s - 1)))
      (fun t (ht : 0 < t) ↦ ?_) measurableSet_Ioi).const_mul _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ 1 / (↑(p i) : ℂ) ^ (s - 1) * ((↑(rexp (-(p i * t))) : ℂ) * (↑(p i * t) : ℂ) ^ (s - 1)) =
    (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)
have convert_3 : 1 / (↑(p i) : ℂ) ^ (s - 1) * ((↑(p i) : ℂ) * (↑t : ℂ)) ^ (s - 1) * (↑(rexp (-(p i * t))) : ℂ) =
  (↑t : ℂ) ^ (s - 1) * (↑(rexp (-(p i * t))) : ℂ)
Tactic: simp_rw [mul_comm (↑(rexp _) : ℂ), ← mul_assoc, neg_mul, ofReal_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ 1 / (↑(p i) : ℂ) ^ (s - 1) * ((↑(p i) : ℂ) * (↑t : ℂ)) ^ (s - 1) * (↑(rexp (-(p i * t))) : ℂ) =
    (↑t : ℂ) ^ (s - 1) * (↑(rexp (-(p i * t))) : ℂ)
have convert_3 : (↑(p i) : ℂ) ^ (s - 1) ≠ 0
Tactic: rw [mul_cpow_ofReal_nonneg hpi.le ht.le, ← mul_assoc, one_div, inv_mul_cancel₀, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ (↑(p i) : ℂ) ^ (s - 1) ≠ 0
have convert_3 : ¬(↑(p i) : ℂ) = 0 ∨ ¬s - 1 ≠ 0
Tactic: rw [Ne, cpow_eq_zero_iff, not_and_or]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
⊢ Summable (α := ℝ) fun (i : ι) ↦
    @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      Norm.norm (E := ℂ) ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i a_1)
have convert_4 : Summable (α := ℝ) fun (a_1 : ι) ↦
  Norm.norm (E := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_2 : ℝ) ↦
      Norm.norm (E := ℂ) ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) a_1 a_2))
Tactic: apply Summable.of_norm
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
⊢ Summable (α := ℝ) fun (a_1 : ι) ↦
    Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_2 : ℝ) ↦
        Norm.norm (E := ℂ) ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) a_1 a_2))
have h : ∀ (i : ι),
  Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        Norm.norm (E := ℂ) ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i a_1)) =
    Real.Gamma s.re * (‖a i‖ / p i ^ s.re)
Tactic: convert! h_sum.mul_left (Real.Gamma s.re) using 2 with i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        Norm.norm (E := ℂ) ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i a_1)) =
    Real.Gamma s.re * (‖a i‖ / p i ^ s.re)
have h : ‖‖a i‖ *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖‖ =
  Real.Gamma s.re * (‖a i‖ / p i ^ s.re)
Tactic: simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc, norm_mul (a i), integral_const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ ‖‖a i‖ *
        @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖‖ =
    Real.Gamma s.re * (‖a i‖ / p i ^ s.re)
have h : ‖a i‖ *
    Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
  ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)
Tactic: rw [← mul_div_assoc, mul_comm (Real.Gamma _), mul_div_assoc, norm_mul ‖a i‖, norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ ‖a i‖ *
      Norm.norm (E := ℝ)
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)
have h : ∀ (hai : a i = 0),
  ‖a i‖ *
      Norm.norm (E := ℝ)
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)
Tactic: rcases hp i with hai | hpi