Lcm.Criterion.not_highlyAbundant_2

@[blueprint  "lem:criterion-reduced"  (title := "Reduction to a lower bound for \\(\\sigma(M)/M\\)")  (statement := /--  If  \begin{equation}\label{eq:sigmaM-lower}    \frac{\sigma(M)}{M}    \;\ge\;    \frac{\sigma(L')}{L'}    \Biggl( \prod_{i=1}^3 \Bigl(1+\frac{1}{p_i(p_i+1)}\Bigr) \Biggr)    \Bigl(1 + \frac{3}{8n}\Bigr),  \end{equation}  then $L_n$ is not highly abundant.  -/)  (proof := /--  Insert \eqref{eq:sigmaM-lower} and \eqref{eq:sigmaLn} into the desired inequality and compare  with the assumed bound \eqref{eq:main-ineq}; this is a straightforward rearrangement.  -/)  (proofUses := ["lem:sigmaLn", "lem:criterion-sufficient"])  (latexEnv := "lemma")]theorem Criterion.not_highlyAbundant_2 (c : Criterion)    (h : σnorm c.M ≥ σnorm c.L' * (∏ i, (1 + 1 / (c.p i * (c.p i + 1 : ℝ)))) *    (1 + (3 : ℝ) / (8 * c.n))) : ¬HighlyAbundant (L c.n) := by  refine c.not_highlyAbundant_1 ?_  have hL'_pos : 0 < σnorm c.L' := by    rw [σnorm]; exact div_pos (cast_pos.mpr <| by rw [σ, sigma_pos_iff]; exact c.L'_pos)      (cast_pos.mpr c.L'_pos)  have hR_pos : (0 : ℝ) < 1 - 4 * (∏ i, c.p i) / (∏ i, c.q i) := by    rw [sub_pos, div_lt_one (cast_pos.mpr <| prod_pos fun i _ ↦ (c.hq i).pos)]    exact_mod_cast c.prod_p_le_prod_q  have hcrit : (∏ i, (1 + (1 : ℝ) / c.q i)) ≤ (∏ i, (1 + 1 / (c.p i * (c.p i + 1 : ℝ)))) *      (1 + 3 / (8 * c.n)) * (1 - (4 : ℝ) * (∏ i, c.p i) / (∏ i, c.q i)) := by    convert c.h_crit using 3; simp only [prod_natCast]  rw [c.σnorm_ln_eq]  calc σnorm c.L' * ∏ i, (1 + (1 : ℝ) / c.q i)    ≤ σnorm c.L' * ((∏ i, (1 + 1 / (c.p i * (c.p i + 1 : ℝ)))) * (1 + 3 / (8 * c.n)) *        (1 - (4 : ℝ) * (∏ i, c.p i) / (∏ i, c.q i))) :=          mul_le_mul_of_nonneg_left hcrit hL'_pos.le  _ = σnorm c.L' * (∏ i, (1 + 1 / (c.p i * (c.p i + 1 : ℝ)))) * (1 + 3 / (8 * c.n)) *    (1 - (4 : ℝ) * (∏ i, c.p i) / (∏ i, c.q i)) := by ring  _ ≤ σnorm c.M * (1 - (4 : ℝ) * (∏ i, c.p i) / (∏ i, c.q i)) :=    mul_le_mul_of_nonneg_right h hR_pos.le