C : Type u₁
inst✝¹ : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr (_ : f ≫ inl = g ≫ inr), isColimit := isColimit h }).hom =
    inr
C : Type u₁
inst✝¹ : Category C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr ≫ (isoPushout h).inv = inr
dsimp [isoPushout, cocone, CommSq.cocone]
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
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk inl inr (_ : f ≫ inl = g ≫ inr), isColimit := isColimit h }).hom =
    inr
simp