mathlib-initiative/mathlib-tactics huggingface dataset:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑((IsDedekindDomain.idealFactorsFunOfQuotHom ⋯) ⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
]

Goal state after:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑((IsDedekindDomain.idealFactorsFunOfQuotHom ⋯) ⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * (↑(if k = 1 then 1 else 0) - fourierCoeffOn ⋯ (fun x ↦ ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun x ↦ ↑(bernoulliFun (k - 1) x)) n)

Tactic:
]

Goal state after:
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * (↑(if k = 1 then 1 else 0) - fourierCoeffOn ⋯ (fun x ↦ ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun x ↦ ↑(bernoulliFun (k - 1) x)) n)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (Ideal.map (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          ↑⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩)) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
]

Goal state after:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (Ideal.map (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          ↑⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩)) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0
⊢ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s =
    ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s

Tactic:
]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
j : ZMod N
⊢ -completedHurwitzZetaOdd (toAddCircle j) s = -completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inl
k : ℕ
hk : k ≠ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if 1 = 1 then 1 else 0) - ↑1 * bernoulliFourierCoeff (1 - 1) n) =
    -↑1! / (2 * ↑π * I * ↑n) ^ 1

Tactic:
]

Goal state after:
case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if 1 = 1 then 1 else 0) - ↑1 * bernoulliFourierCoeff (1 - 1) n) =
    -↑1! / (2 * ↑π * I * ↑n) ^ 1
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0
⊢ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s =
    ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ -(1 / (2 * ↑π * I * ↑n)) = -(1 / (2 * ↑π * I * ↑n))

Tactic:
]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaEven (toAddCircle j) s = completedHurwitzZetaEven (toAddCircle j) s

Tactic:
]

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

Goal state before:
pp: Φ : ZMod 1 → ℂ
s : ℂ
⊢ Φ 1 * completedRiemannZeta s = Φ 1 * completedRiemannZeta s

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * -(↑(k + 1) * (-↑k ! / (2 * ↑π * I * ↑n) ^ k)) =
    -(↑(k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n) ^ 1)

Tactic:
]

Goal state after:
case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * -(↑(k + 1) * (-↑k ! / (2 * ↑π * I * ↑n) ^ k)) =
    -(↑(k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n) ^ 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e'_2
k : ℕ
hk : k ≠ 0
⊢ ∑' (n : ℕ), 1 / ↑n ^ (2 * k) = ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k))

Tactic:
]

Goal state after:
case e'_2
k : ℕ
hk : k ≠ 0
⊢ ∑' (n : ℕ), 1 / ↑n ^ (2 * k) = ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
⊢ fourierCoeffOn ⋯ (ofReal ∘ bernoulliFun k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
]

Goal state after:
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal ∘ bernoulliFun k)
⊢ fourierCoeffOn ⋯ (ofReal ∘ bernoulliFun k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
n : ℤ
⊢ -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
]

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

Goal state before:
pp: case e'_2
⊢ ∑' (n : ℕ), 1 / ↑n ^ 2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)

Tactic:
]

Goal state after:
case e'_2
⊢ ∑' (n : ℕ), 1 / ↑n ^ 2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)
Module: Mathlib.NumberTheory.LSeries.ZMod

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

Tactic:
]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : s ≠ 1
⊢ s ≠ 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e'_2
⊢ ∑' (n : ℕ), 1 / ↑n ^ 4 = ↑(∑' (b : ℕ), ↑1 / ↑b ^ 4)

Tactic:
]

Goal state after:
case e'_2
⊢ ∑' (n : ℕ), 1 / ↑n ^ 4 = ↑(∑' (b : ℕ), ↑1 / ↑b ^ 4)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x ↦ ‖1 / ↑x ^ k‖) = fun x ↦ |1 / ↑x ^ k|
⊢ 1 < k

Tactic:
]

Goal state after:
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x ↦ ‖1 / ↑x ^ k‖) = fun x ↦ |1 / ↑x ^ k|
⊢ 1 < k
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx✝ : x ∈ Icc 0 1
hx : x ∈ Ico 0 1 ∨ x = 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:
]

Goal state after:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx✝ : x ∈ Icc 0 1
hx : x ∈ Ico 0 1 ∨ x = 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))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inl
⊢ -(1 / 2) = -(1 / 2)

Tactic:
]

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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ span {(aeval x) Q} ⊔ ker (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) =
    span {(aeval x) Q} ⊔ Ideal.map (algebraMap R S) I

Tactic:
Ideal.mk_ker

Goal state after:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ span {(aeval x) Q} ⊔ Ideal.map (algebraMap R S) I = span {(aeval x) Q} ⊔ Ideal.map (algebraMap R S) I
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ span {(aeval x) Q} ⊔ Ideal.map (algebraMap R S) I = span {(aeval x) Q} ⊔ Ideal.map (algebraMap R S) I

Tactic:
]

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

Goal state before:
pp: case inr
k : ℕ
hk : k ≠ 0
⊢ -↑(bernoulli' (k + 1)) / (↑k + 1) = -↑(bernoulli' (k + 1)) / (↑k + 1)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
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))
⊢ (fun n ↦ 1 / ↑n ^ k * (fourier n) 0) = fun n ↦ 1 / ↑n ^ k * (fourier n) 0

Tactic:
]

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

Goal state before:
pp: case e_a.e_f.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
i : ZMod N
hi : i ≠ 0
⊢ Φ i * (completedHurwitzZetaEven (toAddCircle i) s / s.Gammaℝ) =
    Φ i * (completedHurwitzZetaEven (toAddCircle i) s / s.Gammaℝ)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case e_a.e_f.inr.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0
⊢ Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ) =
    Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
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))
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 0) = -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 0)

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * ((↑n + 1) ^ ↑x / ↑m ^ ↑x) = z * ((↑m / (↑n + 1)) ^ ↑x)⁻¹
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹

Tactic:
]

Goal state after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case e_a.e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑(↑n + 1) ^ ↑x = ↑(↑n + 1) ^ ↑x

Tactic:
]

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 (ofReal ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
]

Goal state after:
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 (ofReal ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑zeta) s * LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s

pp: case hf
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑↑zeta) s

pp: case hg
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s

Tactic:
]

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑zeta) s * LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s

case hf
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑↑zeta) s

case hg
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s
Module: Mathlib.NumberTheory.ZetaValues

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

pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ (2 * ↑π * I) ^ k ≠ 0

pp: case e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ ↑k ! ≠ 0

Tactic:
]

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ (2 * ↑π * I) ^ k ≠ 0

case e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ ↑k ! ≠ 0
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:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ ¬2 * ↑π * I = 0 ∨ ¬k ≠ 0

Tactic:
]

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ ¬2 * ↑π * I = 0 ∨ ¬k ≠ 0
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 : ℝ
hx : x ≥ y
⊢ (f (n + 1) + ∑' (n_1 : ℕ), if n_1 = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) n_1) = f (n + 1) + ∑' (m : ℕ), F x m

Tactic:
]

Goal state after:
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 : ℝ
hx : x ≥ y
⊢ (f (n + 1) + ∑' (n_1 : ℕ), if n_1 = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) n_1) = f (n + 1) + ∑' (m : ℕ), F x m
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 := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
⊢ y ∈ Ico 0 1

Tactic:
]

Goal state after:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
⊢ y ∈ Ico 0 1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
⊢ bernoulliFun k y = bernoulliFun k y

Tactic:
]

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

Goal state before:
pp: case inr.refine_2
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)
this : B.F = G * H
⊢ ContinuousAt (G * H) 1

Tactic:
]

Goal state after:
case inr.refine_2
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)
this : B.F = G * H
⊢ ContinuousAt (G * H) 1
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
]

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * (fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * (fourier (-↑n)) ↑x
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

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

Tactic:
]

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ B.F ↑(-2) = 0
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
]

Goal state after:
case e'_5.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k / ↑n ^ k = 1 / (-1) ^ k / ↑↑n ^ k
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 = 1

pp: case e'_5.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k ≠ 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) ^ k ≠ 0