awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
rwa :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
⊢ 1 / 2 ≤ S
have rwa₁ : ∀
  (this :
    HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
      HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HMul.hMul (α := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
        HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
rwa :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HMul.hMul (α := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
⊢ 1 / 2 ≤ S
have rwa₂ : ∀
  (this :
    HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
      HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
        HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
rwa :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HMul.hMul (α := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₂ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
⊢ 1 / 2 ≤ S
have rwa₃ : ∀
  (this :
    HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
      HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (β := ℕ) (2 * m) 2).sqrt : ℝ) +
        HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
rwa :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HMul.hMul (α := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₂ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₃ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (β := ℕ) (2 * m) 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
⊢ 1 / 2 ≤ S
have rwa₄ : ∀
  (this :
    HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
      HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) + HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
rwa :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HMul.hMul (α := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₂ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₃ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (β := ℕ) (2 * m) 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₄ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) + HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
⊢ 1 / 2 ≤ S
have rwa₅ : ∀
  (this :
    HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) - HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) ≤
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
rwa :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HMul.hMul (α := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₂ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₃ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (β := ℕ) (2 * m) 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₄ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) + HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₅ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) - HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) ≤
        HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
⊢ 1 / 2 ≤ S
have rwa₆ : ∀
  (this :
    2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) - HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) ≤
      2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
rwa :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HMul.hMul (α := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₂ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₃ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (β := ℕ) (2 * m) 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₄ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) + HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₅ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) - HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) ≤
        HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₆ :
  ∀
    (this :
      2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) - HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) ≤
        2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
⊢ 1 / 2 ≤ S
have rwa₇ : ∀
  (this :
    2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) - (↑m : ℝ) * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑m : ℝ) ≤
      2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
rwa :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HMul.hMul (α := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₂ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₃ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (β := ℕ) (2 * m) 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₄ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) + HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₅ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) - HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) ≤
        HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₆ :
  ∀
    (this :
      2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) - HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) ≤
        2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₇ :
  ∀
    (this :
      2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) -
          (↑m : ℝ) * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑m : ℝ) ≤
        2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
⊢ 1 / 2 ≤ S
have rwa₈ : ∀
  (this :
    2 * ((↑2 : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) - (↑m : ℝ) * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑m : ℝ) ≤
      2 * ((↑2 : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
this :
  HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
rwa :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * (2 * HPow.hPow (β := ℕ) m 2)).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HMul.hMul (α := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₂ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (α := ℕ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) m 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₃ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(HPow.hPow (β := ℕ) (2 * m) 2).sqrt : ℝ) +
          HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₄ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) ≤
        HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) + HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₅ :
  ∀
    (this :
      HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) - HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) ≤
        HMul.hMul (α := ℝ) 2 (↑(2 * HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₆ :
  ∀
    (this :
      2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) - HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * m) : ℝ) ≤
        2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₇ :
  ∀
    (this :
      2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) -
          (↑m : ℝ) * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑m : ℝ) ≤
        2 * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑(HPow.hPow (β := ℕ) m 2) : ℝ) * S),
    1 / 2 ≤ S
rwa₈ :
  ∀
    (this :
      2 * ((↑2 : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) - (↑m : ℝ) * HMul.hMul (α := ℝ) (↑2 : ℝ) (↑m : ℝ) ≤
        2 * ((↑2 : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) * S),
    1 / 2 ≤ S
⊢ 1 / 2 ≤ S
have rwa₉ : ∀
  (this :
    2 * (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) - (↑m : ℝ) * HMul.hMul (α := ℝ) 2 (↑m : ℝ) ≤
      2 * (2 * HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 2) * S),
  1 / 2 ≤ S
Tactic: rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
⊢ 1 / 2 ≤ S
have suffices : HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
Tactic: suffices 2 * N₀ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S by
    rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
⊢ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + (↑((2 * N₀).roughNumbersUpTo k).card : ℝ) ≤
    HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
have grw : HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) +
    HMul.hMul (α := ℝ) (↑(2 * N₀) : ℝ)
      (∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) ≤
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
Tactic: grw [roughNumbersUpTo_card_le']
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
⊢ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) +
      HMul.hMul (α := ℝ) (↑(2 * N₀) : ℝ)
        (∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) ≤
    HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
have norm_cast : (↑(m * (2 * N₀).sqrt) : ℝ) +
    HMul.hMul (α := ℝ) (↑(2 * N₀) : ℝ)
      (∑ x ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑x : ℝ)) ≤
  (↑(m * (2 * N₀).sqrt) : ℝ) +
    HMul.hMul (α := ℝ) (↑(2 * N₀) : ℝ) (∑ x ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑x : ℝ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SumPrimeReciprocals (goal)
Goal:
k : ℕ
m : ℕ := HPow.hPow (α := ℕ) 2 k.primesBelow.card
N₀ : ℕ := 2 * HPow.hPow (β := ℕ) m 2
hN₀ : N₀ = 2 * HPow.hPow (β := ℕ) m 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑(2 * N₀).sqrt : ℝ) + HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) * S
have calc : HMul.hMul (α := ℝ) 2 (↑N₀ : ℝ) =
  HAdd.hAdd (α := ℝ) (↑((2 * N₀).smoothNumbersUpTo k).card : ℝ) (↑((2 * N₀).roughNumbersUpTo k).card : ℝ)
Tactic: calc (2 * N₀ : ℝ)
    _ = ((2 * N₀).smoothNumbersUpTo k).card + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast ((2 * N₀).smoothNumbersUpTo_card_add_roughNumbersUpTo_card k).symm
    _ ≤ m * (2 * N₀).sqrt + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _
    _ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S := by grw [roughNumbersUpTo_card_le']; norm_cast