Lcm.Criterion.val_p_M_ge_two

lemma Criterion.val_p_M_ge_two (c : Criterion) (i : Fin 3) : (c.M).factorization (c.p i) ≥ 2 := by  have h_pi_factorization_M : (Nat.factorization (c.M)) (c.p i) =      (Nat.factorization (4 * ∏ i, c.p i)) (c.p i) + (Nat.factorization (c.m)) (c.p i) +      (Nat.factorization (c.L')) (c.p i) := by    rw [show c.M = (4 * ∏ i, c.p i) * c.m * c.L' by          exact Nat.add_zero (((4 * ∏ i, c.p i) * c.m).mul c.L'), Nat.factorization_mul,            Nat.factorization_mul]    iterate 3 simp [Finset.prod_ne_zero_iff.mpr fun i _ ↦ Nat.Prime.ne_zero (c.hp i),      Nat.ne_of_gt (Criterion.m_pos c)]    · simp only [ne_eq, _root_.mul_eq_zero, OfNat.ofNat_ne_zero, false_or, not_or]      exact ⟨Finset.prod_ne_zero_iff.mpr fun i _ ↦ Nat.Prime.ne_zero (c.hp i),        Nat.ne_of_gt (c.m_pos)⟩    · exact Nat.ne_of_gt (Criterion.L'_pos c)  simp_all only [Finset.prod_eq_prod_sdiff_singleton_mul (Finset.mem_univ i),    ge_iff_le, val_p_L' c i, reduceLeDiff]  rw [Nat.factorization_mul] <;> norm_num  · rw [Nat.factorization_mul]    · exact le_add_of_le_of_nonneg (le_add_of_nonneg_of_le (Nat.zero_le _)        (Nat.one_le_iff_ne_zero.mpr <| by simp [c.hp i])) (Nat.zero_le _)    · simp only [ne_eq, prod_eq_zero_iff, mem_sdiff, mem_univ, mem_singleton, true_and,      not_exists, not_and]      exact fun x hx ↦ Nat.Prime.ne_zero (c.hp x)    · exact Nat.Prime.ne_zero (c.hp i)  · exact ⟨Finset.prod_ne_zero_iff.mpr fun j hj ↦ Nat.Prime.ne_zero (c.hp j),      Nat.Prime.ne_zero (c.hp i)⟩