R : Type u
ι : Type ?u.273517
inst✝ : CommSemiring R
I J K L : Ideal R
h : J ⊔ K = ⊤
⊢ I * K ⊔ J = I ⊔ J
R : Type u
ι : Type ?u.273517
inst✝ : CommSemiring R
I J K L : Ideal R
h : K ⊔ J = ⊤
⊢ I * K ⊔ J = I ⊔ J
rw [sup_comm] at h
no goals
R : Type u
ι : Type ?u.273517
inst✝ : CommSemiring R
I J K L : Ideal R
h : J ⊔ K = ⊤
⊢ I * K ⊔ J = I ⊔ J
rw [sup_comm, sup_mul_eq_of_coprime_right h, sup_comm]