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