no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I'✝ : Ideal R
J✝ J'✝ : Ideal S
I I' : Ideal R
J J' : Ideal S
⊢ prod I J = prod I' J' ↔ I = I' ∧ J = J'
simp only [← idealProdEquiv_symm_apply, idealProdEquiv.symm.injective.eq_iff, Prod.mk.inj_iff]