Lcm.Criterion.val_p_L'

lemma Criterion.val_p_L' (c : Criterion) (i : Fin 3) : (c.L').factorization (c.p i) = 1 := by  have h_pi_factor : Nat.factorization (L c.n) (c.p i) = 1 := by    have h_prime_factor : ∀ {p : ℕ}, Nat.Prime p → Real.sqrt c.n < p → p < c.n →        (Nat.factorization (L c.n)) p = 1 := @fun p hp hp_sqrt hp_lt_n ↦ by      have h_prime_factor : (Nat.factorization (L c.n)) p = 1 := by        have h_prime_factor_def : (Nat.factorization (L c.n)) p = Finset.sup (Finset.Icc 1 c.n)            (fun i ↦ Nat.factorization i p) := by          have h_prime_factor_def : (Nat.factorization (Finset.lcm (Finset.Icc 1 c.n) (fun i ↦ i)))              p = Finset.sup (Finset.Icc 1 c.n) (fun i ↦ Nat.factorization i p) := by            have h_lcm_factorization : ∀ {S : Finset ℕ}, (∀ i ∈ S, i ≠ 0) →                (Nat.factorization (Finset.lcm S (fun i ↦ i))) p =                Finset.sup S (fun i ↦ Nat.factorization i p) := by              intros S hS_nonzero              induction S using Finset.induction with              | empty => simp [Finset.lcm]              | insert i S hiS ih =>                  by_cases hi : i = 0                  · simp_all                  simp only [lcm_insert]                  erw [Nat.factorization_lcm] <;> simp_all            exact h_lcm_factorization fun i hi ↦ by linarith [Finset.mem_Icc.mp hi]          exact h_prime_factor_def        have h_prime_power : ∀ i ∈ Finset.Icc 1 c.n, Nat.factorization i p ≤ 1 := fun i hi ↦ by          have h_prime_power : p^2 > c.n := by            rw [Real.sqrt_lt] at hp_sqrt <;> norm_cast at * <;> nlinarith only [hp_sqrt, hp_lt_n]          exact le_of_not_gt fun h ↦ absurd (Nat.dvd_trans (pow_dvd_pow p h) (Nat.ordProj_dvd i p))            (Nat.not_dvd_of_pos_of_lt (Finset.mem_Icc.mp hi |>.1)            (by nlinarith [Finset.mem_Icc.mp hi |>.2]))        refine h_prime_factor_def.trans (le_antisymm (Finset.sup_le h_prime_power) ?_)        exact le_trans (by norm_num [hp]) (Finset.le_sup (f := fun i ↦ Nat.factorization i p)          (Finset.mem_Icc.mpr ⟨hp.pos, hp_lt_n.le⟩))      exact (Nat.add_right_cancel (congrFun (congrArg HAdd.hAdd ((h_prime_factor.symm))) p)).symm    apply h_prime_factor (c.hp i) (c.h_ord_1.trans_le (by      exact_mod_cast c.hp_mono.monotone (Nat.zero_le _))) (by        have := c.h_ord_2; have := c.h_ord_3; fin_cases i <;> linarith! [c.hp_mono <|          show 0 < 1 by decide, c.hp_mono <| show 1 < 2 by decide, c.hq_mono <|          show 0 < 1 by decide, c.hq_mono <| show 1 < 2 by decide])  have h_pi_factor_L' : Nat.factorization (L c.n) (c.p i) = Nat.factorization (c.L')      (c.p i) + Nat.factorization (∏ i, c.q i) (c.p i) := by    have h_pi_factor_L' : Nat.factorization (L c.n) = Nat.factorization (c.L') +        Nat.factorization (∏ i, c.q i) := by      rw [← Nat.factorization_mul] <;> norm_num [c.L'_pos.ne']      · rw [mul_comm, Criterion.L_eq_prod_q_mul_L']      · exact Finset.prod_ne_zero_iff.mpr fun i _ ↦ Nat.Prime.ne_zero (c.hq i)    aesop  have h_pi_not_div_q : ∀ j, ¬(c.p i ∣ c.q j) := by    intro j hj; have := c.hq j; have := c.hp i; simp_all only [Nat.prime_dvd_prime_iff_eq]    have := c.h_ord_2; have := c.h_ord_3; fin_cases i <;> fin_cases j <;> linarith! [c.hp_mono <|      show 0 < 1 by decide, c.hp_mono <| show 1 < 2 by decide, c.hq_mono <|      show 0 < 1 by decide, c.hq_mono <| show 1 < 2 by decide]  simp_all [Fin.prod_univ_three,Nat.factorization_mul,Nat.Prime.ne_zero (c.hq _),    Nat.factorization_eq_zero_of_not_dvd (h_pi_not_div_q _)]