Lcm.Criterion.ln_eq

@[blueprint  "lem:Lprime-def"  (title := "Factorisation of \\(L_n\\)")  (statement := /--  There exists a positive integer \(L'\) such that  \[    L_n = q_1 q_2 q_3 \, L'  \]  and each prime \(q_i\) divides \(L_n\) exactly once and does not divide \(L'\).  -/)  (proof := /--  Since \(q_i < n\), the prime \(q_i\) divides \(L_n\) exactly once (as \(q_i^2 > n\)).  Hence we may write \(L_n = q_1 q_2 q_3 L'\) where \(L'\) is the quotient obtained by removing  these prime factors.  By construction, \(q_i \nmid L'\) for each \(i\).  -/)  (latexEnv := "lemma")]theorem Criterion.ln_eq (c : Criterion) : L c.n = c.q 0 * c.q 1 * c.q 2 * c.L' := by  rw [L', ← Fin.prod_univ_three, Nat.mul_div_cancel' <| Fintype.prod_dvd_of_isRelPrime ?_ ?_]  · refine fun i j h ↦ Nat.coprime_iff_isRelPrime.mp ?_    exact Nat.coprime_primes (c.hq i) (c.hq j) |>.mpr <| c.hq_mono.injective.ne h  refine fun i ↦    Finset.dvd_lcm <| Finset.mem_Icc.mpr ⟨c.hq i |>.one_le, le_trans ?_ c.h_ord_3.le⟩  exact c.hq_mono.monotone <| Fin.le_last i