cases Nat.exists_prime_and_dvd this with
| intro p hp =>
  exists p
  have hu_pos : 0 < u
  . linarith
  have hpu : p ≤ u := Nat.le_of_dvd hu_pos hp.right
  apply And.intro
  . apply lt_of_le_of_lt hpu
    apply Nat.lt_add_of_pos_left
    apply PrimeRange.prodPos
  . apply And.intro
    . exact Nat.Prime.two_le hp.left
    . apply Nat.dvd_add _ hp.right
      apply PrimeRange.prodDvdOfLt hp.left
      linarith
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
no goals