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
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
rw : (s + 1).Gammaℝ * (a i * ((↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) * (↑|r i| : ℂ)))
| (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ))

Tactic:
rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe,
        SignType.map_cast]

Premises used: SignType.map_cast, sign_mul_abs, Complex.ofRealHom_eq_coe, Complex.ofReal_mul
-- 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 * ((↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) * (↑|r i| : ℂ)))
| (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / ((↑|r i| : ℂ) ^ s * (↑|r i| : ℂ))

Tactic:
enter [1]; rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe,
        SignType.map_cast]

Premises used: SignType.map_cast, sign_mul_abs, Complex.ofRealHom_eq_coe, Complex.ofReal_mul
-- 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 * ((↑((SignType.sign : (a : ℝ) → SignType) (r 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 * (↑|r i| : ℂ))

Tactic:
conv_rhs => enter [1]; rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe,
        SignType.map_cast]

Premises used: SignType.map_cast, sign_mul_abs, Complex.ofRealHom_eq_coe, Complex.ofReal_mul
-- 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
⊢ (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:
field [h]
-- 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)) : ℂ)
⊢ 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
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 : ι), ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re

Tactic:
convert! h_sum using 2 with i
-- 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), ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re
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

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₁ : ‖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
h₇ h₈ : Eq (α := ℝ) 0 0
⊢ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re

Tactic:
rw [h, abs_zero, ofReal_zero, zero_rpow hs₂.ne', zero_rpow hs.ne', div_zero, div_zero]

Premises used: Real.zero_rpow, LT.lt.ne', 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₁ : ‖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
h₁₀ h₁₁ : ‖a 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

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)]

Premises used: Iff.mpr, div_right_comm, Complex.add_re, norm_mul, Complex.norm_real, abs_ne_zero, Real.rpow_one, mul_div_cancel_right₀, abs_pos, Real.rpow_add, div_div, Complex.one_re, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
⊢ χ.zetaMul.IsMultiplicative

Tactic:
isMultiplicative_zeta.natCast.mul <| isMultiplicative_toArithmeticFunction χ

Premises used: ArithmeticFunction.IsMultiplicative.natCast, ArithmeticFunction.isMultiplicative_zeta, ArithmeticFunction.IsMultiplicative.mul, DirichletCharacter.zetaMul, DirichletCharacter.isMultiplicative_toArithmeticFunction
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑χ.zetaMul : (a : ℕ) → ℂ) s

Tactic:
ArithmeticFunction.LSeriesSummable_mul (LSeriesSummable_zeta_iff.mpr hs) <|
    LSeriesSummable_of_bounded_of_one_lt_re (m := 1) (fun n hn ↦ ?_) hs

Premises used: Iff.mpr, LSeriesSummable_of_bounded_of_one_lt_re, ArithmeticFunction.LSeriesSummable_zeta_iff, ArithmeticFunction.LSeriesSummable_mul, DirichletCharacter.zetaMul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ norm (E := ℂ) ((toArithmeticFunction fun (x : ℕ) ↦ (χ : (a : ZMod N) → ℂ) (↑x : ZMod N) : (a : ℕ) → ℂ) n : ℂ) ≤ 1

Tactic:
simpa only [toArithmeticFunction, coe_mk, hn, ↓reduceIte]
  using norm_le_one χ _

Premises used: toArithmeticFunction, DirichletCharacter.norm_le_one, ArithmeticFunction.coe_mk, reduceIte
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
simp : LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)
⊢ LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) (p ^ k) : ℂ)

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]

Premises used: toArithmeticFunction, false_and, pow_eq_zero_iff', ArithmeticFunction.coe_mk, map_pow, ne_eq, Nat.Prime.ne_zero, Nat.sum_divisors_prime_pow, reduceIte, DirichletCharacter.zetaMul, Nat.cast_pow, ArithmeticFunction.coe_zeta_mul_apply
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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)
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)

Tactic:
rcases MulChar.isQuadratic_iff_sq_eq_one.mpr hχ p with h | h | h

Premises used: Iff.mpr, MulChar.isQuadratic_iff_sq_eq_one, Nat.cast
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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)

Tactic:
Finset.sum_nonneg fun i _ ↦ ?_

Premises used: Finset.sum_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (0 : ℂ)
inl : ∀ i ∈ Finset.range (k + 1), 0 ≤ HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) i
⊢ LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)

Tactic:
refine Finset.sum_nonneg fun i _ ↦ ?_

Premises used: Finset.sum_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (0 : ℂ)
i : ℕ
h_1 : i ∈ Finset.range (k + 1)
⊢ 0 ≤ HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) i

Tactic:
simp only [h, le_refl, pow_nonneg]

Premises used: le_refl, pow_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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)

Tactic:
Finset.sum_nonneg fun i _ ↦ ?_

Premises used: Finset.sum_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (1 : ℂ)
inr : ∀ i ∈ Finset.range (k + 1), 0 ≤ HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) i
⊢ LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)

Tactic:
refine Finset.sum_nonneg fun i _ ↦ ?_

Premises used: Finset.sum_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (1 : ℂ)
i : ℕ
h_1 : i ∈ Finset.range (k + 1)
⊢ 0 ≤ HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) i

Tactic:
simp only [h, one_pow, zero_le_one]

Premises used: one_pow, zero_le_one
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (-1 : ℂ)
inr : LE.le (α := ℂ) 0 (if _root_.Even (k + 1) then 0 else 1)
⊢ LE.le (α := ℂ) 0 (∑ x ∈ Finset.range (k + 1), HPow.hPow (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) x)

Tactic:
simp only [h, neg_one_geom_sum]

Premises used: neg_one_geom_sum
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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
neg : ¬_root_.Even (k + 1) → LE.le (α := ℂ) 0 1
⊢ LE.le (α := ℂ) 0 (if _root_.Even (k + 1) then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (-1 : ℂ)
h_1 : _root_.Even (k + 1)
⊢ LE.le (α := ℂ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (-1 : ℂ)
h_1 : ¬_root_.Even (k + 1)
⊢ LE.le (α := ℂ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : Eq (α := ℂ) ((χ : (a : ZMod N) → ℂ) (↑p : ZMod N) : ℂ) (-1 : ℂ)
h_1 : _root_.Even (k + 1)
⊢ LE.le (α := ℂ) 0 0

Tactic:
exacts [le_rfl, zero_le_one]

Premises used: le_rfl, zero_le_one
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
n : ℕ
inl : LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) 0 : ℂ)
inr : ∀ (hn : n ≠ 0), LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) n : ℂ)
⊢ LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) n : ℂ)

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
⊢ LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) 0 : ℂ)

Tactic:
simp only [ArithmeticFunction.map_zero, le_refl]

Premises used: le_refl, ArithmeticFunction.map_zero
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
χ : DirichletCharacter ℂ N
hχ : HPow.hPow (β := ℕ) χ 2 = 1
n : ℕ
hn : n ≠ 0
⊢ LE.le (α := ℂ) (0 : ℂ) ((χ.zetaMul : (a : ℕ) → ℂ) n : ℂ)

Tactic:
simpa only [χ.isMultiplicative_zetaMul.multiplicative_factorization _ hn] using
      Finset.prod_nonneg
        fun p hp ↦ zetaMul_prime_pow_nonneg hχ (Nat.prime_of_mem_primeFactors hp) _

Premises used: DirichletCharacter.zetaMul_prime_pow_nonneg, ArithmeticFunction.IsMultiplicative.multiplicative_factorization, Nat.prime_of_mem_primeFactors, DirichletCharacter.isMultiplicative_zetaMul, Finset.prod_nonneg
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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.χ
f : ℂ → ℂ
⊢ DifferentiableAt ℂ B.F s

Tactic:
apply DifferentiableAt.congr_of_eventuallyEq

Premises used: DifferentiableAt.congr_of_eventuallyEq
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ (riemannZeta * LFunction B.χ) s

Tactic:
(differentiableAt_riemannZeta hs).mul <| differentiableAt_LFunction B.χ s (.inl hs)

Premises used: DifferentiableAt.mul, DirichletCharacter.differentiableAt_LFunction, _private.0.DirichletCharacter.BadChar.χ, differentiableAt_riemannZeta, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ (riemannZeta * LFunction B.χ) s

Tactic:
exact (differentiableAt_riemannZeta hs).mul <| differentiableAt_LFunction B.χ s (.inl hs)

Premises used: DifferentiableAt.mul, DirichletCharacter.differentiableAt_LFunction, _private.0.DirichletCharacter.BadChar.χ, differentiableAt_riemannZeta, Or.inl
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
t : ℂ
ht : t ≠ 1
⊢ B.F t = (riemannZeta * LFunction B.χ) t

Tactic:
Function.update_of_ne ht ..

Premises used: _private.0.DirichletCharacter.BadChar.F, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
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
h₁ h₂ : ∀ (t : ℂ) (ht : t ≠ 1), B.F t = (riemannZeta * LFunction B.χ) t
⊢ B.F =ᶠ[𝓝 s] riemannZeta * LFunction B.χ

Tactic:
filter_upwards [eventually_ne_nhds hs] with t ht using Function.update_of_ne ht ..

Premises used: eventually_ne_nhds
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
rw :
  Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
hf : LSeriesSummable (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s
hg : LSeriesSummable (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
⊢ B.F s = LSeries (⇑B.χ.zetaMul : (a : ℕ) → ℂ) s

Tactic:
rw [F, zetaMul, ← coe_mul, LSeries_convolution']

Premises used: ArithmeticFunction.coe_mul, LSeries_convolution', _private.0.DirichletCharacter.BadChar.F, DirichletCharacter.zetaMul
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
h : s = 1
⊢ False

Tactic:
simp only [h, one_re, lt_self_iff_false] at hs

Premises used: lt_self_iff_false, Complex.one_re
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ s ≠ 1

Tactic:
have hs' : s ≠ 1 := fun h ↦ by simp only [h, one_re, lt_self_iff_false] at hs
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
simp :
  riemannZeta s * LSeries (fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
⊢ Function.update (β := fun (a : ℂ) ↦ ℂ) (fun (s : ℂ) ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s

Tactic:
simp only [ne_eq, hs', not_false_eq_true, Function.update_of_ne, B.χ.LFunction_eq_LSeries hs]

Premises used: DirichletCharacter.LFunction_eq_LSeries, ne_eq, _private.0.DirichletCharacter.BadChar.χ, not_false_eq_true, Function.update_of_ne
-- Module: Mathlib.NumberTheory.LSeries.Nonvanishing
Goal:
N : ℕ
inst : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
e_a : riemannZeta s = LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s
e_a₁ :
  LSeries (fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s =
    LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s
⊢ riemannZeta s * LSeries (fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) s =
    LSeries (⇑(↑zeta : ArithmeticFunction ℂ) : (a : ℕ) → ℂ) s *
      LSeries (⇑(toArithmeticFunction fun (x : ℕ) ↦ (B.χ : (a : ZMod N) → ℂ) (↑x : ZMod N)) : (a : ℕ) → ℂ) s

Tactic:
congr 1