∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
  CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ →
    CategoryTheory.CategoryStruct.comp h₂₁ v₂₂ = CategoryTheory.CategoryStruct.comp v₂₁ h₃₁ →
      (CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
          (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁ ↔
        CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁)