∀ {C₁ : Type u_6} {C₂ : Type u_4} {C₃ : Type u_2} [inst : CategoryTheory.Category.{u_5, u_6} C₁]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} C₂] [inst_2 : CategoryTheory.Category.{u_1, u_2} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂), CategoryTheory.IsPushout ((F.obj X₁).map f₂) ((F.map f₁).app X₂) sq.inr sq.inl