awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
pos : ∀ (h : p i = 0), Eq (α := ℂ) 0 0 ∨ 0 < p i
neg : ∀ (h : ¬p i = 0), a i = 0 ∨ 0 < p i
⊢ (if p i = 0 then 0 else a i) = 0 ∨ 0 < p i

Tactic:
split_ifs with h
-- 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 : ι
h : p i = 0
pos pos₁ : ¬Eq (α := ℂ) 0 0 → 0 < p i
⊢ Eq (α := ℂ) 0 0 ∨ 0 < p i

Tactic:
tauto
-- 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 : ι
h : p i = 0
pos pos₁ : ¬Eq (α := ℂ) 0 0 → 0 < p i
⊢ Eq (α := ℂ) 0 0 ∨ 0 < p i

Tactic:
try tauto
-- 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 : ι
h : ¬p i = 0
⊢ a i = 0 ∨ 0 < p i

Tactic:
Or.inr (lt_of_le_of_ne (hp i) (Ne.symm h))

Premises used: Ne.symm, Or.inr, lt_of_le_of_ne
-- 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 : ι
h : ¬p i = 0
⊢ a i = 0 ∨ 0 < p i

Tactic:
exact Or.inr (lt_of_le_of_ne (hp i) (Ne.symm h))

Premises used: Ne.symm, Or.inr, lt_of_le_of_ne
-- 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 : ι), a' i = 0 ∨ 0 < p i

Tactic:
have hp' i : a' i = 0 ∨ 0 < p i := by
    simp only [a']
    split_ifs with h <;> try tauto
    exact Or.inr (lt_of_le_of_ne (hp i) (Ne.symm h))
-- 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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
i : ι
t : ℝ
⊢ (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)

Tactic:
simp [a']
-- 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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
⊢ ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)

Tactic:
have (i t : _) : (if p i = 0 then 0 else a i * rexp (-π * p i * t)) =
      a' i * rexp (-π * p i * t) := by
    simp [a']
-- 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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
⊢ ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)

Tactic:
simp_rw [this] at hF
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s) (mellin F s)

Tactic:
hasSum_mellin_pi_mul hp' hs hF ?_

Premises used: hasSum_mellin_pi_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
h :
  ∀ (i : ι),
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
      (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s
convert! : Summable (α := ℝ) fun (i : ι) ↦ ‖a' i‖ / p i ^ s.re
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s) (mellin F s)

Tactic:
convert! hasSum_mellin_pi_mul hp' hs hF ?_ using 2 with i

Premises used: hasSum_mellin_pi_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h :
  ∀ (h : p i = 0),
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
      (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s
h₁ :
  ∀ (h : p i ≠ 0),
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
      (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s
⊢ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s

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

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : p i = 0
⊢ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s

Tactic:
simp [a', h, ofReal_zero, zero_cpow hs', div_zero]

Premises used: Complex.zero_cpow, Complex.ofReal_zero, div_zero
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : p i ≠ 0
⊢ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s

Tactic:
simp [a', h, ofReal_zero, zero_cpow hs', div_zero]

Premises used: Complex.zero_cpow, Complex.ofReal_zero, div_zero
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a' i‖ / p i ^ s.re

Tactic:
h_sum.of_norm_bounded (fun i ↦ ?_)

Premises used: Summable.of_norm_bounded
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
refine : ∀ (i : ι), ‖‖a' i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a' i‖ / p i ^ s.re

Tactic:
refine h_sum.of_norm_bounded (fun i ↦ ?_)

Premises used: Summable.of_norm_bounded
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
simp : ‖‖if p i = 0 then 0 else a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
⊢ ‖‖a' i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
simp only [a']
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
pos : p i = 0 → ‖Norm.norm (E := ℂ) 0 / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
neg : ¬p i = 0 → ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
⊢ ‖‖if p i = 0 then 0 else a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : p i = 0
pos : 0 ≤ ‖a i‖ / p i ^ s.re
⊢ ‖Norm.norm (E := ℂ) 0 / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
simp only [norm_zero, zero_div]

Premises used: norm_zero, zero_div
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : p i = 0
⊢ 0 ≤ ‖a i‖ / p i ^ s.re

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : ¬p i = 0
⊢ 0 ≤ p i

Tactic:
have := hp i
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this_1 :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : ¬p i = 0
this : 0 ≤ p i
⊢ 0 ≤ ‖a i‖ / p i ^ s.re

Tactic:
positivity
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
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
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this_1 :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : ¬p i = 0
this : 0 ≤ p i
neg neg₁ : ‖a i‖ / p i ^ s.re ≤ ‖a i‖ / p i ^ s.re
⊢ ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
rw [norm_of_nonneg (by positivity)]

Premises used: Real.norm_of_nonneg
-- 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 : ι) ↦ if r i = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
rw : 0 < s.re / 2
⊢ 0 < (s / 2).re

Tactic:
rw [div_ofNat_re]

Premises used: Complex.div_ofNat_re
-- 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 : ι) ↦ if r i = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
⊢ 0 < s.re / 2

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 : ι) ↦ if r i = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
⊢ 0 < (s / 2).re

Tactic:
have hs' : 0 < (s / 2).re := by rw [div_ofNat_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 : ι) ↦ if r i = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
⊢ ∀ (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)

Tactic:
simp_rw [← sq_eq_zero_iff (a := r _)] at hF

Premises used: sq_eq_zero_iff
-- 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)
⊢ HasSum
    (fun (i : ι) ↦ (↑π : ℂ) ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i / (↑(HPow.hPow (β := ℕ) (r i) 2) : ℂ) ^ (s / 2))
    (mellin F (s / 2))

Tactic:
hasSum_mellin_pi_mul₀ (fun i ↦ sq_nonneg (r i)) hs' hF ?_

Premises used: hasSum_mellin_pi_mul₀, sq_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)
h : ∀ (i : ι), s.Gammaℝ * a i = (↑π : ℂ) ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i
h₁ : ∀ (i : ι), (↑|r i| : ℂ) ^ s = (↑(HPow.hPow (β := ℕ) (r i) 2) : ℂ) ^ (s / 2)
convert! : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re
⊢ HasSum (fun (i : ι) ↦ s.Gammaℝ * a i / (↑|r i| : ℂ) ^ s) (mellin F (s / 2))

Tactic:
convert! hasSum_mellin_pi_mul₀ (fun i ↦ sq_nonneg (r i)) hs' hF ?_ using 3 with i

Premises used: hasSum_mellin_pi_mul₀, sq_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 : ι
h : s.Gammaℝ * a i = (↑π : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2) * a i
h₁ h₂ : (↑π : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2) * a i = (↑π : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2) * a i
⊢ s.Gammaℝ * a i = (↑π : ℂ) ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i

Tactic:
rw [← neg_div, Gammaℝ_def]

Premises used: Complex.Gammaℝ_def, neg_div
-- 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 : (↑|r i| : ℂ) ^ s = (↑|r i| : ℂ) ^ ((↑2 : ℂ) * (s / 2))
h₁ : -π < (↑2 : ℝ) * (↑|r i| : ℂ).arg
h₂ : (↑2 : ℝ) * (↑|r i| : ℂ).arg ≤ π
⊢ (↑|r i| : ℂ) ^ s = (↑(HPow.hPow (β := ℕ) (r i) 2) : ℂ) ^ (s / 2)

Tactic:
rw [← sq_abs, ofReal_pow, ← cpow_nat_mul']

Premises used: Complex.cpow_nat_mul', sq_abs, Complex.ofReal_pow
-- 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 : ι
⊢ (↑|r i| : ℂ) ^ s = (↑|r i| : ℂ) ^ ((↑2 : ℂ) * (s / 2))

Tactic:
ring_nf
-- 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