awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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
⊢ (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)
have h₁ : (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / (↑|0| : ℂ) ^ s =
  (s + 1).Gammaℝ * (a i * (↑0 : ℂ)) / (↑|0| : ℂ) ^ (s + 1)
Tactic: rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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)
⊢ (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)
have h₂ : (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / (↑0 : ℂ) ^ s =
  (s + 1).Gammaℝ * (a i * (↑0 : ℂ)) / (↑0 : ℂ) ^ (s + 1)
Tactic: rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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)
⊢ (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)
have 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)
Tactic: rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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)
⊢ (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)
have h₄ : (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / 0 =
  (s + 1).Gammaℝ * (a i * 0) / HPow.hPow (α := ℂ) 0 (s + 1)
Tactic: rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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)
⊢ (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)
have h₅ : (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℂ) / 0 = (s + 1).Gammaℝ * (a i * 0) / 0
Tactic: rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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
⊢ (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)
have h₆ : 0 = (s + 1).Gammaℝ * (a i * 0) / 0
Tactic: rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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
⊢ (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)
have h₇ : Eq (α := ℂ) 0 0
Tactic: rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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
⊢ (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)
have 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| : ℂ))
Tactic: rw [cpow_add _ _ (ofReal_ne_zero.mpr <| abs_ne_zero.mpr h), cpow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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
| (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / ((↑|r i| : ℂ) ^ s * (↑|r i| : ℂ))
have enter : (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ))
Tactic: enter [1]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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
| (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ))
have rw : (s + 1).Gammaℝ * (a i * ((↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) * (↑|r i| : ℂ)))
Tactic: rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe,
        SignType.map_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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
| (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / ((↑|r i| : ℂ) ^ s * (↑|r i| : ℂ))
have enter : (s + 1).Gammaℝ * (a i * ((↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) * (↑|r i| : ℂ)))
Tactic: enter [1]; rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe,
        SignType.map_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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
⊢ (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| : ℂ))
have h₁ : (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
  (s + 1).Gammaℝ * (a i * ((↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) * (↑|r i| : ℂ))) /
    ((↑|r i| : ℂ) ^ s * (↑|r i| : ℂ))
Tactic: conv_rhs => enter [1]; rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe,
        SignType.map_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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)) : ℂ)
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re
have h : ∀ (i : ι), ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
Tactic: convert! h_sum using 2 with i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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 : ι
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h : ∀ (h : r i = 0), ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
Tactic: rcases eq_or_ne (r i) 0 with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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), ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₁ : ∀ (h : r i ≠ 0), ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
Tactic: rcases eq_or_ne (r i) 0 with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₁ : ‖a i * (↑0 : ℂ)‖ / HPow.hPow (α := ℝ) |0| (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) |0| s.re
Tactic: rw [h, abs_zero, ofReal_zero, zero_rpow hs₂.ne', zero_rpow hs.ne', div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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₁ : ‖a i * (↑0 : ℂ)‖ / HPow.hPow (α := ℝ) |0| (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) |0| s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₂ : ‖a i * (↑0 : ℂ)‖ / HPow.hPow (α := ℝ) 0 (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) 0 s.re
Tactic: rw [h, abs_zero, ofReal_zero, zero_rpow hs₂.ne', zero_rpow hs.ne', div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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₁ : ‖a i * (↑0 : ℂ)‖ / HPow.hPow (α := ℝ) |0| (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) |0| s.re
h₂ : ‖a i * (↑0 : ℂ)‖ / HPow.hPow (α := ℝ) 0 (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) 0 s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₃ : ‖a i * 0‖ / HPow.hPow (α := ℝ) 0 (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) 0 s.re
Tactic: rw [h, abs_zero, ofReal_zero, zero_rpow hs₂.ne', zero_rpow hs.ne', div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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₁ : ‖a i * (↑0 : ℂ)‖ / HPow.hPow (α := ℝ) |0| (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) |0| s.re
h₂ : ‖a i * (↑0 : ℂ)‖ / HPow.hPow (α := ℝ) 0 (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) 0 s.re
h₃ : ‖a i * 0‖ / HPow.hPow (α := ℝ) 0 (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) 0 s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₄ : ‖a i * 0‖ / 0 = ‖a i‖ / HPow.hPow (α := ℝ) 0 s.re
Tactic: rw [h, abs_zero, ofReal_zero, zero_rpow hs₂.ne', zero_rpow hs.ne', div_zero, div_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
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₁ : ‖a i * (↑0 : ℂ)‖ / HPow.hPow (α := ℝ) |0| (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) |0| s.re
h₂ : ‖a i * (↑0 : ℂ)‖ / HPow.hPow (α := ℝ) 0 (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) 0 s.re
h₃ : ‖a i * 0‖ / HPow.hPow (α := ℝ) 0 (s + 1).re = ‖a i‖ / HPow.hPow (α := ℝ) 0 s.re
h₄ : ‖a i * 0‖ / 0 = ‖a i‖ / HPow.hPow (α := ℝ) 0 s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₅ : ‖a i * 0‖ / 0 = ‖a i‖ / 0
Tactic: rw [h, abs_zero, ofReal_zero, zero_rpow hs₂.ne', zero_rpow hs.ne', div_zero, div_zero]