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

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑b.natDegree - ↑⌈-log ε / log ↑(Fintype.card Fq)⌉₊ ≤ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq)

Tactic:
]

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑b.natDegree - ↑⌈-log ε / log ↑(Fintype.card Fq)⌉₊ ≤ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero.inr
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hi : 0 + 1 < 2 * k
hp2 : p ≠ 2
⊢ (Rat.padicValuation p) (↑p ^ (2 * k - 1) / 2) ≤ 1

Tactic:
]

Goal state after:
case succ.zero.inr
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hi : 0 + 1 < 2 * k
hp2 : p ≠ 2
⊢ (Rat.padicValuation p) (↑p ^ (2 * k - 1) / 2) ≤ 1
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq) ≤ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq)

Tactic:
]

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

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x = y
⊢ cardPowDegree (y - z) < a

Tactic:
]

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x = y
⊢ cardPowDegree (y - z) < a
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : y = z
⊢ cardPowDegree (x - y) < a

Tactic:
]

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : y = z
⊢ cardPowDegree (x - y) < a
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : x = z
⊢ 0 < a

Tactic:
]

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : x = z
⊢ 0 < a
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ cardPowDegree (x - z) < a

Tactic:
]

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ cardPowDegree (x - z) < a
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
a✝ : 0 < p ^ k
hbx : ↑p ^ k ≤ x
⊢ ∃ a, 0 < a ∧ a ≤ N ∧ ∃ x_1, 0 < x_1 ∧ ↑x_1 ≤ x ∧ Nat.Prime x_1 ∧ ↑x_1 ≤ x ^ (↑a)⁻¹ ∧ x_1 ^ a = p ^ k

Tactic:
]

Goal state after:
case refine_3
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
a✝ : 0 < p ^ k
hbx : ↑p ^ k ≤ x
⊢ ∃ a, 0 < a ∧ a ≤ N ∧ ∃ x_1, 0 < x_1 ∧ ↑x_1 ≤ x ∧ Nat.Prime x_1 ∧ ↑x_1 ≤ x ^ (↑a)⁻¹ ∧ x_1 ^ a = p ^ k
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ ↑(Fintype.card Fq) ^ (x - z).natDegree ≤
    max (↑(Fintype.card Fq) ^ (x - y).natDegree) (↑(Fintype.card Fq) ^ (y - z).natDegree)

Tactic:
]

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ ↑(Fintype.card Fq) ^ (x - z).natDegree ≤
    max (↑(Fintype.card Fq) ^ (x - y).natDegree) (↑(Fintype.card Fq) ^ (y - z).natDegree)
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ ¬(distinctElems bS adm) i = (distinctElems bS adm) j

Tactic:
]

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ ¬(distinctElems bS adm) i = (distinctElems bS adm) j
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
a✝ : 0 < p ^ k
hbx : ↑p ^ k ≤ x
⊢ log (2 ^ k) ≤ log x

Tactic:
]

Goal state after:
case refine_3.refine_1
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
a✝ : 0 < p ^ k
hbx : ↑p ^ k ≤ x
⊢ log (2 ^ k) ≤ log x
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ (x - z).degree ≤ max (x - y).degree (y - z).degree

Tactic:
]

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ (x - z).degree ≤ max (x - y).degree (y - z).degree
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]
⊢ 0 < ↑(cardPowDegree b) * ε

Tactic:
]

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ 0 < ↑(cardPowDegree b) * ε
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : 0 < k
hfilter : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) = ∑ v ∈ range p, ↑v ^ (2 * k)
⊢ ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)

Tactic:
hfilter,

Goal state after:
k p : ℕ
hk : 0 < k
hfilter : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) = ∑ v ∈ range p, ↑v ^ (2 * k)
⊢ ∑ v ∈ range p, ↑v ^ (2 * k) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : 0 < k
hfilter : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) = ∑ v ∈ range p, ↑v ^ (2 * k)
⊢ ∑ x ∈ range (2 * k), bernoulli x * ↑((2 * k + 1).choose x) * ↑p ^ (2 * k + 1 - x) / (↑(2 * k) + 1) +
      bernoulli (2 * k) * ↑(2 * k + 1) * ↑p ^ 1 / (↑(2 * k) + 1) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)

Tactic:
]

Goal state after:
k p : ℕ
hk : 0 < k
hfilter : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) = ∑ v ∈ range p, ↑v ^ (2 * k)
⊢ ∑ x ∈ range (2 * k), bernoulli x * ↑((2 * k + 1).choose x) * ↑p ^ (2 * k + 1 - x) / (↑(2 * k) + 1) +
      bernoulli (2 * k) * ↑(2 * k + 1) * ↑p ^ 1 / (↑(2 * k) + 1) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
inst✝ : Fact (Nat.Prime p)
hp_ne : ↑p ≠ 0
⊢ ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) / ↑p =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
]

Goal state after:
k p : ℕ
inst✝ : Fact (Nat.Prime p)
hp_ne : ↑p ≠ 0
⊢ ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) / ↑p =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ x_1 ∈ Icc 1 N,
      ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (x_1, y) with
            | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊ then
          match (x_1, y) with
          | (k, p) => f (p ^ k)
        else 0) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ x_1 ∈ Icc 1 N,
      ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (x_1, y) with
            | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊ then
          match (x_1, y) with
          | (k, p) => f (p ^ k)
        else 0) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
inst✝ : Fact (Nat.Prime p)
hp_ne : ↑p ≠ 0
i : ℕ
hi : i ∈ range (2 * k)
this : i < 2 * k
⊢ bernoulli i * ↑((2 * k + 1).choose i) * (↑p ^ (2 * k - i) * ↑p) / (2 * ↑k + 1) / ↑p =
    bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
]

Goal state after:
k p : ℕ
inst✝ : Fact (Nat.Prime p)
hp_ne : ↑p ≠ 0
i : ℕ
hi : i ∈ range (2 * k)
this : i < 2 * k
⊢ bernoulli i * ↑((2 * k + 1).choose i) * (↑p ^ (2 * k - i) * ↑p) / (2 * ↑k + 1) / ↑p =
    bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case e_s
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k p : ℕ
x✝ : 1 ≤ k ∧ k ≤ N
h : (0 < p ∧ p ≤ ⌊x ^ (↑k)⁻¹⌋₊) ∧ Nat.Prime p
⊢ ⌊?m.473⌋₊ ≤ ⌊x⌋₊

pp: case hab
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k p : ℕ
x✝ : 1 ≤ k ∧ k ≤ N
h : (0 < p ∧ p ≤ ⌊x ^ (↑k)⁻¹⌋₊) ∧ Nat.Prime p
⊢ x ^ (↑k)⁻¹ ≤ ?m.473

pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k p : ℕ
x✝ : 1 ≤ k ∧ k ≤ N
h : (0 < p ∧ p ≤ ⌊x ^ (↑k)⁻¹⌋₊) ∧ Nat.Prime p
⊢ ℝ

Tactic:
]

Goal state after:
case hab
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k p : ℕ
x✝ : 1 ≤ k ∧ k ≤ N
h : (0 < p ∧ p ≤ ⌊x ^ (↑k)⁻¹⌋₊) ∧ Nat.Prime p
⊢ x ^ (↑k)⁻¹ ≤ x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
x✝² : ℕ
hk : x✝² ∈ Icc 1 N
x✝¹ : ℕ
x✝ : x✝¹ ∈ {p ∈ Ioc 0 ⌊x ^ (1 / ↑x✝²)⌋₊ | Nat.Prime p}
⊢ log ↑x✝¹ = log ↑x✝¹

pp: x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
x✝² : ℕ
hk : x✝² ∈ Icc 1 N
x✝¹ : ℕ
x✝ : x✝¹ ∈ {p ∈ Ioc 0 ⌊x ^ (1 / ↑x✝²)⌋₊ | Nat.Prime p}
⊢ Nat.Prime x✝¹

Tactic:
]

Goal state after:
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
x✝² : ℕ
hk : x✝² ∈ Icc 1 N
x✝¹ : ℕ
x✝ : x✝¹ ∈ {p ∈ Ioc 0 ⌊x ^ (1 / ↑x✝²)⌋₊ | Nat.Prime p}
⊢ Nat.Prime x✝¹
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ θ (x ^ (1 / ↑1)) + ∑ x_1 ∈ Ioc 1 N, θ (x ^ (1 / ↑x_1)) = θ x + ∑ n ∈ Icc 2 N, θ (x ^ (1 / ↑n))

pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 1 ≤ N

Tactic:
]

Goal state after:
x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ θ (x ^ (1 / ↑1)) + ∑ x_1 ∈ Ioc 1 N, θ (x ^ (1 / ↑x_1)) = θ x + ∑ n ∈ Icc 2 N, θ (x ^ (1 / ↑n))

x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 1 ≤ N
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ log 2 ≤ log x

Tactic:
]

Goal state after:
x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ log 2 ≤ log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
h : x < 2
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
h : 2 ≤ x
⊢ θ x ≤ θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ (1 / ↑n))

Tactic:
]

Goal state after:
case neg
x : ℝ
h : 2 ≤ x
⊢ θ x ≤ θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ (1 / ↑n))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx✝ : 1 ≤ x
hx : x < 2
⊢ 0 ≤ 2 * √x * log x

Tactic:
]

Goal state after:
case pos
x : ℝ
hx✝ : 1 ≤ x
hx : x < 2
⊢ 0 ≤ 2 * √x * log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ |∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ (1 / ↑n))| ≤ 2 * √x * log x

Tactic:
]

Goal state after:
case neg
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ |∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ (1 / ↑n))| ≤ 2 * √x * log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ log 4 * x ^ (1 / ↑i) ≤ log 4 * x ^ (1 / 2)

Tactic:
]

Goal state after:
case h
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ log 4 * x ^ (1 / ↑i) ≤ log 4 * x ^ (1 / 2)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑⌊log x / log 2⌋₊ - ↑1 ≤ log x / log 2

pp: case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ 1 ≤ ⌊log x / log 2⌋₊

Tactic:
]

Goal state after:
case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑⌊log x / log 2⌋₊ - ↑1 ≤ log x / log 2

case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ 1 ≤ ⌊log x / log 2⌋₊
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case e_a.e_a
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑2 * log 2 / log 2 = 2

Tactic:
]

Goal state after:
case e_a.e_a
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑2 * log 2 / log 2 = 2
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
i : ι
j : Fin (cardM bS adm).succ
⊢ μ j * s i = μ j * s i

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ψ x = ψ x - θ x + θ x

Tactic:
by ring

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 2 * √x * log x + log 4 * x = log 4 * x + 2 * √x * log x

Tactic:
by ring

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx✝ : 0 ≤ x
hx : x < 1
⊢ 0 ≤ (log 4 + 4) * x

Tactic:
]

Goal state after:
case pos
x : ℝ
hx✝ : 0 ≤ x
hx : x < 1
⊢ 0 ≤ (log 4 + 4) * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ log 4 * x + 2 * √x * log x ≤ log 4 * x + 4 * x

Tactic:
]

Goal state after:
case neg
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ log 4 * x + 2 * √x * log x ≤ log 4 * x + 4 * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x ^ (1 / 2) * x ^ (1 / 2) * (1 / (1 / 2)) ≤ 4 * x

Tactic:
]

Goal state after:
case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x ^ (1 / 2) * x ^ (1 / 2) * (1 / (1 / 2)) ≤ 4 * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * (x ^ (1 / 2) * x ^ (1 / 2)) * (1 / (1 / 2)) ≤ 4 * x

Tactic:
]

Goal state after:
case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * (x ^ (1 / 2) * x ^ (1 / 2)) * (1 / (1 / 2)) ≤ 4 * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x ^ (1 / 2 + 1 / 2) * (1 / (1 / 2)) ≤ 4 * x

Tactic:
]

Goal state after:
case h₂
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x ^ (1 / 2 + 1 / 2) * (1 / (1 / 2)) ≤ 4 * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ∑ x ∈ Ioc 0 ⌊x⌋₊, (Λ x - if Nat.Prime x then log ↑x else 0) = ∑ a ∈ Ioc 0 ⌊x⌋₊, if ¬Nat.Prime a then Λ a else 0

Tactic:
]

Goal state after:
x : ℝ
⊢ ∑ x ∈ Ioc 0 ⌊x⌋₊, (Λ x - if Nat.Prime x then log ↑x else 0) = ∑ a ∈ Ioc 0 ⌊x⌋₊, if ¬Nat.Prime a then Λ a else 0
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
j : Fin (cardM bS adm).succ
⊢ μ j • ∑ i, (bS.repr a) i • bS i = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
j : Fin (cardM bS adm).succ
⊢ μ j • ∑ i, (bS.repr a) i • bS i = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ log (2 ^ n) ≤ log ((↑n + 1) * ↑n.lcmUpto)

Tactic:
]

Goal state after:
n : ℕ
⊢ log (2 ^ n) ≤ log ((↑n + 1) * ↑n.lcmUpto)
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
]

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ (x - 1) * log 2 - log (x + 2) ≤ ↑⌊x⌋₊ * log 2 - log (↑⌊x⌋₊ + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x ≤ |ψ x - θ x|

Tactic:
]

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x ≤ |ψ x - θ x|
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
hT : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T
hp_ne : ↑p ≠ 0
hAlg :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p
⊢ ↑T - (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
]

Goal state after:
case h
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
hT : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T
hp_ne : ↑p ≠ 0
hAlg :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p
⊢ ↑T - (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ψ x - 2 * √x * log x ≤ θ x

Tactic:
]

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ ψ x - 2 * √x * log x ≤ θ x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inl
x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : x ≤ 1
⊢ 0 ≤ θ (x ^ (↑n)⁻¹)

Tactic:
]

Goal state after:
case inl
x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : x ≤ 1
⊢ 0 ≤ θ (x ^ (↑n)⁻¹)