R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ prod (map (RingHom.fst S R) (map (↑RingEquiv.prodComm) (prod I J)))
      (map (RingHom.snd S R) (map (↑RingEquiv.prodComm) (prod I J))) =
    prod J I
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ map (↑RingEquiv.prodComm) (prod I J) = prod J I
refine' Trans.trans (ideal_prod_eq _) _
no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ prod (map (RingHom.fst S R) (map (↑RingEquiv.prodComm) (prod I J)))
      (map (RingHom.snd S R) (map (↑RingEquiv.prodComm) (prod I J))) =
    prod J I
simp [map_map]