∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  {Z_1 : D} (h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (G.map f) (G.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inr f g)) h