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

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ ‖↑a‖ < 1

Tactic:
]

Goal state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ ‖↑a‖ < 1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 ≠ 0

Tactic:
]

Goal state after:
case e'_5.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 ≠ 0
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ ‖↑a‖ < 1

Tactic:
]

Goal state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ ‖↑a‖ < 1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) = -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x)

Tactic:
]

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

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)

Tactic:
]

Goal state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
x✝ : ℕ
⊢ (fourier ↑x✝) ↑x + (fourier (-↑x✝)) ↑x = (fourier ↑x✝) ↑x + (fourier (-↑x✝)) ↑x

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)

Tactic:
]

Goal state after:
case e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * (z ^ n * z ^ n).re

Tactic:
mul_re,

Goal state after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re * (z ^ n).re - (z ^ n).im * (z ^ n).im)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))

Tactic:
]

Goal state after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x) / 2 = ↑(1 / ↑n ^ (2 * k)) * ↑(Real.cos (2 * π * ↑n * x))

Tactic:
]

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x) / 2 = ↑(1 / ↑n ^ (2 * k)) * ↑(Real.cos (2 * π * ↑n * x))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * (((fourier ↑n) ↑x + (fourier (-↑n)) ↑x) / 2) = ↑(1 / ↑n ^ (2 * k)) * ↑(Real.cos (2 * π * ↑n * x))

Tactic:
]

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * (((fourier ↑n) ↑x + (fourier (-↑n)) ↑x) / 2) = ↑(1 / ↑n ^ (2 * k)) * ↑(Real.cos (2 * π * ↑n * x))
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
⊢ ↑n ^ x ≤ 0 ∨ 1 < ↑n ^ x

Tactic:
]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
⊢ ↑n ^ x ≤ 0 ∨ 1 < ↑n ^ x
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑↑n ^ (2 * k)

Tactic:
]

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑↑n ^ (2 * k)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
⊢ 1 * ↑n ^ (-(I * ↑y)).re = 1

Tactic:
]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
⊢ 1 * ↑n ^ (-(I * ↑y)).re = 1
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ 0 ≤
    3 * (-log (1 - ↑n ^ (-↑x))).re + 4 * (-log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y)))).re +
      (-log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)))).re

Tactic:
]

Goal state after:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ 0 ≤
    3 * (-log (1 - ↑n ^ (-↑x))).re + 4 * (-log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y)))).re +
      (-log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)))).re
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case e'_5.e'_6.e_a
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ ↑n ^ ↑(-x) * (χ ↑n * ↑n ^ (-(I * ↑y))) = ↑n ^ ↑(-x) * (χ ↑n * ↑n ^ (-(I * ↑y)))

Tactic:
]

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

Goal state before:
pp: case e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ ↑n ^ ↑(-x) * (χ ↑n ^ 2 * (↑n ^ (-(I * ↑y))) ^ 2) = ↑n ^ ↑(-x) * (χ ↑n ^ 2 * (↑n ^ (-(I * ↑y))) ^ 2)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (cexp (2 * ↑π * I * ↑n * ↑x) + cexp (2 * ↑π * I * -↑n * ↑x)) / 2 =
    (cexp (2 * ↑π * ↑n * ↑x * I) + cexp (-(2 * ↑π * ↑n * ↑x) * I)) / 2

Tactic:
]

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (cexp (2 * ↑π * I * ↑n * ↑x) + cexp (2 * ↑π * I * -↑n * ↑x)) / 2 =
    (cexp (2 * ↑π * ↑n * ↑x * I) + cexp (-(2 * ↑π * ↑n * ↑x) * I)) / 2
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℝ
⊢ 1 < (1 + ↑x).re ∧ 1 < (1 + ↑x + I * ↑y).re ∧ 1 < (1 + ↑x + 2 * I * ↑y).re

Tactic:
by
  simp only [add_re, one_re, ofReal_re, lt_add_iff_pos_right, hx, mul_re, I_re, zero_mul, I_im,
    ofReal_im, mul_zero, sub_self, add_zero, re_ofNat, im_ofNat, mul_one, mul_im, and_self]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd (𝓕 Φ)
s : ℂ
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
⊢ Differentiable ℂ (completedLFunction (𝓕 Φ))

Tactic:
]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd (𝓕 Φ)
s : ℂ
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
⊢ Differentiable ℂ (completedLFunction (𝓕 Φ))
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : AnalyticOnNhd ℂ F Set.univ
hG : AnalyticOnNhd ℂ G Set.univ
this : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : AnalyticOnNhd ℂ F Set.univ
hG : AnalyticOnNhd ℂ G Set.univ
this : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ ‖cexp (∑' (p : Nat.Primes), -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))) ^ 3 *
          cexp (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))) ^ 4 *
        cexp (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y))))‖ ≥
    1

Tactic:
]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ ‖cexp (∑' (p : Nat.Primes), -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))) ^ 3 *
          cexp (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))) ^ 4 *
        cexp (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y))))‖ ≥
    1
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (↑k + (2 + -1 / 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)

Tactic:
]

Goal state after:
p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (↑k + (2 + -1 / 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))

Tactic:
]

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! *
        ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) /
      2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))

Tactic:
]

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! *
        ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) /
      2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_2.refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p ^ (3 / 2))⁻¹ ≤ 2 * (↑↑p ^ (3 / 2))⁻¹

Tactic:
]

Goal state after:
case refine_2.refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p ^ (3 / 2))⁻¹ ≤ 2 * (↑↑p ^ (3 / 2))⁻¹
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case hbc
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 2 ≤ ↑↑p

Tactic:
]

Goal state after:
case hbc
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 2 ≤ ↑↑p
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    ∑' (b : Nat.Primes),
      (3 * (-log (1 - 1 ↑↑b * ↑↑b ^ (-(1 + ↑x)))).re + 4 * (-log (1 - χ ↑↑b * ↑↑b ^ (-(1 + ↑x + I * ↑y)))).re +
        (-log (1 - (χ ^ 2) ↑↑b * ↑↑b ^ (-(1 + ↑x + 2 * I * ↑y)))).re)

Tactic:
]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    ∑' (b : Nat.Primes),
      (3 * (-log (1 - 1 ↑↑b * ↑↑b ^ (-(1 + ↑x)))).re + 4 * (-log (1 - χ ↑↑b * ↑↑b ^ (-(1 + ↑x + I * ↑y)))).re +
        (-log (1 - (χ ^ 2) ↑↑b * ↑↑b ^ (-(1 + ↑x + 2 * I * ↑y)))).re)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
⊢ Summable (F' ∘ ⇑prodNatEquiv.symm)

Tactic:
]

Goal state after:
case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
⊢ Summable (F' ∘ ⇑prodNatEquiv.symm)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖LSeries (fun x ↦ 1 ↑x) (1 + ↑x) ^ 3 * LSeries (fun x ↦ χ ↑x) (1 + ↑x + I * ↑y) ^ 4 *
        LSeries (fun x ↦ (χ ^ 2) ↑x) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖LSeries (fun x ↦ 1 ↑x) (1 + ↑x) ^ 3 * LSeries (fun x ↦ χ ↑x) (1 + ↑x + I * ↑y) ^ 4 *
        LSeries (fun x ↦ (χ ^ 2) ↑x) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x) =
    1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x)

Tactic:
]

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * ↑y))
⊢ (fun x ↦ LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝 0] fun x ↦ 1

Tactic:
]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * ↑y))
⊢ (fun x ↦ LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝 0] fun x ↦ 1
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1.refine_2
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun x ↦ x + 1
u : Nat.Primes × ℕ
hu : u.2 = 0
⊢ F' u = F' (u.1, u.2)

Tactic:
]

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑q.totient * ↑(residueClass a n) = ∑ χ, χ a⁻¹ * χ ↑n * ↑(Λ n)

Tactic:
]

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑q.totient * ↑(residueClass a n) = ∑ χ, χ a⁻¹ * χ ↑n * ↑(Λ n)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (0 + (1 + I * ↑y))) (0 + (1 + I * ↑y))
⊢ (fun x ↦ LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x ↦ ↑x

Tactic:
]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (0 + (1 + I * ↑y))) (0 + (1 + I * ↑y))
⊢ (fun x ↦ LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x ↦ ↑x
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * I * (2 * ↑π) ^ (2 * k + 1) = -(2 * ↑π * I) ^ (2 * k + 1)

Tactic:
]

Goal state after:
case e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * I * (2 * ↑π) ^ (2 * k + 1) = -(2 * ↑π * I) ^ (2 * k + 1)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ ↑q.totient * L (fun n ↦ ↑(residueClass a n)) s = ∑ x, x a⁻¹ * L ((fun x_1 ↦ x ↑x_1) * fun n ↦ ↑(Λ n)) s

Tactic:
]

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ ↑q.totient * L (fun n ↦ ↑(residueClass a n)) s = ∑ x, x a⁻¹ * L ((fun x_1 ↦ x ↑x_1) * fun n ↦ ↑(Λ n)) s
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s ↦ LFunctionResidueClassAux a s) {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
]

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s ↦ LFunctionResidueClassAux a s) {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inl
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h✝ : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
x : ℝ
h : x ≠ 0
⊢ ↑x = ↑x

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * ((fourier ↑x✝) ↑x - (fourier (-↑x✝)) ↑x) / (2 * I) =
    ↑(1 / ↑x✝ ^ (2 * k + 1)) * ↑(Real.sin (2 * π * ↑x✝ * x))

Tactic:
]

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * ((fourier ↑x✝) ↑x - (fourier (-↑x✝)) ↑x) / (2 * I) =
    ↑(1 / ↑x✝ ^ (2 * k + 1)) * ↑(Real.sin (2 * π * ↑x✝ * x))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * (((fourier ↑x✝) ↑x - (fourier (-↑x✝)) ↑x) / (2 * I)) =
    ↑(1 / ↑x✝ ^ (2 * k + 1)) * ↑(Real.sin (2 * π * ↑x✝ * x))

Tactic:
]

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * (((fourier ↑x✝) ↑x - (fourier (-↑x✝)) ↑x) / (2 * I)) =
    ↑(1 / ↑x✝ ^ (2 * k + 1)) * ↑(Real.sin (2 * π * ↑x✝ * x))