no goals
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map pushout.inl ≫ (iso G f g).inv = pushout.inl
simp [PreservesPushout.iso, Iso.comp_inv_eq]