awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum
        (fun (i : ι) ↦
          if HPow.hPow (β := ℕ) (r i) 2 = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
        (F t)
i : ι
h : HMul.hMul (α := ℝ) (↑2 : ℝ) 0 ≤ π
⊢ (↑2 : ℝ) * (↑|r i| : ℂ).arg ≤ π

Tactic:
rw [arg_ofReal_of_nonneg (abs_nonneg _)]

Premises used: Complex.arg_ofReal_of_nonneg, abs_nonneg
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum
        (fun (i : ι) ↦
          if HPow.hPow (β := ℕ) (r i) 2 = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
        (F t)
i : ι
linarith : π < HMul.hMul (α := ℝ) (↑2 : ℝ) 0 → π - HMul.hMul (α := ℝ) (↑2 : ℝ) 0 + (0 - π) = 0
⊢ HMul.hMul (α := ℝ) (↑2 : ℝ) 0 ≤ π

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum
        (fun (i : ι) ↦
          if HPow.hPow (β := ℕ) (r i) 2 = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
        (F t)
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re

Tactic:
h_sum
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum
        (fun (i : ι) ↦
          if HPow.hPow (β := ℕ) (r i) 2 = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
        (F t)
h : ∀ (i : ι), HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re = |r i| ^ s.re
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re

Tactic:
convert! h_sum using 3 with i
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum
        (fun (i : ι) ↦
          if HPow.hPow (β := ℕ) (r i) 2 = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
        (F t)
i : ι
h : HPow.hPow (β := ℕ) |r i| 2 ^ (s / 2).re = |r i| ^ s.re
h₁ : |r i| ^ ((↑2 : ℝ) * (s / 2).re) = |r i| ^ s.re
h₂ : |r i| ^ ((↑2 : ℝ) * (s.re / 2)) = |r i| ^ s.re
h₃ : |r i| ^ (2 * (s.re / 2)) = |r i| ^ s.re
h₄ h₅ : |r i| ^ s.re = |r i| ^ s.re
⊢ HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re = |r i| ^ s.re

Tactic:
rw [← sq_abs, ← rpow_natCast_mul (abs_nonneg _), div_ofNat_re, Nat.cast_ofNat,
      mul_div_cancel₀ _ two_pos.ne']

Premises used: Nat.cast_ofNat, mul_div_cancel₀, Complex.div_ofNat_re, sq_abs, abs_nonneg, Real.rpow_natCast_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r 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 : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
⊢ 0 < s.re + 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
⊢ 0 < (s + 1).re

Tactic:
have hs₂ : 0 < (s + 1).re := by rw [add_re, one_re]; positivity
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
⊢ s + 1 ≠ 0

Tactic:
have hs₃ : s + 1 ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs₂)
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
pos : ∀ (h : r i = 0), a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) = 0
neg :
  ∀ (h : ¬r i = 0),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
⊢ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
    if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
h : r i = 0
⊢ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) = 0

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
h : ¬r i = 0
⊢ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
⊢ ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)

Tactic:
have (i t : _) : (a i * r i * rexp (-π * r i ^ 2 * t)) =
      if r i = 0 then 0 else (a i * r i * rexp (-π * r i ^ 2 * t)) := by
    split_ifs with h <;> simp [h]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
h :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t) (i : ι),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
| ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)

Tactic:
enter [t, ht, 1, i]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
i : ι
h : if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
| a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
h :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t) (i : ι),
    if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
| ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)

Tactic:
enter [t, ht, 1, i]; rw [this]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
⊢ ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)

Tactic:
conv at hF => enter [t, ht, 1, i]; rw [this]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
hF₁ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re

Tactic:
conv at hF => enter [t, ht, 1, i]; rw [this]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
hF₁ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum₁ : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
⊢ s ≠ 0

Tactic:
conv at hF => enter [t, ht, 1, i]; rw [this]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
hF₁ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum₁ : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₄ : s ≠ 0
⊢ 0 < (s + 1).re

Tactic:
conv at hF => enter [t, ht, 1, i]; rw [this]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
hF₁ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum₁ : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₄ : s ≠ 0
hs₅ : 0 < (s + 1).re
⊢ s + 1 ≠ 0

Tactic:
conv at hF => enter [t, ht, 1, i]; rw [this]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
hF₁ :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum₁ : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₄ : s ≠ 0
hs₅ : 0 < (s + 1).re
hs₆ : s + 1 ≠ 0
⊢ ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)

Tactic:
conv at hF => enter [t, ht, 1, i]; rw [this]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
⊢ HasSum (fun (i : ι) ↦ (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)) (mellin F ((s + 1) / 2))

Tactic:
hasSum_mellin_pi_mul_sq hs₂ hF ?_

Premises used: hasSum_mellin_pi_mul_sq
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
h :
  ∀ (i : ι),
    (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
      (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
convert! : Summable (α := ℝ) fun (i : ι) ↦ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re
⊢ HasSum (fun (i : ι) ↦ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (mellin F ((s + 1) / 2))

Tactic:
convert! hasSum_mellin_pi_mul_sq hs₂ hF ?_ using 2 with i

Premises used: hasSum_mellin_pi_mul_sq
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
i : ι
h :
  ∀ (h : r i = 0),
    (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
      (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
h₁ :
  ∀ (h : r i ≠ 0),
    (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
      (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
⊢ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)

Tactic:
rcases eq_or_ne (r i) 0 with h | h

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
i : ι
h : r i = 0
h₁ :
  (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / (↑|0| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑0 : ℂ)) / (↑|0| : ℂ) ^ (s + 1)
h₂ :
  (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / (↑0 : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑0 : ℂ)) / (↑0 : ℂ) ^ (s + 1)
h₃ :
  (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / HPow.hPow (α := ℂ) 0 s =
    (s + 1).Gammaℝ * (a i * 0) / HPow.hPow (α := ℂ) 0 (s + 1)
h₄ :
  (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / 0 =
    (s + 1).Gammaℝ * (a i * 0) / HPow.hPow (α := ℂ) 0 (s + 1)
h₅ : (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / 0 = (s + 1).Gammaℝ * (a i * 0) / 0
h₆ : 0 = (s + 1).Gammaℝ * (a i * 0) / 0
h₇ h₈ : Eq (α := ℂ) 0 0
⊢ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)

Tactic:
rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]

Premises used: Complex.zero_cpow, Complex.ofReal_zero, abs_zero, div_zero
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
i : ι
h : r i ≠ 0
h₁ :
  (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / ((↑|r i| : ℂ) ^ s * (↑|r i| : ℂ))
⊢ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)

Tactic:
rw [cpow_add _ _ (ofReal_ne_zero.mpr <| abs_ne_zero.mpr h), cpow_one]

Premises used: Iff.mpr, Complex.ofReal_ne_zero, abs_ne_zero, Complex.cpow_one, Complex.cpow_add
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
i : ι
h : r i ≠ 0
enter : (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ))
| (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / ((↑|r i| : ℂ) ^ s * (↑|r i| : ℂ))

Tactic:
enter [1]