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

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ θ x = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Monotone x.appr

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
⊢ x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
this : x ≠ 0
⊢ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
⊢ IntervalIntegrable (fun x ↦ 1 / log x ^ 2) volume a b

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ IntervalIntegrable (fun x ↦ 1 / log a ^ 2) volume a b

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁸ : EuclideanDomain R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra R K
inst✝¹² : IsFractionRing R K
inst✝¹¹ : Algebra K L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁸ : IsScalarTower R K L
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : Ideal S
⊢ Ideal.span {(algebraMap R S) (∏ m ∈ finsetApprox bS adm, m)} ≤ I ↔
    (algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) ∈ (Equiv.refl (Ideal S)) I

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
x✝ : x ∈ Set.Icc a b
left✝ : a ≤ x
right✝ : x ≤ b
⊢ 1 / log x ^ 2 ≤ 1 / log a ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ ∫ (x : ℝ) in a..b, 1 / log x ^ 2 ≤ ∫ (x : ℝ) in a..b, 1 / log a ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ ∫ (x : ℝ) in a..b, 1 / log a ^ 2 ≤ (b - a) / log a ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ ∫ (x : ℝ) in a..b, 1 / log x ^ 2 ≤ (b - a) / log a ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ 2 ^ 2 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝¹ : DecidableEq L := Classical.decEq L
this✝ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b x)
⊢ LinearIndependent R ⇑((Algebra.traceForm K L).dualBasis ⋯ b)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
⊢ 0 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
⊢ x ≤ x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
h : m ≤ n
⊢ p ^ m ∣ x.appr n - x.appr m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 1 < √x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 0 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
⊢ c ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝² : DecidableEq L := Classical.decEq L
this✝¹ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this✝ : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
s : Finset L
b✝ : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b✝ x)
this : LinearIndependent R ⇑((Algebra.traceForm K L).dualBasis ⋯ b✝)
n : ℕ
b : Basis (Fin n) R ↥(↑R (Algebra.linearMap S L)).range
⊢ (S ⧸ (↑R (Algebra.linearMap S L)).ker) ≃ₗ[R] S

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
⊢ Fintype (ClassGroup S)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
⊢ ∃ m, ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ m)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
⊢ ∃ m, ∀ t ∈ rootsOfUnity n L, g ↑t = ↑(t ^ m)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
⊢ ⋯.unit = ⋯.unit ^ p ^ i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ 0 < 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ discr A b = discr A (⇑f ∘ b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A (⇑b ∘ ⇑f.symm) = discr A ⇑b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
⊢ ∀ (j : ι), (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ Real.sqrt =o[atTop] fun x ↦ x / log x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i : ι
hi : g i ≠ 0
⊢ traceMatrix A b *ᵥ g = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ 2 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
⊢ discr A b = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
this : c = ↑(unitCoeff h)
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h)).cast

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
⊢ IsUnit c

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ discr A (b ᵥ* P.map ⇑(algebraMap A B)) = P.det ^ 2 * discr A b

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ 2 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
u : ℝ
x✝ : u ∈ Set.Icc 2 x
⊢ 0 ≤ 1 / log u ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, log 4 * (1 / log x ^ 2) = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2|

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ discr A (P.map ⇑(algebraMap A B) *ᵥ b) = P.det ^ 2 * discr A b

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ i) * ↑(p ^ k) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ ↑(p ^ i) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ 0 ≤ θ t / (t * log t ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℤ_[p]), x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ 0 ≤ t

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
inst✝ : Algebra.IsSeparable K L
b : Basis ι K L
⊢ discr K ⇑b ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ θ t / (t * log t ^ 2) ≤ log 4 * t / (t * log t ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ θ t / (t * log t ^ 2) ≤ log 4 * t / (t * log t ^ 2)

Tactic:
by grw [theta_le_log4_mul_x (by linarith)]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]), x - ↑(x.appr n) ∈ Ideal.span {↑(p ^ n)}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ log 4 * t / (t * log t ^ 2) = log 4 * (1 / log t ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ ∀ᶠ (x : ℝ) in atTop, x / log x = 0 → x / log x ^ 2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
i k : ℕ
hi : k ≤ i
⊢ ↑p ^ k ∣ aux g (p ^ i) - aux g (p ^ k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)) =o[atTop] fun x ↦ x / log x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ x / log x ^ 2) =ᶠ[atTop] fun x ↦ x / log x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑(p ^ n)} → x - ↑b ∈ Ideal.span {↑(p ^ n)} → ↑a = ↑b

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ ↑(π ⌊x⌋₊) - θ x / log x) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
this : x.appr n = 0
⊢ x ∈ Ideal.span {↑p ^ n}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ g ↑↑t = ↑(↑t ^ (χ₀ n g).val)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
inst✝ : Algebra.IsSeparable K L
e : ι ≃ (L →ₐ[K] E)
⊢ (algebraMap K E) (discr K b) = (embeddingsMatrixReindex K E b e).det ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Nat.card ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : g ↑↑ζ = ↑(↑ζ ^ c.val)
this : ↑(↑ζ ^ c.val) = ↑(↑ζ ^ (χ₀ n g).val)
⊢ ζ ^ c.val = ζ ^ (χ₀ n g).val

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Nat.card ↥(rootsOfUnity n L))
hc : ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)
⊢ c = χ₀ n g

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.ker (toZModPow n) = Ideal.span {↑p ^ n}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
⊢ χ₀ n (RingEquiv.refl L) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ (algebraMap K E) (discr K ⇑pb.basis) = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
this : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
⊢ 0 ≤ log x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ (algebraMap K E) (discr K ⇑pb.basis) = ∏ i, ∏ j > i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n) = toZModPow m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
⊢ χ₀ n (g * h) = χ₀ n g * χ₀ n h

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ g ↑t = ↑t ^ (↑((modularCyclotomicCharacter L hn) g)).val

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((toZModPow n) x).cast = (toZModPow m) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
this✝ : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * x / log x
this : 0 ≤ log x
⊢ 0 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ g ↑t = ↑t ^ ((ZMod.ringEquivCongr ⋯) c).val

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
⊢ c = ↑((modularCyclotomicCharacter L hn) g)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℝ) in atTop, ↑(π ⌊x⌋₊) ≤ (log 4 + ε) * x / log x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ (autToPow R hμ) g = (modularCyclotomicCharacter L ⋯) g.toRingEquiv

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ DenseRange Nat.cast

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
g : L ≃+* L
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ (PadicInt.toZModPow n) (χ p g) = ↑((modularCyclotomicCharacter L ⋯) g)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ (↑n * log 2 - log (↑n + 1)) / log ↑n ≤ ↑(π n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
g : L ≃+* L
n : ℕ
t : ↥(rootsOfUnity (p ^ n) L)
⊢ g ↑↑t = ↑↑t ^ ((PadicInt.toZModPow n) (χ p g)).val

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ ((x - 1) * log 2 - log (x + 2)) / log x ≤ ↑(π ⌊x⌋₊)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ DenseRange Int.cast

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x ≤ ↑(π ⌊x⌋₊) * log x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ↑(π ⌊x⌋₊) * log √x = ∑ p ∈ ⌊x⌋₊.primesLE, log √x

Tactic:
by

Goal state after: