no goals
C : Type u
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pullbackSymmetry f g).inv ≫ pullback.snd = pullback.fst
simp [Iso.inv_comp_eq]