∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y S T S' : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T)
  (i' : S' ⟶ S) [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i f))
      (CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i g))]
  [inst_4 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) g)],
  CategoryTheory.Limits.pushout.mapLift f g (CategoryTheory.CategoryStruct.comp i' i) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.congrHom ⋯ ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.mapLift (CategoryTheory.CategoryStruct.comp i f)
          (CategoryTheory.CategoryStruct.comp i g) i')
        (CategoryTheory.Limits.pushout.mapLift f g i))