RS_prime_helper.p_n_lower_large

lemma p_n_lower_large (n : ℕ) (hn : n ≥ 32) :    (nth_prime' n : ℝ) > n * (Real.log n + Real.log (Real.log n) - 3 / 2) := by  have h_dusart : (nth_prime' n : ℝ) ≥ n * (Real.log (nth_prime' n) - 1.112) := by    have h_pi_le : (n : ℝ) ≤ (nth_prime' n) / (Real.log (nth_prime' n) - 1.112) := by      have h_pi_le :          pi (nth_prime' n) ≤ (nth_prime' n : ℝ) / (Real.log (nth_prime' n) - 1.112) := by        convert Dusart.corollary_5_3_b _ using 1        have h_step1 : (nth_prime' n : ℝ) ≥ n + 1 := by          norm_cast          have h_step1 : ∀ n ≥ 1, nth_prime' n ≥ n + 1 := by            intro n hn            induction n, hn using Nat.le_induction with            | base =>              exact Prime.two_le (prime_nth_prime 0) |> succ_le_of_lt |> le_trans <| le_refl _            | succ n _ ih =>              exact succ_le_of_lt (lt_of_le_of_lt ih (nth_strictMono (infinite_setOf_prime) (pred_lt (by positivity))))          exact h_step1 n (by linarith)        generalize_proofs at *        have h_exp_approx : Real.exp 1.112 < 33 := by linarith [LogTables.exp_1_112_lt]        linarith [show (n : ℝ) ≥ 32 by norm_cast]      convert h_pi_le using 1      exact_mod_cast Eq.symm (pi_nth_prime' n (by linarith))    rwa [le_div_iff₀ (sub_pos.mpr <| by      contrapose! h_pi_le      exact lt_of_le_of_lt        (div_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg _) (sub_nonpos.mpr h_pi_le))        (by positivity))] at h_pi_le  have h_log_pn :      Real.log (nth_prime' n) ≥ Real.log n + Real.log (Real.log n - 1.112) := by    have h_pn_ge : (nth_prime' n : ℝ) ≥ n * (Real.log n - 1.112) := by      refine le_trans ?_ h_dusart      generalize_proofs at *; (      gcongr;      refine Nat.le_induction ?_ ?_ n (show n ≥ 1 from by linarith) <;>        intros <;> simp_all only [nth_prime']      · exact Prime.pos (prime_nth_prime 0) |> one_le_of_lt      · exact nth_strictMono (infinite_setOf_prime) (by omega) |> lt_of_le_of_lt (by omega))    have h_log_gt : Real.log n > 1.112 := by      have : Real.log 32 > 1.112 := by linarith [LogTables.log_32_gt]      exact this.trans_le (Real.log_le_log (by norm_num) (mod_cast hn)) |> lt_of_lt_of_le <| le_rfl    have h_log_pn_ge :        Real.log (nth_prime' n) ≥ Real.log (n * (Real.log n - 1.112)) :=      Real.log_le_log (mul_pos (by positivity) (sub_pos.mpr h_log_gt)) h_pn_ge    have h_log_split :        Real.log (n * (Real.log n - 1.112)) =          Real.log n + Real.log (Real.log n - 1.112) := by      rw [Real.log_mul] <;> norm_num      · aesop      · linarith [Real.log_le_log (by norm_num : (0 : ℝ) < 32) (by norm_cast),          LogTables.log_32_gt]    linarith [h_log_pn_ge, h_log_split]  have h_loglog : Real.log (Real.log n - 1.112) > 0.85 := by    have h_log_n_ge : Real.log n ≥ Real.log 32 :=      Real.log_le_log (by norm_num) (by norm_cast)    have h_log_32 : Real.log 32 > 3.465 := by linarith [LogTables.log_32_gt]    have h_log_2_353 : log 2.353 > 0.85 := by linarith [LogTables.log_2_353_gt]    exact (h_log_2_353.trans_le      (Real.log_le_log (by norm_num) (by linarith))).trans_le' (by norm_num)  have h_pn_ge2 : (nth_prime' n : ℝ) ≥ n * (Real.log n + 0.85 - 1.112) :=    le_trans (mul_le_mul_of_nonneg_left (by linarith) (Nat.cast_nonneg _)) h_dusart  have h_log_32_bound : Real.log 32 - 0.262 > 3.2 := by linarith [LogTables.log_32_gt]  have h_pn_ge3 : (nth_prime' n : ℝ) ≥ n * 3.2 := by    have : Real.log n - 0.262 ≥ Real.log 32 - 0.262 :=      sub_le_sub_right (Real.log_le_log (by norm_num) (by norm_cast)) _    exact le_trans (mul_le_mul_of_nonneg_left (by linarith) (cast_nonneg _)) h_pn_ge2  have h_pn_gt_nlogn : (nth_prime' n : ℝ) > n * Real.log n := by    have h_log_pn_gt : Real.log (nth_prime' n) > Real.log n + 1.16 := by      have : Real.log (nth_prime' n) ≥ Real.log n + Real.log (3.2) := by        rw [← log_mul (by positivity) (by positivity)]        exact log_le_log (by positivity) (by linarith)      have : log (3.2) > 1.16 := by linarith [LogTables.log_3_2_gt]      linarith    have : (nth_prime' n : ℝ) ≥ n * (Real.log n + 1.16 - 1.112) :=      le_trans (mul_le_mul_of_nonneg_left (by linarith) (cast_nonneg _)) h_dusart    linarith [show (n : ℝ) ≥ 32 by norm_cast]  have h_log_sum : Real.log (nth_prime' n) > Real.log n + log (log n) := by    rw [← log_mul (by positivity) (by exact ne_of_gt <| log_pos <| by norm_cast; linarith)]    exact log_lt_log (by exact mul_pos (by positivity) <| log_pos <| by norm_cast; linarith) h_pn_gt_nlogn  nlinarith [show (n : ℝ) ≥ 32 by norm_cast]