no goals
C : Type u₁
inst✝¹ : Category C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (isoPullback h).inv ≫ snd = pullback.snd
simp [Iso.inv_comp_eq]