awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
hn : n ≠ 0
inr : ∀ (p : ℕ) (hp : p ∈ n.primesLE), (↑(Nat.log p n) : ℝ) * log (↑p : ℝ) ≤ log (↑n : ℝ)
⊢ LE.le (α := ℝ) (∑ p ∈ n.primesLE, (↑(Nat.log p n) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ n.primesLE, log (↑n : ℝ))

Tactic:
gcongr with p hp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.primesLE
⊢ (↑(Nat.log p n) : ℝ) * log (↑p : ℝ) ≤ log (↑n : ℝ)

Tactic:
le_log_of_pow_le (mod_cast (prime_of_mem_primesLE hp).pos) ?_

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.Prime.pos, Real.le_log_of_pow_le, Nat.cast, Nat.prime_of_mem_primesLE, LT.lt, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.primesLE
inr : HPow.hPow (α := ℝ) (↑p : ℝ) (Nat.log p n) ≤ (↑n : ℝ)
⊢ (↑(Nat.log p n) : ℝ) * log (↑p : ℝ) ≤ log (↑n : ℝ)

Tactic:
refine le_log_of_pow_le (mod_cast (prime_of_mem_primesLE hp).pos) ?_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.primesLE
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (Nat.log p n) ≤ (↑n : ℝ)

Tactic:
exact_mod_cast pow_log_le_self p hn

Premises used: Nat.pow_log_le_self
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
grw : (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
⊢ ψ x ≤ (↑(π ⌊x⌋₊) : ℝ) * log x

Tactic:
grw [psi_eq_psi_coe_floor, psi_le_primeCounting_mul_log]

Premises used: Chebyshev.psi_eq_psi_coe_floor, Chebyshev.psi_le_primeCounting_mul_log
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
inl : ∀ (h : x < 1), (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
inr : ∀ (h : 1 ≤ x), (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
⊢ (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x

Tactic:
rcases lt_or_ge x 1 with h | h

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : x < 1
⊢ (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x

Tactic:
simp [floor_eq_zero.mpr h]

Premises used: Iff.mpr, Nat.floor_eq_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 ≤ x
inr : LT.lt (α := ℝ) 0 (↑⌊x⌋₊ : ℝ)
inr₁ : (↑⌊x⌋₊ : ℝ) ≤ x
⊢ (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 ≤ x
⊢ LT.lt (α := ℝ) 0 (↑⌊x⌋₊ : ℝ)

Tactic:
exact_mod_cast lt_of_add_one_le <| (one_le_floor_iff x).mpr h

Premises used: Iff.mpr, Nat.one_le_floor_iff, Nat.lt_of_add_one_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 ≤ x
⊢ 0 ≤ x

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 1 ≤ x
⊢ (↑⌊x⌋₊ : ℝ) ≤ x

Tactic:
exact floor_le (by positivity)

Premises used: Nat.floor_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ ∀ x ∈ n.primesLE, Ne (α := ℝ) (↑(x ^ Nat.log x n) : ℝ) 0

Tactic:
simp +contextual
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
rw : ψ (↑n : ℝ) = ∑ i ∈ n.primesLE, log (↑(i ^ Nat.log i n) : ℝ)
⊢ ψ (↑n : ℝ) = log (↑n.lcmUpto : ℝ)

Tactic:
rw [lcmUpto_eq_prod_pow_log, cast_prod, log_prod (by simp +contextual)]

Premises used: Real.log_prod, Nat.cast_prod, Nat.lcmUpto_eq_prod_pow_log
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ ψ (↑n : ℝ) = ∑ i ∈ n.primesLE, log (↑(i ^ Nat.log i n) : ℝ)

Tactic:
simp [psi_eq_sum_mul_log_prime]

Premises used: Chebyshev.psi_eq_sum_mul_log_prime
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n k : ℕ
hkn : k ≤ n
rw :
  ∀ (p : ℕ),
    Nat.Prime p →
      LE.le (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ n.choose k ∣ n.lcmUpto

Tactic:
rw [← factorization_prime_le_iff_dvd (choose_ne_zero hkn) (lcmUpto_ne_zero n)]

Premises used: Nat.lcmUpto_ne_zero, Nat.choose_ne_zero, Nat.factorization_prime_le_iff_dvd
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : Nat.Prime p
rw : ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ Nat.log p n
⊢ LE.le (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [factorization_lcmUpto n hp]

Premises used: Nat.factorization_lcmUpto
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : Nat.Prime p
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ Nat.log p n

Tactic:
factorization_choose_le_log

Premises used: Nat.factorization_choose_le_log
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : Nat.Prime p
⊢ ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ Nat.log p n

Tactic:
exact factorization_choose_le_log

Premises used: Nat.factorization_choose_le_log
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
h : ∀ (k : ℕ) (hk : k ∈ range (n + 1)), n.choose k ≤ n.lcmUpto
⊢ LE.le (α := ℕ) (∑ m ∈ range (n + 1), n.choose m) (∑ k ∈ range (n + 1), n.lcmUpto)

Tactic:
gcongr with k hk
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n k : ℕ
hk : k ∈ range (n + 1)
⊢ k ≤ n

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n k : ℕ
hk : k ∈ range (n + 1)
⊢ n.choose k ≤ n.lcmUpto

Tactic:
exact le_of_dvd (lcmUpto_pos n) (choose_dvd_lcmUpto <| by grind)

Premises used: Nat.lcmUpto_pos, Chebyshev.choose_dvd_lcmUpto, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ ∑ k ∈ range (n + 1), n.lcmUpto = (n + 1) * n.lcmUpto

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
trans :
  Eq.{u_1 + 1} (α := R) (∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n)
    (∑ x ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match (motive := ℕ × ℕ → Prop) x with
      | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊,
      match (motive := ℕ × ℕ → R) x with
      | (k, p) => f (p ^ k))
trans₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ x ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match (motive := ℕ × ℕ → Prop) x with
      | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊,
      match (motive := ℕ × ℕ → R) x with
      | (k, p) => f (p ^ k))
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))
⊢ Eq.{u_1 + 1} (α := R) (∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))

Tactic:
trans ∑ ⟨k, p⟩ ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ (Ioc 0 ⌊x⌋₊).filter Nat.Prime
    with p ≤ ⌊x ^ (k : ℝ)⁻¹⌋₊, f (p ^ k)

Premises used: Nat.Prime, HDiv.hDiv, Finset.Icc, Real.log, Nat.floor, OfNat.ofNat, Finset.filter, Finset.Ioc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
⊢ Eq.{u_1 + 1} (α := R) (∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n)
    (∑ x ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match (motive := ℕ × ℕ → Prop) x with
      | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊,
      match (motive := ℕ × ℕ → R) x with
      | (k, p) => f (p ^ k))

Tactic:
(sum_bij (i := fun ⟨k, p⟩ _ ↦ p ^ k) ?_ ?_ ?_ ?_).symm

Premises used: Finset.sum_bij, Eq.symm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
⊢ ∀ (a : ℕ × ℕ)
    (ha :
      a ∈
        {x_1 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match (motive := ℕ × ℕ → Prop) x_1 with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}),
    (fun (x_1 : ℕ × ℕ)
            (x_2 :
              x_1 ∈
                {x_2 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                  match (motive := ℕ × ℕ → Prop) x_2 with
                  | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}) ↦
          (match (motive :=
              (x_3 : ℕ × ℕ) →
                x_3 ∈
                    {x_4 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                      match (motive := ℕ × ℕ → Prop) x_4 with
                      | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} →
                  ℕ)
              x_1, x_2 with
            | (k, p), x => p ^ k :
            ℕ))
        a ha ∈
      {n ∈ Ioc 0 ⌊x⌋₊ | IsPrimePow n}

Tactic:
simp +contextual [hx, rpow_nonneg, le_floor_iff, ← pos_iff_ne_zero, Prime.isPrimePow,
        one_le_iff_ne_zero, le_rpow_inv_iff_of_pos, isPrimePow_pow_iff, prime_iff]

Premises used: Nat.prime_iff, Nat.le_floor_iff, Real.le_rpow_inv_iff_of_pos, Prime.isPrimePow, Nat.one_le_iff_ne_zero, Real.rpow_nonneg, isPrimePow_pow_iff, pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
refine_2 :
  ∀ (a b : ℕ),
    a ≠ 0 →
      a ≤ ⌊log x / log 2⌋₊ →
        b ≠ 0 →
          (↑b : ℝ) ≤ x →
            Nat.Prime b →
              (↑b : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ →
                ∀ (a_7 b_1 : ℕ),
                  a_7 ≠ 0 →
                    a_7 ≤ ⌊log x / log 2⌋₊ →
                      b_1 ≠ 0 →
                        (↑b_1 : ℝ) ≤ x →
                          Nat.Prime b_1 →
                            (↑b_1 : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a_7 : ℝ)⁻¹ → b ^ a = b_1 ^ a_7 → a = a_7 ∧ b = b_1
⊢ ∀ (a₁ : ℕ × ℕ)
    (ha₁ :
      a₁ ∈
        {x_1 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match (motive := ℕ × ℕ → Prop) x_1 with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊})
    (a₂ : ℕ × ℕ)
    (ha₂ :
      a₂ ∈
        {x_1 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match (motive := ℕ × ℕ → Prop) x_1 with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}),
    Eq (α := ℕ)
        ((fun (x_1 : ℕ × ℕ)
              (x_2 :
                x_1 ∈
                  {x_2 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                    match (motive := ℕ × ℕ → Prop) x_2 with
                    | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}) ↦
            (match (motive :=
                (x_3 : ℕ × ℕ) →
                  x_3 ∈
                      {x_4 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                        match (motive := ℕ × ℕ → Prop) x_4 with
                        | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} →
                    ℕ)
                x_1, x_2 with
              | (k, p), x => p ^ k :
              ℕ))
          a₁ ha₁)
        ((fun (x_1 : ℕ × ℕ)
              (x_2 :
                x_1 ∈
                  {x_2 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                    match (motive := ℕ × ℕ → Prop) x_2 with
                    | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}) ↦
            (match (motive :=
                (x_3 : ℕ × ℕ) →
                  x_3 ∈
                      {x_4 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                        match (motive := ℕ × ℕ → Prop) x_4 with
                        | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} →
                    ℕ)
                x_1, x_2 with
              | (k, p), x => p ^ k :
              ℕ))
          a₂ ha₂) →
      a₁ = a₂

Tactic:
simp +contextual only [hx, rpow_nonneg, le_floor_iff, mem_filter, mem_product, mem_Icc,
        one_le_iff_ne_zero, pos_iff_ne_zero, mem_Ioc, and_imp, Prod.forall, Prod.mk.injEq]

Premises used: and_imp, Finset.mem_Icc, Nat.le_floor_iff, Prod.mk.injEq, Prod.forall, Finset.mem_filter, Nat.one_le_iff_ne_zero, Real.rpow_nonneg, Finset.mem_Ioc, Finset.mem_product, pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
refine_2 :
  k₁ ≤ ⌊log x / log 2⌋₊ →
    p₁ ≠ 0 →
      (↑p₁ : ℝ) ≤ x →
        Nat.Prime p₁ →
          (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹ →
            ∀ (a b : ℕ),
              a ≠ 0 →
                a ≤ ⌊log x / log 2⌋₊ →
                  b ≠ 0 →
                    (↑b : ℝ) ≤ x →
                      Nat.Prime b → (↑b : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
⊢ k₁ ≤ ⌊log x / log 2⌋₊ →
    p₁ ≠ 0 →
      (↑p₁ : ℝ) ≤ x →
        Nat.Prime p₁ →
          (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹ →
            ∀ (a b : ℕ),
              a ≠ 0 →
                a ≤ ⌊log x / log 2⌋₊ →
                  b ≠ 0 →
                    (↑b : ℝ) ≤ x →
                      Nat.Prime b → (↑b : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
h : k₁ ≤ ⌊log x / log 2⌋₊
refine_2 :
  p₁ ≠ 0 →
    (↑p₁ : ℝ) ≤ x →
      Nat.Prime p₁ →
        (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹ →
          ∀ (a b : ℕ),
            a ≠ 0 →
              a ≤ ⌊log x / log 2⌋₊ →
                b ≠ 0 →
                  (↑b : ℝ) ≤ x →
                    Nat.Prime b → (↑b : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
⊢ p₁ ≠ 0 →
    (↑p₁ : ℝ) ≤ x →
      Nat.Prime p₁ →
        (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹ →
          ∀ (a b : ℕ),
            a ≠ 0 →
              a ≤ ⌊log x / log 2⌋₊ →
                b ≠ 0 →
                  (↑b : ℝ) ≤ x →
                    Nat.Prime b → (↑b : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
h : k₁ ≤ ⌊log x / log 2⌋₊
h_1 : p₁ ≠ 0
refine_2 :
  (↑p₁ : ℝ) ≤ x →
    Nat.Prime p₁ →
      (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹ →
        ∀ (a b : ℕ),
          a ≠ 0 →
            a ≤ ⌊log x / log 2⌋₊ →
              b ≠ 0 →
                (↑b : ℝ) ≤ x →
                  Nat.Prime b → (↑b : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
⊢ (↑p₁ : ℝ) ≤ x →
    Nat.Prime p₁ →
      (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹ →
        ∀ (a b : ℕ),
          a ≠ 0 →
            a ≤ ⌊log x / log 2⌋₊ →
              b ≠ 0 →
                (↑b : ℝ) ≤ x →
                  Nat.Prime b → (↑b : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
h : k₁ ≤ ⌊log x / log 2⌋₊
h_1 : p₁ ≠ 0
h_2 : (↑p₁ : ℝ) ≤ x
hp₁ : Nat.Prime p₁
refine_2 :
  (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹ →
    ∀ (a b : ℕ),
      a ≠ 0 →
        a ≤ ⌊log x / log 2⌋₊ →
          b ≠ 0 →
            (↑b : ℝ) ≤ x → Nat.Prime b → (↑b : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
⊢ (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹ →
    ∀ (a b : ℕ),
      a ≠ 0 →
        a ≤ ⌊log x / log 2⌋₊ →
          b ≠ 0 →
            (↑b : ℝ) ≤ x → Nat.Prime b → (↑b : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
h : k₁ ≤ ⌊log x / log 2⌋₊
h_1 : p₁ ≠ 0
h_2 : (↑p₁ : ℝ) ≤ x
hp₁ : Nat.Prime p₁
h_3 : (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
refine_2 :
  k₂ ≤ ⌊log x / log 2⌋₊ →
    p₂ ≠ 0 →
      (↑p₂ : ℝ) ≤ x →
        Nat.Prime p₂ → (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
⊢ k₂ ≤ ⌊log x / log 2⌋₊ →
    p₂ ≠ 0 →
      (↑p₂ : ℝ) ≤ x →
        Nat.Prime p₂ → (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
h : k₁ ≤ ⌊log x / log 2⌋₊
h_1 : p₁ ≠ 0
h_2 : (↑p₁ : ℝ) ≤ x
hp₁ : Nat.Prime p₁
h_3 : (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
h_4 : k₂ ≤ ⌊log x / log 2⌋₊
refine_2 :
  p₂ ≠ 0 →
    (↑p₂ : ℝ) ≤ x → Nat.Prime p₂ → (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
⊢ p₂ ≠ 0 →
    (↑p₂ : ℝ) ≤ x → Nat.Prime p₂ → (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
h : k₁ ≤ ⌊log x / log 2⌋₊
h_1 : p₁ ≠ 0
h_2 : (↑p₁ : ℝ) ≤ x
hp₁ : Nat.Prime p₁
h_3 : (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
h_4 : k₂ ≤ ⌊log x / log 2⌋₊
h_5 : p₂ ≠ 0
refine_2 :
  (↑p₂ : ℝ) ≤ x → Nat.Prime p₂ → (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
⊢ (↑p₂ : ℝ) ≤ x → Nat.Prime p₂ → (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
h : k₁ ≤ ⌊log x / log 2⌋₊
h_1 : p₁ ≠ 0
h_2 : (↑p₁ : ℝ) ≤ x
hp₁ : Nat.Prime p₁
h_3 : (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
h_4 : k₂ ≤ ⌊log x / log 2⌋₊
h_5 : p₂ ≠ 0
h_6 : (↑p₂ : ℝ) ≤ x
hp₂ : Nat.Prime p₂
refine_2 : (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
⊢ (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
h : k₁ ≤ ⌊log x / log 2⌋₊
h_1 : p₁ ≠ 0
h_2 : (↑p₁ : ℝ) ≤ x
hp₁ : Nat.Prime p₁
h_3 : (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
h_4 : k₂ ≤ ⌊log x / log 2⌋₊
h_5 : p₂ ≠ 0
h_6 : (↑p₂ : ℝ) ≤ x
hp₂ : Nat.Prime p₂
h_7 : (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹
H : p₁ ^ k₁ = p₂ ^ k₂
⊢ k₁ = k₂ ∧ p₁ = p₂

Tactic:
(hp₁.pow_inj' hp₂ hk₁ hk₂ H).symm

Premises used: And.symm, Nat.Prime.pow_inj'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
h : k₁ ≤ ⌊log x / log 2⌋₊
h_1 : p₁ ≠ 0
h_2 : (↑p₁ : ℝ) ≤ x
hp₁ : Nat.Prime p₁
h_3 : (↑p₁ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₁ : ℝ)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
h_4 : k₂ ≤ ⌊log x / log 2⌋₊
h_5 : p₂ ≠ 0
h_6 : (↑p₂ : ℝ) ≤ x
hp₂ : Nat.Prime p₂
h_7 : (↑p₂ : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k₂ : ℝ)⁻¹
H : p₁ ^ k₁ = p₂ ^ k₂
⊢ k₁ = k₂ ∧ p₁ = p₂

Tactic:
exact (hp₁.pow_inj' hp₂ hk₁ hk₂ H).symm

Premises used: And.symm, Nat.Prime.pow_inj'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
refine_3 :
  ∀ (b : ℕ),
    0 < b →
      (↑b : ℝ) ≤ x →
        IsPrimePow b →
          ∃ (a : ℕ),
            0 < a ∧
              a ≤ ⌊log x / log 2⌋₊ ∧
                ∃ (x_1 : ℕ),
                  0 < x_1 ∧ (↑x_1 : ℝ) ≤ x ∧ Nat.Prime x_1 ∧ (↑x_1 : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ ∧ x_1 ^ a = b
⊢ ∀ b ∈ {n ∈ Ioc 0 ⌊x⌋₊ | IsPrimePow n},
    ∃ (a : ℕ × ℕ) (ha :
      a ∈
        {x_1 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match (motive := ℕ × ℕ → Prop) x_1 with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}),
      (fun (x_1 : ℕ × ℕ)
              (x_2 :
                x_1 ∈
                  {x_2 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                    match (motive := ℕ × ℕ → Prop) x_2 with
                    | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}) ↦
            (match (motive :=
                (x_3 : ℕ × ℕ) →
                  x_3 ∈
                      {x_4 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                        match (motive := ℕ × ℕ → Prop) x_4 with
                        | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} →
                    ℕ)
                x_1, x_2 with
              | (k, p), x => p ^ k :
              ℕ))
          a ha =
        b

Tactic:
simp +contextual only [mem_filter, mem_Ioc, hx, le_floor_iff, and_assoc, rpow_nonneg,
        mem_product, mem_Icc, succ_le_iff, exists_prop, Prod.exists, exists_and_left, and_imp]

Premises used: and_imp, Finset.mem_Icc, exists_and_left, Nat.le_floor_iff, exists_prop, and_assoc, Finset.mem_filter, Real.rpow_nonneg, Finset.mem_Ioc, Nat.succ_le_iff, Prod.exists, Finset.mem_product
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : (↑(p ^ k) : ℝ) ≤ x
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x

Tactic:
rw [cast_pow] at hbx

Premises used: Nat.cast_pow
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
⊢ ∃ (a : ℕ),
    0 < a ∧
      a ≤ ⌊log x / log 2⌋₊ ∧
        ∃ (x_1 : ℕ),
          0 < x_1 ∧ (↑x_1 : ℝ) ≤ x ∧ Nat.Prime x_1 ∧ (↑x_1 : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ ∧ x_1 ^ a = p ^ k

Tactic:
⟨k, hk₀, le_floor ?_, p, hp.nat_prime.pos, ?_, hp.nat_prime, ?_, rfl⟩

Premises used: Nat.Prime.pos, Prime.nat_prime, And.intro, Exists.intro, Nat.le_floor, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
refine_3 : (↑k : ℝ) ≤ log x / log 2
refine_3₁ : (↑p : ℝ) ≤ x
refine_3₂ : (↑p : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹
⊢ ∃ (a : ℕ),
    0 < a ∧
      a ≤ ⌊log x / log 2⌋₊ ∧
        ∃ (x_1 : ℕ),
          0 < x_1 ∧ (↑x_1 : ℝ) ≤ x ∧ Nat.Prime x_1 ∧ (↑x_1 : ℝ) ≤ HPow.hPow (β := ℝ) x (↑a : ℝ)⁻¹ ∧ x_1 ^ a = p ^ k

Tactic:
refine ⟨k, hk₀, le_floor ?_, p, hp.nat_prime.pos, ?_, hp.nat_prime, ?_, rfl⟩
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
⊢ LT.lt (α := ℝ) 1 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
refine_3 : log (HPow.hPow (α := ℝ) 2 k) ≤ log x
⊢ (↑k : ℝ) ≤ log x / log 2

Tactic:
rw [le_div_iff₀ (log_pos (by norm_num)), ← Real.log_pow]

Premises used: Real.log_pos, Real.log_pow, le_div_iff₀
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
refine_3 : HPow.hPow (α := ℝ) 2 k ≤ x
⊢ log (HPow.hPow (α := ℝ) 2 k) ≤ log x

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
apply : HPow.hPow (α := ℝ) 2 k ≤ HPow.hPow (α := ℝ) (↑p : ℝ) k
⊢ HPow.hPow (α := ℝ) 2 k ≤ x

Tactic:
apply (LE.le.trans ?_ hbx)

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
⊢ LE.le (α := ℝ) 0 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
⊢ HPow.hPow (α := ℝ) 2 k ≤ HPow.hPow (α := ℝ) (↑p : ℝ) k

Tactic:
exact pow_le_pow_left₀ (by norm_num) (mod_cast hp.nat_prime.two_le) _

Premises used: pow_le_pow_left₀
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
⊢ (↑p : ℝ) ≤ x

Tactic:
(le_self_pow₀ (mod_cast hp.nat_prime.one_le) hk₀.ne').trans hbx

Premises used: LT.lt.ne', le_self_pow₀, LE.le.trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
⊢ (↑p : ℝ) ≤ x

Tactic:
exact (le_self_pow₀ (mod_cast hp.nat_prime.one_le) hk₀.ne').trans hbx

Premises used: LT.lt.ne', le_self_pow₀, LE.le.trans