Lcm.Criterion.p_gt_two

lemma Criterion.p_gt_two (c : Criterion) (i : Fin 3) : 2 < c.p i := by  have h_pi_gt_two : ∀ i, 1 < c.p i := fun i ↦ Nat.Prime.one_lt (c.hp i)  by_contra h_contra  interval_cases _ : c.p i; iterate 2 grind  · have := c.h_ord_1; have := c.h_ord_2; have := c.h_ord_3; fin_cases i    · simp_all only [Fin.isValue, Fin.zero_eta, cast_ofNat]      rw [Real.sqrt_lt] at * <;> norm_cast at * <;>      linarith [h_pi_gt_two 0, h_pi_gt_two 1, h_pi_gt_two 2, 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)]    · grind [c.hp_mono (show 0 < 1 by decide) , c.hp_mono (show 1 < 2 by decide)]    · grind [h_pi_gt_two 0, h_pi_gt_two 1, h_pi_gt_two 2, c.hp_mono (show 0 < 1 by decide),        c.hp_mono (show 1 < 2 by decide)]