intro h
case mp
n p : ℕ
hp : p.Prime
⊢ p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p → p ≤ n
case mp
n p : ℕ
hp : p.Prime
h : p ∣ ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1)), p
⊢ p ≤ n