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

Goal state before:
pp: case convert_2.refine_1
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
hlim : Tendsto (fun n ↦ ↑n ^ (-(s.re - r))) atTop (𝓝 0)
⊢ (fun n ↦ ↑↑n ^ (-s)) =O[atTop] fun n ↦ ↑n ^ (-s.re)

pp: case convert_2.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
hlim : Tendsto (fun n ↦ ↑n ^ (-(s.re - r))) atTop (𝓝 0)
⊢ -s.re + r ≤ -(s.re - r)

Tactic:
·

Goal state after:
case convert_2.refine_1
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
hlim : Tendsto (fun n ↦ ↑n ^ (-(s.re - r))) atTop (𝓝 0)
⊢ (fun n ↦ ↑↑n ^ (-s)) =O[atTop] fun n ↦ ↑n ^ (-s.re)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case convert_2.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
hlim : Tendsto (fun n ↦ ↑n ^ (-(s.re - r))) atTop (𝓝 0)
⊢ -s.re + r ≤ -(s.re - r)

Tactic:
·

Goal state after:
case convert_2.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
hlim : Tendsto (fun n ↦ ↑n ^ (-(s.re - r))) atTop (𝓝 0)
⊢ -s.re + r ≤ -(s.re - r)
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: case neg
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 : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h✝ : ¬(↑b / a).val ≤ p / 2
⊢ (a * -(↑b / a)).valMinAbs.natAbs = b

Tactic:
·

Goal state after:
case neg
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 : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h✝ : ¬(↑b / a).val ≤ p / 2
⊢ (a * -(↑b / a)).valMinAbs.natAbs = b
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case convert_3
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 ↦ deriv (fun x ↦ ↑x ^ (-s)) t * ∑ k ∈ Icc 0 ⌊t⌋₊, f k) =O[atTop] fun x ↦ x ^ ((-s - 1).re + r)

Tactic:
·

Goal state after:
case convert_3
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 ↦ deriv (fun x ↦ ↑x ^ (-s)) t * ∑ k ∈ Icc 0 ⌊t⌋₊, f k) =O[atTop] fun x ↦ x ^ ((-s - 1).re + r)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case convert_3.refine_1
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
⊢ (deriv fun x ↦ ↑x ^ (-s)) =O[atTop] fun t ↦ t ^ (-(s + 1).re)

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:
·

Goal state after:
case convert_3.refine_1
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
⊢ (deriv fun x ↦ ↑x ^ (-s)) =O[atTop] fun t ↦ t ^ (-(s + 1).re)
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:
·

Goal state after:
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
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_1
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
⊢ (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) =O[atTop] fun t ↦ t ^ (-s)

pp: case refine_2
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
⊢ IntegrableAtFilter (fun t ↦ t ^ (-s)) atTop volume

Tactic:
·

Goal state after:
case refine_1
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
⊢ (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) =O[atTop] fun t ↦ t ^ (-s)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
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
⊢ IntegrableAtFilter (fun t ↦ t ^ (-s)) atTop volume

Tactic:
·

Goal state after:
case refine_2
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
⊢ IntegrableAtFilter (fun t ↦ t ^ (-s)) atTop volume
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) →
    IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)

pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R) →
    Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) →
    IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

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

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

Tactic:
·

Goal state after:
case refine_1
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ ∀ᶠ (x : ℝ) in atTop, ‖‖S x‖ * x ^ (-s - 1)‖ ≤ ε * ‖x ^ (-s)‖
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mp.inl
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
hy : 0 < 1
⊢ 0 ≤ x

pp: case mp.inr
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 : y < 1
hy0 : y ≠ 0
⊢ y ≤ x

Tactic:
·

Goal state after:
case mp.inl
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
hy : 0 < 1
⊢ 0 ≤ x
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mp.inr
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 : y < 1
hy0 : y ≠ 0
⊢ y ≤ x

Tactic:
·

Goal state after:
case mp.inr
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 : y < 1
hy0 : y ≠ 0
⊢ y ≤ x
Module: Mathlib.NumberTheory.LSeries.SumCoeff

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

Tactic:
·

Goal state after:
case refine_2
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ IntegrableAtFilter (fun t ↦ t ^ (-s)) atTop volume
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R) →
    Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R) →
    Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
⊢ IsDiscrete R

pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : ¬IsNontrivial R
⊢ IsDiscrete R

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
⊢ IsDiscrete R
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R

pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : ¬DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : ¬DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : ¬DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

Tactic:
·

Goal state after:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

Tactic:
·

Goal state after:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : ¬IsNontrivial R
⊢ IsDiscrete R

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : ¬IsNontrivial R
⊢ IsDiscrete R
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_1
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ioi T) volume

pp: case refine_2
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (fun t ↦ ε * t ^ (-s)) (Set.Ioi T) volume

pp: case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)

Tactic:
·

Goal state after:
case refine_1
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ioi T) volume
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (fun t ↦ ε * t ^ (-s)) (Set.Ioi T) volume

pp: case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)

Tactic:
·

Goal state after:
case refine_2
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (fun t ↦ ε * t ^ (-s)) (Set.Ioi T) volume
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)

Tactic:
·

Goal state after:
case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
ht' : 0 < t
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)

Tactic:
rw [h ht', ← mul_assoc]

Goal state after:
case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
ht' : 0 < t
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t * t ^ (-s - 1)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ J(a | b) ≠ 0

pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0

Tactic:
·

Goal state after:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ J(a | b) ≠ 0
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0

Tactic:
·

Goal state after:
case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : x ∈ I
⊢ x * ϖ ^ n ∈ I * I ^ n

pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : x * ϖ ^ n ∈ I * I ^ n
⊢ x ∈ I

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : x ∈ I
⊢ x * ϖ ^ n ∈ I * I ^ n
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : x * ϖ ^ n ∈ I * I ^ n
⊢ x ∈ I

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : x * ϖ ^ n ∈ I * I ^ n
⊢ x ∈ I
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

pp: case inr
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b ≠ 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
·

Goal state after:
case inl
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case succ.inl
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

pp: case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
·

Goal state after:
case succ.inl
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : x = ϖ * y
⊢ x ∈ I

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
⊢ ϖ ≠ 0

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : x = ϖ * y
⊢ x ∈ I