mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: χ : DirichletCharacter ℂ 1
⊢ LFunction χ = riemannZeta

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ deriv (LFunction χ) s = deriv (LSeries fun x ↦ χ ↑x) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
n : ℕ
inst✝ : NeZero n
⊢ LFunction χ (-(2 * ↑n)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
⊢ 2 ∈ {1}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ ↑N ^ (-s) * Φ j * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s) = Φ j * (↑N ^ (-s) * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j * (↑N ^ (-s) * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s)) = Φ j * (1 / ↑↑N ^ s * (1 / ↑((↑j.val + ↑N * ↑m) / ↑N) ^ s))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C' * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ 0 < C' * mulHeight ![a✝, b✝] * mulHeight ![c✝, d✝]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ ∃ C,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 → ![c, d] ≠ 0 → C + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j * (1 / ↑↑N ^ s * (1 / ↑((↑j.val + ↑N * ↑m) / ↑N) ^ s)) = Φ j / (↑↑N * ↑((↑j.val + ↑N * ↑m) / ↑N)) ^ s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
C₁ : ℝ
hC₁ : ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C₁ + logHeight ![a, b] + logHeight ![c, d]
C₂ : ℝ
hC₂ :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C₂ + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ |logHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝] - (logHeight ![a✝, b✝] + logHeight ![c✝, d✝])| ≤ max C₁ (-C₂)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ ∃ C,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 → |logHeight ![a * c, a * d + b * c, b * d] - (logHeight ![a, b] + logHeight ![c, d])| ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑↑N * ↑((↑j.val + ↑N * ↑m) / ↑N)) ^ s = Φ j / (↑N * (↑j.val + ↑N * ↑m) / ↑N) ^ s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
⊢ 1 < re 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑N * (↑j.val + ↑N * ↑m) / ↑N) ^ s = Φ j / (↑j.val + ↑N * ↑m) ^ s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑j.val + ↑N * ↑m) ^ s = Φ ↑(j.val + N * m) / ↑(j.val + N * m) ^ s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ ↑(j.val + N * m) / ↑(j.val + N * m) ^ s = LSeries.term (fun x ↦ Φ ↑x) s (j.val + N * m)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
⊢ LFunction Φ s = LSeries (fun x ↦ Φ ↑x) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun s ↦ ↑N ^ (-s)) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (LFunction Φ) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Φ j / ↑N = Φ j * (1 / ↑N * 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case refine_3.refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
t : ℂ
ht : 1 < t.re
⊢ LFunction ((changeLevel hMN) χ) t = (fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))) t

Tactic:
· simpa [LFunction_eq_LSeries _ ht] using LSeries_changeLevel hMN χ ht

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ : (changeLevel hMN) χ ≠ 1
p : ℕ
hp : p ∈ N.primeFactors
⊢ Continuous fun s ↦ 1 - χ ↑p * ↑p ^ (-s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Tendsto (fun s ↦ (s - 1) * LFunction Φ s) (𝓝[≠] 1) (𝓝 (∑ j, Φ j / ↑N))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1 ∨ s ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunction ((changeLevel ⋯) 1) s = LFunction 1 s * ∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))

Tactic:
convert! LFunction_changeLevel N.one_dvd 1 (.inr hs) using 4 with p

Goal state after:
case a
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
p : ℕ
a✝ : p ∈ N.primeFactors
⊢ ↑p ^ (-s) = 1 ↑p * ↑p ^ (-s)
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * riemannZeta s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (toAddCircle j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
⊢ IsOpen U

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
hp : p ∈ N.primeFactors
⊢ Continuous fun s ↦ 1 - ↑p ^ (-s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ Tendsto (fun s ↦ (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1) (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ.Even
s : ℂ
⊢ χ.gammaFactor s = s.Gammaℝ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ.Odd
s : ℂ
⊢ χ.gammaFactor s = (s + 1).Gammaℝ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: χ : DirichletCharacter ℂ 1
⊢ completedLFunction χ = completedRiemannZeta

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ s ≠ 0 ∨ χ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs₀ : s ≠ 0 ∨ N ≠ 1
hs₁ : s ≠ 1 ∨ χ ≠ 1
⊢ s ≠ 1 ∨ ∑ j, χ j = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
⊢ Differentiable ℂ (completedLFunction χ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: χ : DirichletCharacter ℂ 1
⊢ χ.rootNumber = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
u : ℂ
⊢ u ∈ U ↔ u ≠ 1 ∨ j ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
⊢ ∑ j, χ j = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
⊢ AnalyticOnNhd ℂ f U

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
⊢ AnalyticOnNhd ℂ g U

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
h : j = 0
⊢ 1 < Module.rank ℝ ℂ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 ⇑χ) s =
    ?m.242 * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
⊢ IsPreconnected U

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1)) =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ LFunctionTrivChar₁ n 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ' : (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
⊢ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J') = J

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : ℂ
hs : x✝ ∈ Set.univ \ {1}
⊢ DifferentiableAt ℂ (fun s ↦ (s - 1) * LFunctionTrivChar n s) x✝

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Differentiable ℂ (LFunctionTrivChar₁ n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ n) s = deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s
⊢ DifferentiableAt ℂ (fun w ↦ w - 1) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
⊢ 2 ∈ re ⁻¹' Set.Ioi 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ContinuousOn (fun s ↦ -deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s)
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
hV : V ∈ 𝓝 2
⊢ 2 ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: x : ℝ
⊢ bernoulliFun 0 x = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: x : ℝ
⊢ bernoulliFun 1 x = x - 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
χ : DirichletCharacter ℂ n
hχ : χ ≠ 1
⊢ ContinuousOn (fun s ↦ -deriv (LFunction χ) s / LFunction χ s) {s | LFunction χ s ≠ 0}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: x : ℝ
⊢ bernoulliFun 2 x = x ^ 2 - x + 6⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ bernoulliFun k 0 = ↑(bernoulli k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 1 = bernoulliFun k 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (toAddCircle j) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))
⊢ (algebraMap ℂ ℂ).comp ofRealHom = ofRealHom.comp (algebraMap ℝ ℝ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
⊢ HasDerivAt (bernoulliFun k) (↑k * bernoulliFun (k - 1) x) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ ContDiff ℝ ⊤ (bernoulliFun k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ deriv (bernoulliFun k) = fun x ↦ ↑k * bernoulliFun (k - 1) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
⊢ HasDerivAt (fun x ↦ bernoulliFun (k + 1) x / (↑k + 1)) (bernoulliFun k x) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ ∫ (x : ℝ) in 0..1, bernoulliFun k x = if k = 0 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ ∫ (x : ℝ) in 0..1, bernoulliFun k x = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ cosZeta (↑x) (2 * ↑k) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
⊢ Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
x y : ℝ
⊢ Continuous fun t ↦ ↑(k + 1) * bernoulliFun k t

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
x y : ℝ
⊢ bernoulliFun (k + 1) y = bernoulliFun (k + 1) x + ∫ (t : ℝ) in x..y, ↑(k + 1) * bernoulliFun k t

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
⊢ bernoulliFun k (1 - x) = (-1) ^ k * bernoulliFun k x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
h : ∀ (x : ℝ), f k x = 0
⊢ bernoulliFun k (↑m * x) = ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
⊢ LFunction (𝓕 Φ) s = ∑ j, Φ j * expZeta (toAddCircle (-j)) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
⊢ LFunction Φ (1 - s) =
    ↑N ^ (s - 1) * (2 * ↑π) ^ (-s) * Gamma s *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)

Tactic:
LFunction

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
⊢ ↑N ^ (-(1 - s)) * ∑ j, Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
    ↑N ^ (s - 1) * (2 * ↑π) ^ (-s) * Gamma s *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
⊢ (algebraMap ℂ ℂ).comp ofRealHom = ofRealHom.comp (algebraMap ℝ ℝ)

Tactic:
by

Goal state after: