isPushoutOfIsInitialIsCoproduct — Mathlib

Lean4
/-- The coproduct is the pushout under the initial object. -/
def isPushoutOfIsInitialIsCoproduct {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : IsInitial W)
    (H₂ : IsColimit (BinaryCofan.mk f g)) : IsColimit (PushoutCocone.mk _ _ (show h ≫ f = k ≫ g from H₁.hom_ext _ _)) :=
  by
  apply PushoutCocone.isColimitAux'
  intro s
  use H₂.desc (BinaryCofan.mk s.inl s.inr)
  use H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.left⟩
  use H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.right⟩
  intro m h₁ h₂
  apply H₂.hom_ext
  rintro ⟨⟨⟩⟩
  · exact h₁.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.left⟩).symm
  · exact h₂.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.right⟩).symm
Похожие утверждения