rw [primesOver_eq_empty_of_not_isPrime S p h]
case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : ¬p.IsPrime
⊢ (primesOver S p).Finite
case neg
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
h : ¬p.IsPrime
⊢ ∅.Finite