no goals
C : Type u
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ pushout.inl ≫ (pushoutSymmetry f g).inv = pushout.inr
simp [Iso.comp_inv_eq]