no goals
C : Type u_2
inst✝³ : Category C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ coprod.inr ≫ (pushoutZeroZeroIso X Y).inv = pushout.inr
simp [Iso.comp_inv_eq]