no goals
C : Type u
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝² : HasPushout f g
inst✝¹ : HasPushout pushout.inr g'
inst✝ : HasPushout f (g ≫ g')
⊢ pushout.inl ≫ pushout.inl ≫ (pushoutLeftPushoutInrIso f g g').hom = pushout.inl
rw [← Category.assoc, ← Iso.eq_comp_inv, inl_pushoutLeftPushoutInrIso_inv]