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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (-f) s n = -term f s n

Tactic:
by

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

Goal state before:
pp: k : ℕ
⊢ riemannZeta (-↑k) = (-1) ^ k * ↑(bernoulli (k + 1)) / (↑k + 1)

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
s a : ℂ
hf : LSeriesHasSum f s a
⊢ LSeriesHasSum (-f) s (-a)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ}, y ∈ Ico 0 1 → HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ k ≠ 1

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (-f) s

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
⊢ LSeries (-f) s = -LSeries f s

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
⊢ term (f - g) s = term f s - term g s

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f - g) s n = term f s n - term g s n

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f - g) s (a - b)

Tactic:
by

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

Goal state before:
pp: m n : ℕ
z : ℂ
x : ℝ
⊢ 0 ≤ (↑n + 1)⁻¹

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeriesSummable (f - g) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
⊢ LFunction Φ s = completedLFunction Φ s / s.Gammaℝ

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ LFunction Φ s = completedLFunction Φ s / (s + 1).Gammaℝ

Tactic:
by

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

Goal state before:
pp: m n : ℕ
z : ℂ
x : ℝ
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeries (f - g) s = LSeries f s - LSeries g s

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
c s : ℂ
⊢ term (c • f) s = c • term f s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
this :
  ∀ {y : ℝ}, y ∈ Ico 0 1 → HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
c s : ℂ
n : ℕ
⊢ term (c • f) s n = c * term f s n

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
c s a : ℂ
hf : LSeriesHasSum f s a
⊢ LSeriesHasSum (c • f) s (c * a)

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
c s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (c • f) s

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
c s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (c • f) s

Tactic:
by
  simpa [LSeriesSummable, term_smul] using! hf.const_smul c

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
this : ∑ x, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
c s : ℂ
hc : c ≠ 0
hf : LSeriesSummable (c • f) s
⊢ LSeriesSummable f s

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
c s : ℂ
⊢ LSeries (c • f) s = c * LSeries f s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
this : ∑ x, Φ x * cosZeta (toAddCircle x) s = LFunction (𝓕 Φ) s
⊢ ∑ x, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
x : ℝ
m : ℕ
hm : m ≤ n + 1
⊢ F x m = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
x✝ : ℕ
⊢ term (∑ i ∈ S, f i) s x✝ = (∑ i ∈ S, term (f i) s) x✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
a : ι → ℂ
hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)
⊢ LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
⊢ k ≠ 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ LSeriesSummable (∑ i ∈ S, f i) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ ∀ (x : ZMod N),
    Φ x * expZeta (toAddCircle x) s = Φ ((Equiv.neg (ZMod N)) x) * expZeta (-toAddCircle ((Equiv.neg (ZMod N)) x)) s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s
⊢ 0 < (s + 1).re

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑χ.zetaMul) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
⊢ k ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
⊢ ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
⊢ 0 ≤ χ.zetaMul (p ^ k)

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
this : ∑ x, Φ x * sinZeta (toAddCircle x) s = I * LFunction (𝓕 Φ) s
⊢ ∑ x, Φ x * completedSinZeta (toAddCircle x) s = I * completedLFunction (𝓕 Φ) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
n : ℕ
⊢ 0 ≤ χ.zetaMul n

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
x : ℝ
m : ℕ
hm : m ≠ n + 1
⊢ F x m = (↑n + 1) ^ ↑x * term f (↑x) m

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ ∑ x, Φ x * sinZeta (toAddCircle x) s =
    (∑ x, Φ x * expZeta (toAddCircle x) s) / (2 * I) - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I)

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
x : ℝ
hx : x ≥ y
⊢ Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
x : ZMod N
⊢ Φ (-x) * expZeta (toAddCircle (-x)) s = Φ ((Equiv.neg (ZMod N)) x) * expZeta (toAddCircle ((Equiv.neg (ZMod N)) x)) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (∑ x, Φ x * expZeta (toAddCircle x) s) / (2 * I) - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    (∑ x, Φ (-x) * expZeta (toAddCircle (-x)) s) / ?m.227 - ?m.229

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
h : s = 1
⊢ False

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (∑ x, Φ (-x) * expZeta (toAddCircle (-x)) s) / (2 * I) - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    -I⁻¹ * LFunction (𝓕 Φ) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ -I⁻¹ * LFunction (𝓕 Φ) s = I * LFunction (𝓕 Φ) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ B.F s = LSeries (⇑B.χ.zetaMul) s

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
⊢ B.F = G * H

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
⊢ ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
⊢ Differentiable ℂ B.F

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ -2 ≠ 1

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
⊢ B.F ↑(-2) = 0

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
⊢ Uc.Countable

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
⊢ LFunction χ 1 ≠ 0

Tactic:
by

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

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

Tactic:
by

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
⊢ ‖↑a * z‖ < 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ k ≠ 0

Tactic:
by

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
⊢ ‖↑a * z ^ 2‖ < 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x))
    (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ 2 ≤ 2 * k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ 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))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: 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))
⊢ ↑2 = 2

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
⊢ Summable (F y)

Tactic:
by

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

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
⊢ 0 ≤ 3 * (-log (1 - ↑a)).re + 4 * (-log (1 - ↑a * z)).re + (-log (1 - ↑a * z ^ 2)).re

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
⊢ IsPreconnected U

Tactic:
by

Goal state after:
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) < 1

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
k : ℕ
H : n + 1 < k
⊢ 0 ≤ ↑k / (↑n + 1)

Tactic:
by

Goal state after:
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
⊢ 0 < n

Tactic:
by

Goal state after:
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
⊢ ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ ↑k / (↑n + 1)
⊢ 0 ≤ (↑n + 1) / ↑k

Tactic:
by

Goal state after:
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
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ 0 ≤ ↑n ^ (-x)

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
⊢ AnalyticOnNhd ℂ F U

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ ↑k / (↑n + 1)
H₀' : 0 ≤ (↑n + 1) / ↑k
⊢ ↑k / (↑n + 1) = ↑(↑k / (↑n + 1))

Tactic:
by

Goal state after:
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
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ ¬n = 0

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
t : ℂ
ht : t ∈ U
h : Φ 0 = 0
⊢ ∑ j, 𝓕 Φ j = 0

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
⊢ AnalyticOnNhd ℂ G U

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
hG : AnalyticOnNhd ℂ G U
⊢ 2 ∈ re ⁻¹' Set.Ioi 1

Tactic:
by

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
hG : AnalyticOnNhd ℂ G U
hV : {z | 1 < z.re} ∈ 𝓝 2
t : ℂ
ht : t ∈ {z | 1 < z.re}
⊢ F t = G t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ 0 ≤ ↑↑p ^ (-s).re

Tactic:
by

Goal state after: