R : Type ?u.797297
A : Type u_1
K : Type ?u.797303
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hP : P ≠ ⊥
h : IsPrime P
I J : Ideal A
hIJ : P ∣ I * J
⊢ P ∣ I ∨ P ∣ J
R : Type ?u.797297
A : Type u_1
K : Type ?u.797303
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hP : P ≠ ⊥
h : IsPrime P
⊢ Prime P
refine ⟨hP, mt Ideal.isUnit_iff.mp h.ne_top, fun I J hIJ => ?_⟩
no goals
R : Type ?u.797297
A : Type u_1
K : Type ?u.797303
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hP : P ≠ ⊥
h : IsPrime P
I J : Ideal A
hIJ : P ∣ I * J
⊢ P ∣ I ∨ P ∣ J
simpa only [Ideal.dvd_iff_le] using h.mul_le.mp (Ideal.le_of_dvd hIJ)