rw [Finset.mem_filter, Finset.mem_range] at hq
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : q ∈ Finset.filter Nat.Prime (Finset.range (n + 1)) ∧ p ∣ q
⊢ p ≤ n
case mp.intro
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
h' : ∃ i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p ∣ i := Prime.exists_mem_finset_dvd (Nat.Prime.prime hp) h
q : ℕ
hq : (q < n + 1 ∧ q.Prime) ∧ p ∣ q
⊢ p ≤ n