R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : Ideal.IsPrime p
hp0 : p ≠ ⊥
this : IsDomain S
⊢ ⊥ < Ideal.comap (algebraMap R S) p
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : Ideal.IsPrime p
hp0 : p ≠ ⊥
⊢ ⊥ < Ideal.comap (algebraMap R S) p
haveI : IsDomain S := isDomain_of_le_nonZeroDivisors _ hM
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : Ideal.IsPrime p
hp0 : p ≠ ⊥
this : IsDomain S
⊢ Ideal.comap (algebraMap R S) ⊥ < Ideal.comap (algebraMap R S) p
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : Ideal.IsPrime p
hp0 : p ≠ ⊥
this : IsDomain S
⊢ ⊥ < Ideal.comap (algebraMap R S) p
rw [← Ideal.comap_bot_of_injective (algebraMap R S) (IsLocalization.injective _ hM)]
no goals
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : Ideal.IsPrime p
hp0 : p ≠ ⊥
this : IsDomain S
⊢ Ideal.comap (algebraMap R S) ⊥ < Ideal.comap (algebraMap R S) p
convert (orderIsoOfPrime M S).lt_iff_lt.mpr (show (⟨⊥, Ideal.bot_prime⟩ :
  { p : Ideal S // p.IsPrime }) < ⟨p, hpp⟩ from hp0.bot_lt)