R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ : J ∣ I
hK : K ∣ I
⊢ J * K ∣ I
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), J ≤ P → K ≤ P → ¬IsPrime P
hJ : I ≤ J
hK : I ≤ K
⊢ I ≤ J * K
simp only [← Ideal.dvd_iff_le] at coprime hJ hK ⊢
case pos
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ : J ∣ I
hK : K ∣ I
hJ0 : J = 0
⊢ J * K ∣ I

case neg
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ : J ∣ I
hK : K ∣ I
hJ0 : ¬J = 0
⊢ J * K ∣ I
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ : J ∣ I
hK : K ∣ I
⊢ J * K ∣ I
by_cases hJ0 : J = 0
case neg.intro
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ J * K ∣ K * I'
case neg
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ : J ∣ I
hK : K ∣ I
hJ0 : ¬J = 0
⊢ J * K ∣ I
obtain ⟨I', rfl⟩ := hK
case neg.intro
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ K * J ∣ K * I'
case neg.intro
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ J * K ∣ K * I'
rw [mul_comm]
case neg.intro
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ ∀ {d : Ideal R}, d ∣ J → d ∣ K → ¬Prime d
case neg.intro
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ K * J ∣ K * I'
refine mul_dvd_mul_left K
  (UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors (b := K) hJ0 ?_ hJ)
no goals
case neg.intro
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ0 : ¬J = 0
I' : Ideal R
hJ : J ∣ K * I'
⊢ ∀ {d : Ideal R}, d ∣ J → d ∣ K → ¬Prime d
exact fun hPJ hPK => mt Ideal.isPrime_of_prime (coprime _ hPJ hPK)
no goals
case pos
R : Type u_1
A : Type ?u.1183773
K✝ : Type ?u.1183776
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬IsPrime P
hJ : J ∣ I
hK : K ∣ I
hJ0 : J = 0
⊢ J * K ∣ I
simpa only [hJ0, MulZeroClass.zero_mul] using hJ