no goals
C : Type u₁
inst✝ : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : PushoutCocone f g
h : IsColimit c
⊢ PushoutCocone.inl c ≫ (Iso.refl c.pt).hom =
    PushoutCocone.inl
      (PushoutCocone.mk (PushoutCocone.inl c) (PushoutCocone.inr c)
        (_ : f ≫ PushoutCocone.inl c = g ≫ PushoutCocone.inr c))
aesop_cat
no goals
C : Type u₁
inst✝ : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
c : PushoutCocone f g
h : IsColimit c
⊢ PushoutCocone.inr c ≫ (Iso.refl c.pt).hom =
    PushoutCocone.inr
      (PushoutCocone.mk (PushoutCocone.inl c) (PushoutCocone.inr c)
        (_ : f ≫ PushoutCocone.inl c = g ≫ PushoutCocone.inr c))
aesop_cat