Lcm.exists_p_primes

@[blueprint  "lem:choose-pi"  (title := "Choice of medium primes \\(p_i\\)")  (statement := /--  Let \(n \ge X_0^2\). Set \(x := \sqrt{n}\). Then there exist primes \(p_1,p_2,p_3\) with  \[    p_i \le x \Bigl(1 + \frac{1}{\log^3 x}\Bigr)^i  \]  and \(p_1 < p_2 < p_3\).  Moreover, \(\sqrt{n} < p_1\)  -/)  (proof := /-- Apply Proposition~\ref{Dusart_prop_5_4} successively with  \(x, x(1+1/\log^3 x), x(1+1/\log^3 x)^2\), keeping track of the resulting primes and bounds.  For \(n\) large and \(x = \sqrt{n}\), we have \(\sqrt{n} < p_1\) as soon as the first interval  lies strictly above \(\sqrt{n}\); this can be enforced by taking \(n\) large enough. -/)  (latexEnv := "lemma")]theorem exists_p_primes {n : ℕ} (hn : n ≥ X₀ ^ 2) :    ∃ p : Fin 3 → ℕ, (∀ i, Nat.Prime (p i)) ∧ StrictMono p ∧      (∀ i, p i ≤ √(n : ℝ) * (1 + 1 / (log √(n : ℝ)) ^ 3) ^ (i + 1 : ℝ)) ∧      √(n : ℝ) < p 0 := by  let x := √(n : ℝ)  have hx_pos : 0 < x := (by grind : (0 : ℝ) < X₀).trans_le (hsqrt_ge hn)  have hlog_pos : 0 < log x := by positivity [hlog hn]  set ε := 1 / (log x) ^ 3 with hε_def  have upper {y : ℝ} (hy : 0 < y) (hlog_ge : log y ≥ log x) {p : ℕ}      (hp : (p : ℝ) ≤ y + y / (log y) ^ (3 : ℝ)) : (p : ℝ) ≤ y * (1 + ε) := by    have h : y / (log y) ^ (3 : ℝ) ≤ y / (log x) ^ (3 : ℝ) :=      div_le_div_of_nonneg_left hy.le (rpow_pos_of_pos hlog_pos 3)        (rpow_le_rpow hlog_pos.le hlog_ge (by grind))    calc (p : ℝ) ≤ y + y / (log y) ^ (3 : ℝ) := hp      _ ≤ y + y / (log x) ^ (3 : ℝ) := add_le_add_right h y      _ = y * (1 + ε) := by simp only [hε_def, ← rpow_natCast]; grind  have hε_pos : 0 < ε := by positivity  have hx1_ge : x * (1 + ε) ≥ X₀ := (hsqrt_ge hn).trans (le_mul_of_one_le_right hx_pos.le    (by grind))  have hx2_ge : x * (1 + ε) ^ 2 ≥ X₀ := (hsqrt_ge hn).trans (le_mul_of_one_le_right hx_pos.le    (by nlinarith [sq_nonneg ε]))  obtain ⟨p₀, hp₀_prime, hp₀_lb, hp₀_ub⟩ := Dusart.proposition_5_4 x (hsqrt_ge hn)  obtain ⟨p₁, hp₁_prime, hp₁_lb, hp₁_ub⟩ := Dusart.proposition_5_4 _ hx1_ge  obtain ⟨p₂, hp₂_prime, hp₂_lb, hp₂_ub⟩ := Dusart.proposition_5_4 _ hx2_ge  have hp₀_ub' : (p₀ : ℝ) ≤ x * (1 + ε) := upper hx_pos le_rfl hp₀_ub  have hp₁_ub' : (p₁ : ℝ) ≤ x * (1 + ε) ^ 2 := by    linarith [sq (1 + ε), upper (by grind) (log_le_log hx_pos (by grind)) hp₁_ub]  have hp₂_ub' : (p₂ : ℝ) ≤ x * (1 + ε) ^ 3 := by    linarith [pow_succ (1 + ε) 2, upper (by grind) (log_le_log hx_pos (by grind)) hp₂_ub]  refine ⟨![p₀, p₁, p₂], fun i ↦ by fin_cases i <;> assumption,    Fin.strictMono_iff_lt_succ.mpr fun i ↦ by      fin_cases i      · exact cast_lt.mp (hp₀_ub'.trans_lt hp₁_lb)      · exact cast_lt.mp (hp₁_ub'.trans_lt hp₂_lb), fun i ↦ ?_, hp₀_lb⟩  fin_cases i <;> norm_num  · convert hp₀_ub' using 2  · convert hp₁_ub' using 2  · convert hp₂_ub' using 2