awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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 : ℝ)⁻¹⌋₊})
    (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₂
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
⊢ ∀ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
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
⊢ ∃ (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
have hbx₁ : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
Tactic: rw [cast_pow] at hbx
Cleared hypotheses: hbx
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
have refine_3 : (↑k : ℝ) ≤ log x / log 2
Tactic: refine ⟨k, hk₀, le_floor ?_, p, hp.nat_prime.pos, ?_, hp.nat_prime, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ ∃ (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
have refine_3₁ : (↑p : ℝ) ≤ x
Tactic: refine ⟨k, hk₀, le_floor ?_, p, hp.nat_prime.pos, ?_, hp.nat_prime, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ ∃ (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
have refine_3₂ : (↑p : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹
Tactic: refine ⟨k, hk₀, le_floor ?_, p, hp.nat_prime.pos, ?_, hp.nat_prime, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ (↑k : ℝ) ≤ log x / log 2
have refine_3 : log (HPow.hPow (α := ℝ) 2 k) ≤ log x
Tactic: rw [le_div_iff₀ (log_pos (by norm_num)), ← Real.log_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ log (HPow.hPow (α := ℝ) 2 k) ≤ log x
have refine_3 : HPow.hPow (α := ℝ) 2 k ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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 ≤ x
have apply : HPow.hPow (α := ℝ) 2 k ≤ HPow.hPow (α := ℝ) (↑p : ℝ) k
Tactic: apply (LE.le.trans ?_ hbx)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
⊢ 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))
have rw : Eq.{u_1 + 1} (α := R)
  (∑ x_1 ∈ Icc 1 ⌊log x / log 2⌋₊,
    ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
      if
          match (motive := ℕ × ℕ → Prop) (x_1, y) with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ then
        match (motive := ℕ × ℕ → R) (x_1, y) with
        | (k, p) => f (p ^ k)
      else 0)
  (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))
Tactic: rw [sum_filter, sum_product]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ Icc 1 ⌊log x / log 2⌋₊,
      ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (motive := ℕ × ℕ → Prop) (x_1, y) with
            | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ then
          match (motive := ℕ × ℕ → R) (x_1, y) with
          | (k, p) => f (p ^ k)
        else 0)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))
have refine : ∀ k ∈ Icc 1 ⌊log x / log 2⌋₊,
  Eq.{u_1 + 1} (α := R)
    (∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
      if
          match (motive := ℕ × ℕ → Prop) (k, y) with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ then
        match (motive := ℕ × ℕ → R) (k, y) with
        | (k, p) => f (p ^ k)
      else 0)
    (∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))
Tactic: refine sum_congr rfl fun k _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
⊢ Eq.{u_1 + 1} (α := R)
    (∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
      if
          match (motive := ℕ × ℕ → Prop) (k, y) with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ then
        match (motive := ℕ × ℕ → R) (k, y) with
        | (k, p) => f (p ^ k)
      else 0)
    (∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))
have simp : Eq.{u_1 + 1} (α := R) (∑ x ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with x ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊, f (x ^ k))
  (∑ x ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime x, f (x ^ k))
Tactic: simp only [sum_ite, not_le, sum_const_zero, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with x ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊, f (x ^ k))
    (∑ x ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime x, f (x ^ k))
have e_s : {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} =
  {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ | Nat.Prime p}
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
⊢ {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} =
    {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ | Nat.Prime p}
have e_s : ∀ (p : ℕ),
  p ∈ {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} ↔
    p ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ | Nat.Prime p}
Tactic: ext p
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
p : ℕ
⊢ p ∈ {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} ↔
    p ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ | Nat.Prime p}
have e_s : ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ ↔
  (0 < p ∧ p ≤ ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊) ∧ Nat.Prime p
Tactic: simp only [mem_filter, mem_Ioc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
p : ℕ
⊢ ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ ↔
    (0 < p ∧ p ≤ ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊) ∧ Nat.Prime p
have e_s : ∀ (h : (0 < p ∧ p ≤ ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊) ∧ Nat.Prime p),
  ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊
Tactic: refine ⟨fun _ ↦ (by simp_all), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h_1 : k ∈ Icc 1 ⌊log x / log 2⌋₊
p : ℕ
h : (0 < p ∧ p ≤ ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊) ∧ Nat.Prime p
⊢ ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊
have e_s : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊ → ∀ (h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p), p ≤ ⌊x⌋₊
Tactic: simp_all only [mem_Icc, one_div, true_and, and_true]
Cleared hypotheses: h_1, h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
⊢ p ≤ ⌊x⌋₊
have e_s : HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹ ≤ x
Tactic: grw [h.1.2, floor_le_floor]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
⊢ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹ ≤ x
have apply : 1 ≤ x
Tactic: apply rpow_le_self_of_one_le _ (by bound)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
⊢ 1 ≤ x
have this : 1 ≤ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹
Tactic: have := one_le_floor_iff _ |>.mp <| le_trans (one_le_cast.mp h.2.one_le) h.1.2
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
this : 1 ≤ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹
⊢ 1 ≤ x
have contrapose! : ∀ (this : x < 1), HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹ < 1
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ ψ x = ∑ n ∈ Icc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have simp_rw : Eq (α := ℝ)
  (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊,
    ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, log (↑(p ^ k).minFac : ℝ))
  (∑ n ∈ Icc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
Tactic: simp_rw [psi, vonMangoldt_apply, ← sum_filter, sum_PrimePow_eq_sum_sum _ hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ Eq (α := ℝ)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊,
      ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, log (↑(p ^ k).minFac : ℝ))
    (∑ n ∈ Icc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
have apply : ∀ (x_1 : ℕ) (hk : x_1 ∈ Icc 1 ⌊log x / log 2⌋₊),
  ∀ x_2 ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)⌋₊ | Nat.Prime p},
    log (↑(x_2 ^ x_1).minFac : ℝ) = log (↑x_2 : ℝ)
Tactic: apply sum_congr rfl fun _ hk ↦ sum_congr rfl fun _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
x_1 : ℕ
hk : x_1 ∈ Icc 1 ⌊log x / log 2⌋₊
x_2 : ℕ
h : x_2 ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)⌋₊ | Nat.Prime p}
⊢ x_1 ≠ 0
have linarith : x_1 = 0 → -1 + HSub.hSub (α := ℤ) (↑x_1 : ℤ) 0 + HSub.hSub (α := ℤ) 1 (↑x_1 : ℤ) = 0
Tactic: linarith [mem_Icc.mp hk]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
x_1 : ℕ
hk : x_1 ∈ Icc 1 ⌊log x / log 2⌋₊
x_2 : ℕ
h : x_2 ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)⌋₊ | Nat.Prime p}
⊢ log (↑(x_2 ^ x_1).minFac : ℝ) = log (↑x_2 : ℝ)
have rw : Nat.Prime x_2
Tactic: rw [Prime.pow_minFac _ (by linarith [mem_Icc.mp hk])]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ 0 ≤ x
have linarith : x < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
linarith : x < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - x) + (x - 0) = 0
⊢ 0 ≤ x
have linarith₁ : x < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ ψ x = θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw : θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) + ∑ x_1 ∈ Ioc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) =
  θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [psi_eq_sum_theta (by linarith), ← add_sum_Ioc_eq_sum_Icc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
rw :
  θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) + ∑ x_1 ∈ Ioc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) =
    θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ ψ x = θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have rw₁ : 1 ≤ ⌊log x / log 2⌋₊
Tactic: rw [psi_eq_sum_theta (by linarith), ← add_sum_Ioc_eq_sum_Icc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) + ∑ x_1 ∈ Ioc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) =
    θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have e_a : x ^ HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ) = x
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ 1 ≤ ⌊log x / log 2⌋₊
have rw : log 2 ≤ log x
Tactic: rw [le_floor_iff' one_ne_zero, le_div_iff₀ (by positivity), cast_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ log 2 ≤ log x
have hx₁ : LT.lt (α := ℝ) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ θ x ≤ ψ x
have pos : ∀ (h : x < 2), θ x ≤ ψ x
Tactic: by_cases! h : x < 2
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
pos : ∀ (h : x < 2), θ x ≤ ψ x
⊢ θ x ≤ ψ x
have neg : ∀ (h : 2 ≤ x), θ x ≤ ψ x
Tactic: by_cases! h : x < 2
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : x < 2
⊢ θ x ≤ ψ x
have pos : 0 ≤ ψ x
Tactic: rw [theta_eq_zero_of_lt_two h, psi_eq_zero_of_lt_two h]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : x < 2
pos : 0 ≤ ψ x
⊢ θ x ≤ ψ x
have pos₁ : LE.le (α := ℝ) 0 0
Tactic: rw [theta_eq_zero_of_lt_two h, psi_eq_zero_of_lt_two h]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 2 ≤ x
⊢ θ x ≤ ψ x
have neg : θ x ≤ θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [psi_eq_theta_add_sum_theta h]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 2 ≤ x
⊢ θ x ≤ θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have neg : LE.le (α := ℝ) 0 (∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
Tactic: simp only [le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ |ψ x - θ x| ≤ 2 * √x * log x
have pos : ∀ (hx : x < 2), |ψ x - θ x| ≤ 2 * √x * log x
Tactic: by_cases! hx : x < 2
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
pos : ∀ (hx : x < 2), |ψ x - θ x| ≤ 2 * √x * log x
⊢ |ψ x - θ x| ≤ 2 * √x * log x
have neg : ∀ (hx : 2 ≤ x), |ψ x - θ x| ≤ 2 * √x * log x
Tactic: by_cases! hx : x < 2
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : x < 2
⊢ |ψ x - θ x| ≤ 2 * √x * log x
have pos : 0 ≤ 2 * √x * log x
Tactic: rw [psi_eq_zero_of_lt_two hx, theta_eq_zero_of_lt_two hx, sub_zero, abs_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ |ψ x - θ x| ≤ 2 * √x * log x
have neg : |∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))| ≤ 2 * √x * log x
Tactic: rw [psi_eq_theta_add_sum_theta hx, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ |∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))| ≤ 2 * √x * log x
have neg : ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, |θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ))| ≤ 2 * √x * log x
Tactic: apply le_trans <| abs_sum_le_sum_abs ..
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, |θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ))| ≤ 2 * √x * log x
have neg : ∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) ≤ 2 * √x * log x
Tactic: simp_rw [abs_of_nonneg <| theta_nonneg _]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) ≤ 2 * √x * log x
have trans : LE.le (α := ℝ) (∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)))
  (∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x)
Tactic: trans ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * x.sqrt
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
trans :
  LE.le (α := ℝ) (∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)))
    (∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x)
⊢ ∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) ≤ 2 * √x * log x
have trans₁ : ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x ≤ 2 * √x * log x
Tactic: trans ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * x.sqrt
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ LE.le (α := ℝ) (∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)))
    (∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x)
have h : ∀ (i : ℕ) (hi : i ∈ Icc 2 ⌊log x / log 2⌋₊), θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) ≤ log 4 * √x
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ 0 ≤ x
have linarith : x < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
linarith : x < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - x) + (x - 0) = 0
⊢ 0 ≤ x
have linarith₁ : x < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) ≤ log 4 * √x
have h : log 4 * x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ) ≤ log 4 * √x
Tactic: apply le_trans (theta_le_log4_mul_x (rpow_nonneg (by linarith) _))
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ log 4 * x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ) ≤ log 4 * √x
have h : log 4 * x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ) ≤ log 4 * x ^ (1 / 2)
Tactic: rw [sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ log 4 * x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ) ≤ log 4 * x ^ (1 / 2)
have h : LE.le (α := ℝ) 2 (↑i : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x ≤ 2 * √x * log x
have simp : (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ 2 * √x * log x
Tactic: simp only [sum_const, card_Icc, reduceSubDiff, nsmul_eq_mul]