-- 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
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) * (1 / 2) ≤ 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