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

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ (b : ℝ), x₀ ≤ b → LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : max x₀ (max yf yg) ≤ x
⊢ LSeriesSummable f ↑x

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ (b : ℝ), x₀ ≤ b → LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : max x₀ (max yf yg) ≤ x
Hf : LSeriesSummable f ↑x
⊢ LSeriesSummable g ↑x

Tactic:
by

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

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] fun x ↦ LSeries g ↑x
⊢ (fun x ↦ LSeries (f - g) ↑x) =ᶠ[atTop] 0

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] fun x ↦ LSeries g ↑x
n : ℕ
hn : n ≠ 0
⊢ f n = g n

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
⊢ LSeries f = LSeries g ↔ ∀ (n : ℕ), n ≠ 0 → f n = g n

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 + 1) * Real.sin (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
n : ℕ
⊢ ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k

Tactic:
by

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

Goal state before:
pp: ⊢ Set.InjOn LSeries {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}

Tactic:
by

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

Goal state before:
pp: ⊢ 2 ∈ {1}ᶜ

Tactic:
by

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

Goal state before:
pp: ⊢ 1 < Module.rank ℝ ℂ

Tactic:
by

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

Goal state before:
pp: ⊢ riemannZetaZerosᶜ ∈ Filter.codiscreteWithin {1}ᶜ

Tactic:
by

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

Goal state before:
pp: this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
hx : x ≠ 1
⊢ ({1}ᶜ ∩ riemannZetaZeros)ᶜ ⊆ riemannZetaZerosᶜ

Tactic:
by

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

Goal state before:
pp: ⊢ riemannZetaZerosᶜ ∈ Filter.codiscrete ℂ

Tactic:
by

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

Goal state before:
pp: ⊢ IsClosed riemannZetaZeros

Tactic:
by

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

Goal state before:
pp: ⊢ IsDiscrete riemannZetaZeros

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2

Tactic:
by

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

Goal state before:
pp: S : Set ℂ
hS : IsCompact S
⊢ (S ∩ riemannZetaZeros).Finite

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.Complex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ ringChar ℂ ≠ ringChar F

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.Complex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
ch : PrimitiveAddChar F ℂ := primitiveChar F ℂ ⋯
⊢ CyclotomicField ↑ch.n ℂ →* ℂ

Tactic:
exact (IsCyclotomicExtension.algEquiv {(ch.n : ℕ)} ℂ (CyclotomicField ch.n ℂ) ℂ).toMonoidHom

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.Complex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ AddChar F ℂ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.Complex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ (primitiveChar_to_Complex F).IsPrimitive

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ HasSum (fun n ↦ 1 / ↑n ^ (2 * k)) ((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ 2 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ HasSum (fun n ↦ 1 / ↑n ^ 2) (π ^ 2 / 6)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ HasSum (fun n ↦ 1 / ↑n ^ 4) (π ^ 4 / 90)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ 2 * 1 + 1 = 3

Tactic:
by

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

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
⊢ ∃ ξ ∈ Set.Ioc 1 2, (C + C') * (ξ - 1) < (↑q.totient)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ HasSum (fun n ↦ 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)) (π ^ 3 / 32)

Tactic:
by

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

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
⊢ ¬Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n

Tactic:
by

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

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
⊢ {p | Prime p ∧ ↑p = a}.Infinite

Tactic:
by

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

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
n : ℕ
⊢ ∃ p > n, Prime p ∧ ↑p = a

Tactic:
by

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

Goal state before:
pp: n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a ↑q
this : NeZero q
⊢ IsUnit ↑a

Tactic:
by

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

Goal state before:
pp: n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a ↑q
⊢ ∃ p > n, Prime p ∧ ↑p ≡ a [ZMOD ↑q]

Tactic:
by

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

Goal state before:
pp: n q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ IsCoprime ↑a ↑q

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
⊢ ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2

Tactic:
by

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

Goal state before:
pp: n q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ ∃ p > n, Prime p ∧ p ≡ a [MOD q]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
x✝ : ℕ
hx : x✝ ∈ Ico 1 (p / 2).succ
⊢ 1 < 2

Tactic:
by

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

Goal state before:
pp: q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ a [MOD q]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
⊢ ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ (-s).re < 0

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ 0 < s.re - r

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ -(s + 1).re + r ≤ (-s - 1).re + r

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
⊢ ∀ b ∈ Ico 1 (p / 2).succ, ∃ x, ∃ (_ : x ∈ Ico 1 (p / 2).succ), (a * ↑x).valMinAbs.natAbs = b

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
⊢ Multiset.map (fun x ↦ (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val =
    Multiset.map (fun a ↦ a) (Ico 1 (p / 2).succ).val

Tactic:
by

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

Goal state before:
pp: case convert_3.refine_2
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ (fun t ↦ ∑ k ∈ Icc 0 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ r

Tactic:
exact (hO.comp_tendsto tendsto_nat_floor_atTop).trans <|
        isEquivalent_nat_floor.isBigO.rpow hr (eventually_ge_atTop 0)

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑(∏ x ∈ Ico 1 (p / 2).succ, a * ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(∏ x ∈ Ico 1 (p / 2).succ, a * ↑x) = ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).val

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico 1 (p / 2).succ
⊢ ↑(↑a * ↑x✝¹).val = (if (↑a * ↑x✝¹).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x✝¹).valMinAbs.natAbs

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ (fun n ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ∏ x ∈ Ico 1 (p / 2).succ, (if (↑a * ↑x).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
n k : ℕ
hk : k ∈ Icc 1 n
⊢ (if k = 0 then 0 else f k) = f k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ↑(p / 2)!

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ 1 < 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) * ↑(p / 2)!

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
⊢ ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
hp : p ≠ 2
ha0 : ↑a ≠ 0
⊢ legendreSym p a = (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x ∈ Ico 1 (p / 2).succ, a * x) = ↑(∑ x ∈ Ico 1 (p / 2).succ, (a * x % p + p * (a * x / p)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x ∈ Ico 1 (p / 2).succ, (a * x % p + p * (a * x / p))) =
    ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑(a * x)).val) + ↑(∑ x ∈ Ico 1 (p / 2).succ, a * x / p)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑(a * x)).val) =
    ∑ x ∈ Ico 1 (p / 2).succ, ↑((↑a * ↑x).valMinAbs + ↑(if (↑a * ↑x).val ≤ p / 2 then 0 else p))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ∑ x ∈ Ico 1 (p / 2).succ, ↑((↑a * ↑x).valMinAbs + ↑(if (↑a * ↑x).val ≤ p / 2 then 0 else p)) =
    ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑a * ↑x).valMinAbs.natAbs)

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℝ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
hf : ∀ (n : ℕ), 0 ≤ f n
x✝ : ℕ
⊢ ∑ k ∈ Icc 1 x✝, f k = ∑ k ∈ Icc 1 x✝, ‖↑(f k)‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑a * ↑x).valMinAbs.natAbs) =
    ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, x)

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (p % 2 = 1)
a : ℕ
ha2✝ : a % 2 = 1
hap : ↑a ≠ 0
ha2 : ↑a = ↑1
⊢ ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) - ↑(∑ x ∈ Ico 1 (p / 2).succ, x * a / p) = 0

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑(↑n ^ 1)) atTop (𝓝 l)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
⊢ a / b = #(Ico 1 (a / b).succ)

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ (fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
h : x * b ≤ a
⊢ x ≤ a / b

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ {x ∈ Ico 1 c.succ | x * b ≤ a}

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ 1
⊢ 1 + (-s - 1) ≤ -s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p q : ℕ
hp0 : p = 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p = #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p q : ℕ
hp0 : ¬p = 0
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
⊢ x * q / p ≤ p / 2 * q / p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p q : ℕ
hp0 : ¬p = 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, #({x ∈ Ico 1 (q / 2).succ | x * p ≤ a * q}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
x✝ : ℕ × ℕ
fst✝ snd✝ : ℕ
⊢ (fst✝, snd✝) ∈ {x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p} ↔
    (Equiv.prodComm ℕ ℕ) (fst✝, snd✝) ∈ {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p}

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ IntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
⊢ x ≠ 0

Tactic:
by

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

Goal state before:
pp: s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ LocallyIntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
⊢ x < 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
⊢ x.1 ≤ p / 2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : EquivLike.inv e.symm y < 1
hy0 : y ≠ 0
⊢ EquivLike.inv e.symm y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
⊢ 1 < 2

Tactic:
by

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

Goal state before:
pp: s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ IntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : EquivLike.inv e.symm y < 1
hy0 : y ≠ 0
⊢ 1 ≠ 0

Tactic:
by

Goal state after: