awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
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)
⊢ 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:
convert! h_sum.mul_left (Real.Gamma s.re) using 2 with i

Premises used: Complex.re, Summable.mul_left, Real.Gamma
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  ‖‖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)
⊢ 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:
simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc, norm_mul (a i), integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, mul_assoc, norm_mul, mul_comm
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  ‖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)
⊢ ‖‖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:
rw [← mul_div_assoc, mul_comm (Real.Gamma _), mul_div_assoc, norm_mul ‖a i‖, norm_norm]

Premises used: Norm.norm, mul_div_assoc, norm_mul, norm_norm, Real.Gamma, mul_comm
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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‖ *
        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)
h₁ :
  ∀ (hpi : 0 < p 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)
⊢ ‖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
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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‖ *
      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:
simp [hai]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
h :
  Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    Real.Gamma s.re / p i ^ s.re
⊢ ‖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:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-(p i * t))) =
    (1 / p i) ^ s.re * Real.Gamma s.re

Tactic:
have := Real.integral_rpow_mul_exp_neg_mul_Ioi hs hpi
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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.re - 1) * rexp (-(p i * t))) =
    (1 / p i) ^ s.re * Real.Gamma s.re
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re

Tactic:
simp_rw [← neg_mul (p i), one_div, inv_rpow hpi.le, ← div_eq_inv_mul] at this

Premises used: Real.inv_rpow, LT.lt.le, one_div, neg_mul, div_eq_inv_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ‖(↑x : ℂ) ^ (s - 1) * (↑(rexp (-p i * x)) : ℂ)‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t))
⊢ Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    Real.Gamma s.re / p i ^ s.re

Tactic:
rw [norm_of_nonneg (integral_nonneg (fun _ ↦ norm_nonneg _)), ← this]

Premises used: MeasureTheory.integral_nonneg, norm_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ‖(↑x : ℂ) ^ (s - 1) * (↑(rexp (-p i * x)) : ℂ)‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t))

Tactic:
setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
h :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ‖(↑x : ℂ) ^ (s - 1) * (↑(rexp (-p i * x)) : ℂ)‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖(↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₁ : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖rexp (-p i * t)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₂ : ‖(↑t : ℂ) ^ (s - 1)‖ * |rexp (-p i * t)| = t ^ (s.re - 1) * rexp (-p i * t)
h₃ : ‖(↑t : ℂ) ^ (s - 1)‖ * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
h₄ : t ^ (s - 1).re * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
h₅ : t ^ (s.re - re 1) * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
h₆ h₇ : t ^ (s.re - 1) * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
⊢ ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)

Tactic:
rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
      norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]

Premises used: Complex.sub_re, norm_mul, Complex.norm_real, Complex.one_re, Complex.norm_cpow_eq_rpow_re_of_pos, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
i : ι
inl : ∀ (h : a i = 0), a i = 0 ∨ 0 < π * q i
inr : ∀ (h : 0 < q i), a i = 0 ∨ 0 < π * q i
⊢ a i = 0 ∨ 0 < π * q i

Tactic:
rcases hq i with h | h
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
i : ι
h : a i = 0
⊢ a i = 0 ∨ 0 < π * q i

Tactic:
simp [h, pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
i : ι
h : 0 < q i
⊢ a i = 0 ∨ 0 < π * q i

Tactic:
simp [h, pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
⊢ ∀ (i : ι), a i = 0 ∨ 0 < π * q i

Tactic:
have hp i : a i = 0 ∨ 0 < π * q i := by rcases hq i with h | h <;> simp [h, pi_pos]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-(π * q i) * t)) : ℂ)) (F t)

Tactic:
simpa using hF
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
h : ∀ (i : ι), (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s = Complex.Gamma s * a i / (↑(π * q i) : ℂ) ^ s
convert! : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / (π * q i) ^ s.re
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s) (mellin F s)

Tactic:
convert! hasSum_mellin hp hs (by simpa using hF) ?_ using 2 with i

Premises used: hasSum_mellin
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
inl : ∀ (h : a i = 0), a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr : ∀ (h : 0 < q i), a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
⊢ a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s

Tactic:
rcases hq i with h | h
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
inr : a i / ((↑π : ℂ) * (↑(q i) : ℂ)) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr₁ : a i / ((↑π : ℂ) ^ s * (↑(q i) : ℂ) ^ s) = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr₂ : a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr₃ : a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s = ((↑π : ℂ) ^ s)⁻¹ * a i / (↑(q i) : ℂ) ^ s
inr₄ inr₅ : a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s = a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s
⊢ a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s

Tactic:
rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg,
          ← div_eq_inv_mul]

Premises used: Complex.cpow_neg, Real.pi_pos, LT.lt.le, Complex.mul_cpow_ofReal_nonneg, div_div, div_eq_inv_mul, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
⊢ a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s

Tactic:
have : a i / ↑(π * q i) ^ s = π ^ (-s) * a i / q i ^ s := by
      rcases hq i with h | h
      · simp [h]
      · rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg,
          ← div_eq_inv_mul]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
this : a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
h :
  (↑π : ℂ) ^ (-s) * Complex.Gamma s * (a i / (↑(q i) : ℂ) ^ s) =
    Complex.Gamma s * ((↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s)
⊢ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s = Complex.Gamma s * a i / (↑(π * q i) : ℂ) ^ s

Tactic:
simp_rw [mul_div_assoc, this]

Premises used: mul_div_assoc
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
this : a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
⊢ (↑π : ℂ) ^ (-s) * Complex.Gamma s * (a i / (↑(q i) : ℂ) ^ s) =
    Complex.Gamma s * ((↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
inl : ∀ (h : a i = 0), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
inr : ∀ (h : 0 < q i), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
rcases hq i with h | h
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
inr : ‖a i‖ / (π ^ s.re * q i ^ s.re) = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
inr₁ : ‖a i‖ / π ^ s.re / q i ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
inr₂ : ‖a i‖ / π ^ s.re / q i ^ s.re = (π ^ s.re)⁻¹ * ‖a i‖ / q i ^ s.re
inr₃ inr₄ : ‖a i‖ / π ^ s.re / q i ^ s.re = ‖a i‖ / π ^ s.re / q i ^ s.re
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]

Premises used: Real.mul_rpow, Real.pi_pos, LT.lt.le, div_div, div_eq_inv_mul, Real.rpow_neg
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ ∀ (i : ι), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
have (i : _) : ‖a i‖ / ↑(π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re := by
      rcases hq i with h | h
      · simp [h]
      · rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
this : ∀ (i : ι), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / (π * q i) ^ s.re

Tactic:
simpa only [this, mul_div_assoc] using h_sum.mul_left _

Premises used: mul_div_assoc, Summable.mul_left
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
⊢ s ≠ 0

Tactic:
have hs' : s ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs)
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : (i : ι) → ℂ := fun (i : ι) ↦ if p i = 0 then 0 else a i
i : ι
simp : (if p i = 0 then 0 else a i) = 0 ∨ 0 < p i
⊢ a' i = 0 ∨ 0 < p i

Tactic:
simp only [a']