rw [← hP.2, hP', ← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
hP' : P = ⊥
⊢ p = ⊥
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
hP' : P = ⊥
⊢ Function.Injective ⇑(algebraMap R S)