LeanPool.DirectedTopologyLean4.PushoutAlternative #
theorem
PushoutAlternative.isPushout_alternative
{X X₁ X₂ X₀ : CategoryTheory.Cat}
{i₁ : X₀ ⟶ X₁}
{i₂ : X₀ ⟶ X₂}
{j₁ : X₁ ⟶ X}
{j₂ : X₂ ⟶ X}
(h_comm : CategoryTheory.CategoryStruct.comp i₁ j₁ = CategoryTheory.CategoryStruct.comp i₂ j₂)
(h_uniq :
∀ (C : CategoryTheory.Cat) (F₁ : X₁ ⟶ C) (F₂ : X₂ ⟶ C),
CategoryTheory.CategoryStruct.comp i₁ F₁ = CategoryTheory.CategoryStruct.comp i₂ F₂ →
∃! F : X ⟶ C, CategoryTheory.CategoryStruct.comp j₁ F = F₁ ∧ CategoryTheory.CategoryStruct.comp j₂ F = F₂)
:
CategoryTheory.IsPushout i₁ i₂ j₁ j₂