exact ⟨Q, hQ⟩
case intro.intro
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
Q : Ideal S
left✝ : Q ≥ ⊥
hQ : Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = p
⊢ (primesOver S p).Nonempty
no goals