Erdos392.Params.primeCounting_ge_log

lemma Params.primeCounting_ge_log (n : ℕ) (hn : n ≥ 2) :    (n.primeCounting : ℝ) ≥ Real.log n := by  have h_prod_le : ∀ k : ℕ, Nat.primeCounting (2 ^ k) ≥ k := by    intro k    induction k with    | zero => norm_num    | succ k ih =>      obtain ⟨p, hp_prime, hp_bounds⟩ : ∃ p, p.Prime ∧ 2 ^ k < p ∧ p ≤ 2 ^ (k + 1) := by        obtain ⟨p, hp₁, hp₂⟩ := bertrand (2 ^ k) (by positivity)        exact ⟨p, hp₁, by linarith, by rw [_root_.pow_succ']; linarith⟩      rw [primeCounting] at *      rw [primeCounting', count_eq_card_filter_range] at *      refine le_trans (succ_le_succ ih) (Finset.card_lt_card ?_)      norm_num [Finset.ssubset_def, Finset.subset_iff]      exact ⟨fun x hx₁ hx₂ => ⟨by linarith, hx₂⟩,        p, by linarith, hp_prime, fun hx₃ => by linarith⟩  obtain ⟨k, hk⟩ : ∃ k : ℕ, 2 ^ k ≤ n ∧ n < 2 ^ (k + 1) :=    ⟨log 2 n, pow_le_of_le_log (ne_zero_of_lt hn)        (log_anti_left (h_prod_le (succ 1)) (h_prod_le 2)),      lt_pow_of_log_lt (one_lt_two) (Nat.lt_add_of_pos_right (h_prod_le (succ 0)))⟩  have h_pi_ge_k : primeCounting n ≥ k := le_trans (h_prod_le k) (monotone_primeCounting hk.1)  have h_log_le : Real.log n ≤ (k + 1) * Real.log 2 := by    rw [← Real.log_rpow zero_lt_two]    gcongr    norm_cast    linarith [pow_succ' 2 k]  have h_k_ge_5 : 5 ≤ k → (k + 1) * Real.log 2 ≤ k := fun hk => by    have := Real.log_two_lt_d9    norm_num1 at *    nlinarith [show (k : ℝ) ≥ 5 by norm_cast]  by_cases hk_ge_5 : 5 ≤ k  · exact le_trans h_log_le (le_trans (h_k_ge_5 hk_ge_5) (mod_cast h_pi_ge_k))  · interval_cases k <;> norm_num at *    · grind    · rcases hk with ⟨hk₁, hk₂⟩; interval_cases n <;> norm_num at *      · exact le_trans log_two_lt_d9.le          (by norm_num; linarith [show (primeCounting 2 : ℝ) ≥ 1 by exact_mod_cast h_pi_ge_k])      · rw [show primeCounting 3 = 2 by rfl]; norm_num        linarith [log_le_sub_one_of_pos zero_lt_three]    · rcases hk with ⟨hk₁, hk₂⟩; interval_cases n <;> norm_num at *      · rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]; norm_num        exact le_trans (mul_le_mul_of_nonneg_left log_two_lt_d9.le zero_le_two)          (by norm_num; linarith [show (primeCounting 4 : ℝ) ≥ 2 by exact_mod_cast h_pi_ge_k])      · rw [show (primeCounting 5 : ℝ) = 3 by norm_cast]        have := log_two_lt_d9; norm_num at *        linarith [log_le_sub_one_of_pos (show 0 < 5 / 4 by norm_num)]      · rw [show primeCounting 6 = 3 by rfl]; norm_num        have := log_two_lt_d9; have := log_lt_sub_one_of_pos zero_lt_three        norm_num at *        linarith      · rw [show primeCounting 7 = 4 by rfl]; norm_num        linarith [LogTables.log_7_lt]    · grw [h_log_le, log_two_lt_d9, ← h_pi_ge_k]; norm_num    · grw [h_log_le, log_two_lt_d9, ← h_pi_ge_k]; norm_num