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

Goal state before:
pp: N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n ↦ χ ↑n) s
h : s.re ≤ 1
⊢ s.re ≤ re 1

Tactic:
by

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

Goal state before:
pp: N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
⊢ LSeriesSummable (fun n ↦ χ ↑n) s ↔ 1 < s.re

Tactic:
by

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

Goal state before:
pp: N : ℕ
hn : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ (abscissaOfAbsConv fun n ↦ χ ↑n) = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: r : ℝ
h : ¬r < -1
H : Summable fun p ↦ ↑↑p ^ r
x✝ : Primes
⊢ 0 ≤ 1 / ↑↑x✝

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ LSeriesSummable ((fun n ↦ χ ↑n) * f) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: r : ℝ
h : ¬r < -1
H : Summable fun p ↦ ↑↑p ^ r
p : Primes
⊢ 1 ≤ ↑↑p

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ χ ↑n) s * L ((fun n ↦ χ ↑n) * fun n ↦ ↑(μ n)) s = 1

Tactic:
by

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : L (fun n ↦ χ ↑n) s = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: r : ℝ
⊢ (Summable fun p ↦ ↑↑p ^ r) ↔ r < -1

Tactic:
by

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

Goal state before:
pp: ⊢ (L fun n ↦ ↑(ζ n)) = L 1

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
⊢ ↑(ζ n✝) = 1 n✝

Tactic:
by

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

Goal state before:
pp: ⊢ (abscissaOfAbsConv fun n ↦ ↑(ζ n)) = 1

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : ∑' (n : ℕ), term (fun n ↦ if n = 0 then 0 else 1) s n = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ L (fun n ↦ ↑(ζ n)) s = riemannZeta s

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(ζ n)) s = riemannZeta s

Tactic:
by

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
    ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(ζ n)) s * L (fun n ↦ ↑(μ n)) s = 1

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
h : L (fun n ↦ ↑(ζ n)) s = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 1 < (↑x).re

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 1 < x
hx' : 1 < (↑x).re
x✝ : ℕ
⊢ 0 x✝ ≤ 1 x✝

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 1 < x
hx' : 1 < (↑x).re
⊢ 0 < 1 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 1 < x
hx' : 1 < (↑x).re
⊢ 1 < ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 0 < riemannZeta ↑x

Tactic:
by

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

Goal state before:
pp: ⊢ ((fun n ↦ ↑(Λ n)) ⍟ fun n ↦ ↑(ζ n)) = fun n ↦ Complex.log ↑n

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
hf : Summable fun x ↦ ‖term (logMul 1) s x‖
n : ℕ
⊢ ‖(fun n ↦ ↑(Λ n)) n‖ ≤ ‖Complex.log ↑n‖

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
hf : Summable fun x ↦ ‖term (logMul 1) s x‖
n : ℕ
hΛ : ‖(fun n ↦ ↑(Λ n)) n‖ ≤ ‖Complex.log ↑n‖
⊢ ‖Complex.log ↑n‖ ≤ ‖logMul 1 n‖

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (fun n ↦ ↑(Λ n)) s

Tactic:
by

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ 2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)) (sinKernel (↑a) t)

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
⊢ (((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) ⍟ fun n ↦ χ ↑n) = (fun n ↦ χ ↑n) * fun n ↦ Complex.log ↑n

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ oddKernel a =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
⊢ (abscissaOfAbsConv fun n ↦ χ ↑n) < ↑s.re

Tactic:
by

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ s.Gammaℝ / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s)

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
hs' : (abscissaOfAbsConv fun n ↦ χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s
n✝ : ℕ
x✝ : n✝ ≠ 0
⊢ ((fun n ↦ χ ↑n) * fun n ↦ Complex.log ↑n) n✝ = logMul (fun n ↦ χ ↑n) n✝

Tactic:
by

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

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
⊢ Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))

Tactic:
by

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(Λ n)) s = -deriv (L 1) s / L 1 s

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : deriv (L 1) s = deriv riemannZeta s
⊢ L (fun n ↦ ↑(Λ n)) s = -deriv riemannZeta s / riemannZeta s

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(Λ n)) s = -deriv riemannZeta s / riemannZeta s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: x✝⁵ x✝⁴ x✝³ : ℕ
x✝² : x✝⁵ ≠ 0
x✝¹ : x✝⁴ ≠ 0
x✝ : x✝³ ≠ 0
⊢ x✝⁵ ^ 0 + x✝⁴ ^ 0 ≠ x✝³ ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: h : FermatLastTheoremFor 1
⊢ 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: h : FermatLastTheoremFor 1
⊢ 2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: h : FermatLastTheoremFor 1
⊢ 1 ^ 1 + 1 ^ 1 = 2 ^ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: h : FermatLastTheoremFor 2
⊢ 3 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: h : FermatLastTheoremFor 2
⊢ 4 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: h : FermatLastTheoremFor 2
⊢ 5 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: h : FermatLastTheoremFor 2
⊢ 3 ^ 2 + 4 ^ 2 = 5 ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremWith R m
⊢ FermatLastTheoremWith R n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremFor m
⊢ FermatLastTheoremFor n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ a.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ b.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ c.natAbs ≠ 0

Tactic:
by

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

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
x : ℂ
⊢ x = 1 / x⁻¹

Tactic:
by

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

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ a.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ b.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ c.natAbs ≠ 0

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ sinKernel a =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
⊢ 0 < 3 / 2

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
x : ℝ
hx : x ∈ Ioi 0
⊢ (ofReal ∘ oddKernel a) (1 / x) = (1 * ↑(x ^ (3 / 2))) • (ofReal ∘ sinKernel a) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : 0 < c
⊢ 0 < c ^ n

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
⊢ hurwitzZetaEven a s = completedHurwitzZetaEven a s / s.Gammaℝ

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven (-a) s = hurwitzZetaEven a s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
⊢ b.natAbs ≠ 0

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ -2 * (↑n + 1) = -(2 * ↑(n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
⊢ c.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
⊢ a.natAbs ≠ 0

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
n : ℕ
⊢ hurwitzZetaEven a (-2 * (↑n + 1)) = 0

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
r : ℝ
⊢ (fun x ↦ (ofReal ∘ oddKernel a) x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
⊢ a.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
⊢ c.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
⊢ b.natAbs ≠ 0

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
⊢ c.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
⊢ a.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
⊢ b.natAbs ≠ 0

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
r : ℝ
⊢ (fun x ↦ (ofReal ∘ sinKernel a) x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd (-a) s = -completedHurwitzZetaOdd a s

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedSinZeta (-a) s = -completedSinZeta a s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ c.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ b.natAbs ≠ 0

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ a.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : c < 0
⊢ 0 < a ^ n + b ^ n

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = ↑(3 / 2) - (s + 1) / 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ b.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ c.natAbs ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ False

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
this : DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ a.num * ↑b.den * ↑c.den ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ ↑a.den * b.num * ↑c.den ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ ↑a.den * ↑b.den * c.num ≠ 0

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedSinZeta a (1 - s) = completedHurwitzZetaOdd a s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
this : (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0
⊢ ↑a.den ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
this : (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0
⊢ ↑b.den ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
this : (↑a.den * ↑b.den * ↑c.den) ^ n ≠ 0
⊢ ↑c.den ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ False

Tactic:
by

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = ↑(2 * π * a * ↑n) * I

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Tactic:
by

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

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZetaEven a 1))

Tactic:
by

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

Goal state before:
pp: a b : UnitAddCircle
⊢ Differentiable ℂ fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
by

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun i ↦ s.Gammaℝ / ↑|↑i + a| ^ s / 2 / s.Gammaℝ) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)
n : ℤ
⊢ 1 / ↑|↑n + a| ^ s / 2 = s.Gammaℝ / ↑|↑n + a| ^ s / 2 / s.Gammaℝ

Tactic:
by

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ ‖c n‖ = 1 / 2

Tactic:
by

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ 1 / ↑|↑n + a| ^ s / 2) (hurwitzZetaEven (↑a) s)

Tactic:
by

Goal state after: