BrunTitchmarsh.tmp

theorem tmp (N : ℕ) :    ((Finset.range N).filter Nat.Prime).card ≤      4 * (N / Real.log N) + 6 * (N ^ (1/2 : ℝ) * (1 + 1/2 * Real.log N) ^ 3) := by  trans ↑((Finset.range (N+1)).filter Nat.Prime).card  · norm_cast    refine Finset.card_le_card fun n ↦ ?_    simp only [Finset.mem_filter, Finset.mem_range, and_imp]    exact fun hnN hp ↦ ⟨by omega, hp⟩  rw [← primesBetween_one]  by_cases hN : N = 0  · simp [hN, primesBetween]  by_cases hN : N = 1  · simp (config := {decide:=true}) [hN, primesBetween]  have h : primesBetween 1 (1 + N) ≤      2 * (N / Real.log (N ^ (1/2 : ℝ))) +        6 * (N ^ (1 / 2 : ℝ) * (1 + Real.log (N ^ (1/2 : ℝ))) ^ 3) := by    convert (primesBetween_le 1 N (N ^ (1/2 : ℝ)) (by norm_num) (by norm_cast; omega)      (Real.one_lt_rpow (by norm_cast; omega) (by norm_num))) using 1    ring  calc    _ ≤ (primesBetween 1 (1+N):ℝ) := by      norm_cast      apply primesBetween_mono_right      norm_cast      omega    _ ≤ _ := by      rw [Real.log_rpow (by norm_num; omega)] at h      convert h using 2      ring