obtain ⟨Q, _, hQ⟩ := Ideal.exists_ideal_over_prime_of_isIntegral p ⊥
  (by rw [Ideal.comap_bot_of_injective _
    (NoZeroSMulDivisors.algebraMap_injective R S)]; exact bot_le)
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
⊢ (primesOver S p).Nonempty
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