have H_log_le_primeCountingReal_add_one (n : ℕ) (x : ℝ) (hxge : x ≥ n) (hxlt : x < n + 1) :
    Real.log x ≤ primeCountingReal x + 1 :=
  calc
    Real.log x ≤ ∑ k in Icc 1 n, (k : ℝ)⁻¹ := by sorry
    _ ≤ (∑' m : (S₁ x), (m : ℝ)⁻¹) := by sorry
    _ ≤ (∏ p in primesBelow ⌊x⌋.natAbs, (∑' k : ℕ, (p ^ k : ℝ)⁻¹)) := by sorry
    _ ≤ (∏ k in Icc 1 (primeCountingReal x), (nth Nat.Prime k) / ((nth Nat.Prime k) - 1)) := by sorry
    _ ≤ (∏ k in Icc 1 (primeCountingReal x), (k + 1) / k) := by sorry
    _ ≤ primeCountingReal x + 1 := by sorry
⊢ Tendsto π atTop atTop
H_log_le_primeCountingReal_add_one : ∀ (n : ℕ), ∀ x ≥ ↑n, x < ↑n + 1 → x.log ≤ ↑(primeCountingReal x) + 1
⊢ Tendsto π atTop atTop