case refine_1
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
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
h : Prime P
⊢ P ≠ ⊤

case refine_2
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
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
h : Prime P
x✝ y✝ : A
hxy : x✝ * y✝ ∈ P
⊢ x✝ ∈ P ∨ y✝ ∈ P
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
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
h : Prime P
⊢ IsPrime P
refine ⟨?_, fun hxy => ?_⟩
case refine_1
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : Prime ⊤
⊢ False
case refine_1
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
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
h : Prime P
⊢ P ≠ ⊤
rintro rfl
case refine_1
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : Prime 1
⊢ False
case refine_1
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : Prime ⊤
⊢ False
rw [← Ideal.one_eq_top] at h
no goals
case refine_1
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : Prime 1
⊢ False
exact h.not_unit isUnit_one
case refine_2
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
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
h : Prime P
x✝ y✝ : A
hxy : P ∣ span {x✝} * span {y✝}
⊢ P ∣ span {x✝} ∨ P ∣ span {y✝}
case refine_2
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
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
h : Prime P
x✝ y✝ : A
hxy : x✝ * y✝ ∈ P
⊢ x✝ ∈ P ∨ y✝ ∈ P
simp only [← Ideal.dvd_span_singleton, ← Ideal.span_singleton_mul_span_singleton] at hxy ⊢
no goals
case refine_2
R : Type ?u.795002
A : Type u_1
K : Type ?u.795008
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
h : Prime P
x✝ y✝ : A
hxy : P ∣ span {x✝} * span {y✝}
⊢ P ∣ span {x✝} ∨ P ∣ span {y✝}
exact h.dvd_or_dvd hxy