no goals
R✝ : Type u
ι : Type ?u.297281
inst✝² : CommSemiring R✝
I✝ J✝ K L : Ideal R✝
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R
h : I = ⊥ ∨ J = ⊥
⊢ I * J = ⊥
cases' h with h h <;> rw [← Ideal.mul_bot, h, Ideal.mul_comm]