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
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
h₅ : ‖a i * 0‖ / 0 = ‖a i‖ / 0
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₆ : 0 = ‖a i‖ / 0
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
h₅ : ‖a i * 0‖ / 0 = ‖a i‖ / 0
h₆ : 0 = ‖a i‖ / 0
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₇ : Eq (α := ℝ) 0 0
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
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr 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
h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₂ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr 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
h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
h₂ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₃ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * HPow.hPow (β := ℝ) |r i| 1) = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr 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
h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
h₂ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re
h₃ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * HPow.hPow (β := ℝ) |r i| 1) = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₄ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr 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
h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
h₂ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re
h₃ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * HPow.hPow (β := ℝ) |r i| 1) = ‖a i‖ / |r i| ^ s.re
h₄ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₅ : ‖a i‖ * ‖(↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr 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
h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
h₂ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re
h₃ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * HPow.hPow (β := ℝ) |r i| 1) = ‖a i‖ / |r i| ^ s.re
h₄ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₅ : ‖a i‖ * ‖(↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₆ : ‖a i‖ * ‖r i‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr 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
h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
h₂ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re
h₃ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * HPow.hPow (β := ℝ) |r i| 1) = ‖a i‖ / |r i| ^ s.re
h₄ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₅ : ‖a i‖ * ‖(↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₆ : ‖a i‖ * ‖r i‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₇ : ‖a i‖ * |r i| / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr 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
h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
h₂ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re
h₃ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * HPow.hPow (β := ℝ) |r i| 1) = ‖a i‖ / |r i| ^ s.re
h₄ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₅ : ‖a i‖ * ‖(↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₆ : ‖a i‖ * ‖r i‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₇ : ‖a i‖ * |r i| / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₈ : ‖a i‖ * |r i| / |r i| ^ s.re / |r i| = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr 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
h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
h₂ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re
h₃ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * HPow.hPow (β := ℝ) |r i| 1) = ‖a i‖ / |r i| ^ s.re
h₄ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₅ : ‖a i‖ * ‖(↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₆ : ‖a i‖ * ‖r i‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₇ : ‖a i‖ * |r i| / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₈ : ‖a i‖ * |r i| / |r i| ^ s.re / |r i| = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₉ : ‖a i‖ * |r i| / |r i| / |r i| ^ s.re = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr 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
h₁ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + re 1) = ‖a i‖ / |r i| ^ s.re
h₂ : ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s.re + 1) = ‖a i‖ / |r i| ^ s.re
h₃ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * HPow.hPow (β := ℝ) |r i| 1) = ‖a i‖ / |r i| ^ s.re
h₄ : ‖a i * (↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₅ : ‖a i‖ * ‖(↑(r i) : ℂ)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₆ : ‖a i‖ * ‖r i‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₇ : ‖a i‖ * |r i| / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
h₈ : ‖a i‖ * |r i| / |r i| ^ s.re / |r i| = ‖a i‖ / |r i| ^ s.re
h₉ : ‖a i‖ * |r i| / |r i| / |r i| ^ s.re = ‖a i‖ / |r i| ^ s.re
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
have h₁₀ : ‖a i‖ / |r i| ^ s.re = ‖a i‖ / |r i| ^ s.re
Tactic: rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr h)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
⊢ LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) (p ^ k) : ℂ)
have simp : LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
Tactic: simp only [zetaMul, toArithmeticFunction, coe_zeta_mul_apply, coe_mk,
    Nat.sum_divisors_prime_pow hp, pow_eq_zero_iff', hp.ne_zero, ne_eq, false_and, ↓reduceIte,
    Nat.cast_pow, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
⊢ LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
have inl : ∀ (h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (0 : ℂ)),
  LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
Tactic: rcases MulChar.isQuadratic_iff_sq_eq_one.mpr hχ p with h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
inl :
  ∀ (h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (0 : ℂ)),
    LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
⊢ LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
have inr : ∀ (h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (1 : ℂ)),
  LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
Tactic: rcases MulChar.isQuadratic_iff_sq_eq_one.mpr hχ p with h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
inl :
  ∀ (h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (0 : ℂ)),
    LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
inr :
  ∀ (h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (1 : ℂ)),
    LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
⊢ LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
have inr₁ : ∀ (h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (-1 : ℂ)),
  LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
Tactic: rcases MulChar.isQuadratic_iff_sq_eq_one.mpr hχ p with h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (0 : ℂ)
⊢ LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
have inl : ∀ i ∈ Finset.range (k + 1), 0 ≤ HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) i
Tactic: refine Finset.sum_nonneg fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (1 : ℂ)
⊢ LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
have inr : ∀ i ∈ Finset.range (k + 1), 0 ≤ HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) i
Tactic: refine Finset.sum_nonneg fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (-1 : ℂ)
⊢ LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
have inr : LE.le (α := ℂ) 0 (if _root_.Even (k + 1) then 0 else 1)
Tactic: simp only [h, neg_one_geom_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (-1 : ℂ)
⊢ LE.le (α := ℂ) 0 (if _root_.Even (k + 1) then 0 else 1)
have pos : _root_.Even (k + 1) → LE.le (α := ℂ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (-1 : ℂ)
pos : _root_.Even (k + 1) → LE.le (α := ℂ) 0 0
⊢ LE.le (α := ℂ) 0 (if _root_.Even (k + 1) then 0 else 1)
have neg : ¬_root_.Even (k + 1) → LE.le (α := ℂ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
n : ℕ
⊢ LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) n : ℂ)
have inl : LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) 0 : ℂ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
n : ℕ
inl : LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) 0 : ℂ)
⊢ LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) n : ℂ)
have inr : ∀ (hn : n ≠ 0), LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) n : ℂ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s
have h : DifferentiableAt ℂ (riemannZeta * LFunction B.χ) s
Tactic: apply DifferentiableAt.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
h : DifferentiableAt ℂ (riemannZeta * LFunction B.χ) s
⊢ DifferentiableAt ℂ B.F s
have hL : B.F =ᶠ[𝓝 s] riemannZeta * LFunction B.χ
Tactic: apply DifferentiableAt.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
h : DifferentiableAt ℂ (riemannZeta * LFunction B.χ) s
hL : B.F =ᶠ[𝓝 s] riemannZeta * LFunction B.χ
⊢ DifferentiableAt ℂ B.F s
have f : ℂ → ℂ
Tactic: apply DifferentiableAt.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ B.F =ᶠ[𝓝 s] riemannZeta * LFunction B.χ
have h : ∀ (a : ℂ),
  Membership.mem (γ := Set ℂ)
    {x : ℂ |
      Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ x ≠ 1) x} x →
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ B.F x = (riemannZeta * LFunction B.χ) x) x} x}
    a
Tactic: filter_upwards [eventually_ne_nhds hs] with t ht using Function.update_of_ne ht ..
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Nonvanishing (goal)
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ x ≠ 1) x} x →
          Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ B.F x = (riemannZeta * LFunction B.χ) x) x} x}
      a
⊢ B.F =ᶠ[𝓝 s] riemannZeta * LFunction B.χ
have h₁ : ∀ (a : ℂ), a ≠ 1 → B.F a = (riemannZeta * LFunction B.χ) a
Tactic: filter_upwards [eventually_ne_nhds hs] with t ht using Function.update_of_ne ht ..