isColimit — Mathlib

Lean4
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` are composable morphisms,
then the cokernel of `φ f g : X ⊞ Y ⟶ Y ⊞ Z` identifies
to `cokernel (f ≫ g)`. -/
noncomputable def isColimit : IsColimit (CokernelCofork.ofπ _ (φ_π f g)) :=
  CokernelCofork.IsColimit.ofπ' _ _
    (fun {A} k hk ↦ by
      refine ⟨cokernel.desc _ (biprod.inr ≫ k) ?_, ?_⟩
      all_goals
        obtain ⟨k₁, k₂, rfl⟩ := biprod.decomp_hom_from k
        simp only [comp_add, φ_snd_assoc, biprod.ext_from_iff, inl_φ_assoc, BinaryBicone.inl_fst_assoc,
          BinaryBicone.inl_snd_assoc, zero_comp, add_zero, comp_zero, inr_φ_fst_assoc, neg_comp, id_comp,
          BinaryBicone.inr_snd_assoc, neg_add_eq_zero] at hk
        obtain ⟨hk, rfl⟩ := hk
        aesop)
Похожие утверждения