mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ cardPowDegree (x - z) < a

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
hyz' : ¬y = z
hxz' : ¬x = z
⊢ cardPowDegree (x - 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
hyz' : ¬y = z
hxz' : x = z
⊢ cardPowDegree (x - z) < a
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
x : R
⊢ (∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = x) →
    x ≠ 0 ∧ ∃ a ∈ Finset.univ, (distinctElems bS adm) a.1 - (distinctElems bS adm) a.2 = x

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
x : R
⊢ (∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = x) →
    x ≠ 0 ∧ ∃ a ∈ Finset.univ, (distinctElems bS adm) a.1 - (distinctElems bS adm) a.2 = x
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.inl
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)
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
⊢ (Rat.padicValuation p)
      (bernoulli (i + 1 + 1) * ↑((2 * k + 1).choose (i + 1 + 1)) * ↑p ^ (2 * k - (i + 1 + 1)) / (2 * ↑k + 1)) ≤
    1

pp: case succ.succ.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)
i : ℕ
hi : i + 1 + 1 < 2 * k
hodd : Odd (i + 2)
⊢ (Rat.padicValuation p)
      (bernoulli (i + 1 + 1) * ↑((2 * k + 1).choose (i + 1 + 1)) * ↑p ^ (2 * k - (i + 1 + 1)) / (2 * ↑k + 1)) ≤
    1

Tactic:
·

Goal state after:
case succ.succ.inl
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)
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
⊢ (Rat.padicValuation p)
      (bernoulli (i + 1 + 1) * ↑((2 * k + 1).choose (i + 1 + 1)) * ↑p ^ (2 * k - (i + 1 + 1)) / (2 * ↑k + 1)) ≤
    1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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)
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
⊢ 0 < m ∧ m < k ∧ i + 2 = 2 * m

Tactic:
by lia

Goal state after:
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
⊢ ↑k ≤ log x / log 2

pp: case refine_3.refine_2
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
⊢ ↑p ≤ x

pp: case refine_3.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
⊢ ↑p ≤ x ^ (↑k)⁻¹

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
⊢ ↑k ≤ log x / log 2
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.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)
i : ℕ
hi : i + 1 + 1 < 2 * k
hodd : Odd (i + 2)
⊢ (Rat.padicValuation p)
      (bernoulli (i + 1 + 1) * ↑((2 * k + 1).choose (i + 1 + 1)) * ↑p ^ (2 * k - (i + 1 + 1)) / (2 * ↑k + 1)) ≤
    1

Tactic:
·

Goal state after:
case succ.succ.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)
i : ℕ
hi : i + 1 + 1 < 2 * k
hodd : Odd (i + 2)
⊢ (Rat.padicValuation p)
      (bernoulli (i + 1 + 1) * ↑((2 * k + 1).choose (i + 1 + 1)) * ↑p ^ (2 * k - (i + 1 + 1)) / (2 * ↑k + 1)) ≤
    1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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)
i : ℕ
hi : i + 1 + 1 < 2 * k
hodd : Odd (i + 2)
⊢ 1 < i + 2

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_3.refine_2
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
⊢ ↑p ≤ x

pp: case refine_3.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
⊢ ↑p ≤ x ^ (↑k)⁻¹

Tactic:
·

Goal state after:
case refine_3.refine_2
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
⊢ ↑p ≤ x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_3.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
⊢ ↑p ≤ x ^ (↑k)⁻¹

Tactic:
·

Goal state after:
case refine_3.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
⊢ ↑p ≤ x ^ (↑k)⁻¹
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ (a : ℕ × ℕ)
    (ha :
      a ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
    (match a with
      | (k, p) => f (p ^ k)) =
      f
        (match a, ha with
        | (k, p), x => p ^ k)

Tactic:
·

Goal state after:
case refine_4
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∀ (a : ℕ × ℕ)
    (ha :
      a ∈
        {x_1 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match x_1 with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊}),
    (match a with
      | (k, p) => f (p ^ k)) =
      f
        (match a, ha with
        | (k, p), x => p ^ k)
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 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match x with
      | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊,
      match x with
      | (k, p) => f (p ^ k)) =
    ∑ 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 ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match x with
      | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊,
      match x with
      | (k, p) => f (p ^ k)) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)
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))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
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
⊢ 1 ≤ N
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case hx
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 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ 0 ≤ ↑(abv b)

pp: case hy
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 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ 0 ≤ ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))

Tactic:
·

Goal state after:
case hx
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 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ 0 ≤ ↑(abv b)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin (n + 1)), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε

Tactic:
·

Goal state after:
case succ
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin (n + 1)), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Chebyshev

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

pp: case neg
x : ℝ
h : 2 ≤ x
⊢ θ x ≤ ψ x

Tactic:
·

Goal state after:
case pos
x : ℝ
h : x < 2
⊢ θ x ≤ ψ x
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case hy
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 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ 0 ≤ ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))

Tactic:
·

Goal state after:
case hy
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 < ε
this✝ : 0 < normBound abv bS
this : 0 ≤ abv b
⊢ 0 ≤ ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx✝ : 1 ≤ x
hx : x < 2
⊢ |ψ x - θ x| ≤ 2 * √x * log x

pp: case neg
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ |ψ x - θ x| ≤ 2 * √x * log x

Tactic:
·

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

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

Tactic:
add_sub_cancel_left

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: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ (1 / ↑x_1)) ≤ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x

pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x ≤ 2 * √x * log x

Tactic:
·

Goal state after:
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ (1 / ↑x_1)) ≤ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x
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
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
have r_eq : ∀ j i, rs j i = μ j * s i % b := fun i j => rfl

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
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
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
Module: Mathlib.NumberTheory.Chebyshev

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

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

Tactic:
·

Goal state after:
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑⌊log x / log 2⌋₊ - ↑1 ≤ ↑⌊log x / log 2⌋₊
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
·

Goal state after:
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑⌊log x / log 2⌋₊ ≤ log x / log 2
Module: Mathlib.NumberTheory.Chebyshev

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

pp: case h₂
x : ℝ
hx : 1 ≤ x
⊢ θ x ≤ log 4 * x

Tactic:
·

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

Goal state before:
pp: case h₂
x : ℝ
hx : 1 ≤ x
⊢ θ x ≤ log 4 * x

Tactic:
·

Goal state after:
case h₂
x : ℝ
hx : 1 ≤ x
⊢ θ x ≤ log 4 * x
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
by
  calc
  _ = ψ x - θ x + θ x := by ring
  _ ≤ 2 * x.sqrt * x.log + log 4 * x := by
    gcongr
    · exact le_trans (le_abs_self _) (abs_psi_sub_theta_le_sqrt_mul_log hx)
    · exact theta_le_log4_mul_x (by linarith)
  _ = _ := by ring

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

pp: case neg
x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ ψ x ≤ (log 4 + 4) * x

Tactic:
·

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

Goal state before:
pp: case pos
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ Λ n - log ↑n = 0

pp: case neg
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
h : ¬Nat.Prime n
⊢ Λ n - 0 = Λ n

Tactic:
·

Goal state after:
case pos
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ Λ n - log ↑n = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
h : ¬Nat.Prime n
⊢ Λ n - 0 = Λ n

Tactic:
·

Goal state after:
case neg
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
h : ¬Nat.Prime n
⊢ Λ n - 0 = Λ n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hbc
x : ℝ
hx : 0 ≤ x
⊢ x - 1 ≤ ↑⌊x⌋₊

pp: case h₁
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ ≤ x

pp: case h₂
x : ℝ
hx : 0 ≤ x
⊢ 1 ≤ 2

Tactic:
·

Goal state after:
case hbc
x : ℝ
hx : 0 ≤ x
⊢ x - 1 ≤ ↑⌊x⌋₊
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h₁
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ ≤ x

pp: case h₂
x : ℝ
hx : 0 ≤ x
⊢ 1 ≤ 2

Tactic:
·

Goal state after:
case h₁
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ ≤ x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h₂
x : ℝ
hx : 0 ≤ x
⊢ 1 ≤ 2

Tactic:
·

Goal state after:
case h₂
x : ℝ
hx : 0 ≤ x
⊢ 1 ≤ 2
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (x - 1) * log 2 - log (x + 2) ≤ ψ x

Tactic:
grw [psi_eq_psi_coe_floor, ← psi_ge]
  gcongr
  · exact (Nat.sub_one_lt_floor x).le
  · exact floor_le hx
  · exact one_le_two

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inl
⊢ ↑0 * log 2 - log (↑0 + 1) - 2 * √↑0 * log ↑0 ≤ θ ↑0

pp: case inr
n : ℕ
hn : n > 0
⊢ ↑n * log 2 - log (↑n + 1) - 2 * √↑n * log ↑n ≤ θ ↑n

Tactic:
·

Goal state after:
case inl
⊢ ↑0 * log 2 - log (↑0 + 1) - 2 * √↑0 * log ↑0 ≤ θ ↑0
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
⊢ θ (x ^ (↑m)⁻¹) ≤ θ (x ^ (↑n)⁻¹)

pp: case inr
x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : 1 < x
⊢ θ (x ^ (↑m)⁻¹) ≤ θ (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
⊢ θ (x ^ (↑m)⁻¹) ≤ θ (x ^ (↑n)⁻¹)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
N : ℕ
hN : N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊
⊢ ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)

Tactic:
simp_rw [psi_eq_sum_theta' this hN, one_div, b, cast_mul, mul_inv_rev, mul_comm,
    ← rpow_mul (by positivity)]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inl
⊢ bernoulli (2 * 0) + ∑ p ∈ range (2 * 0 + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * 0, 1 / ↑p ∈ Set.range Int.cast

pp: case inr
k : ℕ
hk : k > 0
⊢ bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p ∈ Set.range Int.cast

Tactic:
·

Goal state after:
case inl
⊢ bernoulli (2 * 0) + ∑ p ∈ range (2 * 0 + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * 0, 1 / ↑p ∈ Set.range Int.cast
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr
k : ℕ
hk : k > 0
⊢ bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p ∈ Set.range Int.cast

Tactic:
·

Goal state after:
case inr
k : ℕ
hk : k > 0
⊢ bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p ∈ Set.range Int.cast