by_cases hps : p ∈ s
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
⊢ False
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∈ s
⊢ False

case neg
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
⊢ False