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
c : PullbackCone f g
h : IsLimit c
⊢ PullbackCone.fst c =
    (Iso.refl c.pt).hom ≫
      PullbackCone.fst
        (PullbackCone.mk (PullbackCone.fst c) (PullbackCone.snd c)
          (_ : PullbackCone.fst c ≫ f = PullbackCone.snd c ≫ g))
aesop_cat
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
c : PullbackCone f g
h : IsLimit c
⊢ PullbackCone.snd c =
    (Iso.refl c.pt).hom ≫
      PullbackCone.snd
        (PullbackCone.mk (PullbackCone.fst c) (PullbackCone.snd c)
          (_ : PullbackCone.fst c ≫ f = PullbackCone.snd c ≫ g))
aesop_cat