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
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd (_ : fst ≫ f = snd ≫ g), isLimit := isLimit h }).inv ≫
      pullback.snd =
    snd
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).hom ≫ pullback.snd = snd
dsimp [isoPullback, cone, CommSq.cone]
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
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd (_ : fst ≫ f = snd ≫ g), isLimit := isLimit h }).inv ≫
      pullback.snd =
    snd
simp