Lcm.Criterion.q_not_dvd_L'

@[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.q_not_dvd_L' (c : Criterion) : ∀ i, ¬(c.q i ∣ c.L') := by  intro i hqi  have hn_lt_q_sq := Real.lt_sq_of_sqrt_lt <| c.h_ord_1.trans_le <| cast_le.mpr <|    show c.p 0 ≤ c.q i by      grw [c.hp_mono.monotone <| Fin.zero_le 2, c.h_ord_2, c.hq_mono.monotone <| Fin.zero_le i]  norm_cast at hn_lt_q_sq  suffices ¬(c.q i) ^ 2 ∣ L c.n from this <| Nat.pow_two _ ▸ by    refine mul_dvd_mul_right (Finset.dvd_prod_of_mem c.q <| Finset.mem_univ i) _ |>.trans ?_    exact Fin.prod_univ_three c.q ▸ c.ln_eq ▸ mul_dvd_mul_left _ hqi   set p : ℕ := c.q i  have hp : Nat.Prime p := c.hq i   -- 1) prime power divides binary lcm iff divides one side  have pow_dvd_lcm_iff (a b k : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) :      p ^ k ∣ Nat.lcm a b ↔ (p ^ k ∣ a ∨ p ^ k ∣ b) := by    refine ⟨?_, by grind [dvd_trans, Nat.dvd_lcm_left, Nat.dvd_lcm_right]⟩    grind [Prime.pow_dvd_iff_le_factorization, lcm_ne_zero, Nat.factorization_lcm, Finsupp.sup_apply]   -- 2) prime power divides finset-lcm -> appears in some member  have exists_mem_of_pow_dvd_finset_lcm (s : Finset ℕ) (hs_nz : ∀ x ∈ s, x ≠ 0) (k)      (hk : 0 < k) (h : p ^ k ∣ s.lcm _root_.id) : ∃ m ∈ s, p ^ k ∣ m := by    induction s using Finset.induction with    | empty =>      have := one_lt_pow hk.ne' hp.one_lt |>.trans_le <| le_of_dvd zero_lt_one h      contradiction    | insert a s ha ih =>      have ha0 := hs_nz _ <| mem_insert_self a s      have hs_nz' := (hs_nz · <| mem_insert_of_mem ·)      have hs0 := lcm_ne_zero_iff.mpr hs_nz'      have := (pow_dvd_lcm_iff _ _ k ha0 hs0).1 <| by simpa using! h      rcases this with hpa | hps      · exact ⟨a, mem_insert_self a s, hpa⟩      · have ⟨m, hmS, hpm⟩ := ih hs_nz' hps        exact ⟨m, mem_insert_of_mem hmS, hpm⟩   intro hq2  have ⟨m, hmIcc, hpm⟩ := exists_mem_of_pow_dvd_finset_lcm _ (by grind) 2 zero_lt_two hq2  refine not_lt_of_ge ?_ hn_lt_q_sq  refine le_trans (le_of_dvd ?_ hpm) (Finset.mem_Icc.mp hmIcc).2  exact succ_le_iff.mp (Finset.mem_Icc.mp hmIcc).1