Lcm.Criterion.Ln_div_M_lt

@[blueprint  "lem:M-basic"  (title := "Basic properties of \\(M\\)")  (statement := /--  With notation as above, we have:  \begin{enumerate}    \item \(M < L_n\).    \item    \[      1 < \frac{L_n}{M} = \Bigl(1 - \frac{r}{q_1 q_2 q_3}\Bigr)^{-1}        < \Bigl(1 - \frac{4 p_1 p_2 p_3}{q_1 q_2 q_3}\Bigr)^{-1}.    \]  \end{enumerate}  -/)  (proof := /--  The first item is by construction of the division algorithm.  For the second, note that  \[    L_n = q_1 q_2 q_3 L' = (4 p_1 p_2 p_3 m + r) L' > 4 p_1 p_2 p_3 m L' = M,  \]  since \(r>0\). For the third,  \[    \frac{L_n}{M} = \frac{4 p_1 p_2 p_3 m + r}{4 p_1 p_2 p_3 m}                = 1 + \frac{r}{4 p_1 p_2 p_3 m}                = \Bigl(1 - \frac{r}{4 p_1 p_2 p_3 m + r}\Bigr)^{-1}                = \Bigl(1 - \frac{r}{q_1 q_2 q_3}\Bigr)^{-1}.  \]  Since \(0 < r < 4p_1p_2p_3\) and \(4p_1p_2p_3 < q_1q_2q_3\), we have  \[    0<\frac{r}{q_1 q_2 q_3}<\frac{4p_1p_2p_3}{q_1 q_2 q_3},  \]  so  \[    \Bigl(1-\frac{r}{q_1 q_2 q_3}\Bigr)^{-1}    < \Bigl(1-\frac{4p_1p_2p_3}{q_1 q_2 q_3}\Bigr)^{-1}.  \]  -/)  (latexEnv := "lemma")]theorem Criterion.Ln_div_M_lt (c : Criterion) :    L c.n / c.M < (1 - (4 : ℝ) * (∏ i, c.p i) / (∏ i, c.q i))⁻¹ := by  have hprod_q_pos_R : (0 : ℝ) < (∏ i, c.q i) :=    cast_pos.mpr <| prod_pos fun i _ ↦ (c.hq i).pos  have hLM_eq :      (L c.n : ℝ) / c.M = ((∏ i, c.q i) : ℝ) / (((4 * ∏ i, c.p i) * c.m) : ℕ) := by    simp only [c.L_eq_prod_q_mul_L', M, cast_mul]    have hL'_ne : (c.L' : ℝ) ≠ 0 := cast_ne_zero.mpr c.L'_pos.ne'    field_simp    congr 1    exact prod_natCast univ c.q  have hLM_eq' : (L c.n : ℝ) / c.M = (1 - (c.r : ℝ) / (∏ i, c.q i))⁻¹ := by    have hprod_q_eq_R : ((∏ i, c.q i) : ℝ) = ((4 * ∏ i, c.p i) * c.m : ℕ) + c.r := by      exact_mod_cast c.prod_q_eq    have h4pm_pos : 0 < (4 * ∏ i, c.p i) * c.m := mul_pos      (mul_pos (by norm_num) <| prod_pos fun i _ ↦ (c.hp i).pos) c.m_pos    rw [hLM_eq, hprod_q_eq_R]    have hne : (((4 * ∏ i, c.p i) * c.m : ℕ) : ℝ) ≠ 0 := cast_ne_zero.mpr h4pm_pos.ne'    have hsum_pos : (0 : ℝ) < ((4 * ∏ i, c.p i) * c.m : ℕ) + c.r := by positivity    field_simp    simp_all  have h1_sub_pos : (0 : ℝ) < 1 - (4 : ℝ) * (∏ i, c.p i) / (∏ i, c.q i) := by    rw [sub_pos, div_lt_one hprod_q_pos_R]; exact_mod_cast c.prod_p_le_prod_q  have hsub_lt : 1 - (4 : ℝ) * (∏ i, c.p i) / (∏ i, c.q i) <      1 - (c.r : ℝ) / (∏ i, c.q i) := by gcongr; exact_mod_cast c.r_le  rw [hLM_eq']  have hinv := one_div_lt_one_div_of_lt h1_sub_pos hsub_lt  simp only [one_div] at hinv  convert hinv using 2