isColimitOf' — Mathlib

Lean4
/-- Recognizing filtered colimits of types. The injectivity condition here is
slightly easier to check as compared to `isColimitOf`. -/
noncomputable def isColimitOf' (t : Cocone F) (hsurj : ∀ x : t.pt, ∃ i xi, x = t.ι.app i xi)
    (hinj : ∀ i x y, t.ι.app i x = t.ι.app i y → ∃ (k : _) (f : i ⟶ k), F.map f x = F.map f y) : IsColimit t :=
  isColimitOf _ _ hsurj
    (fun i j xi xj h ↦
      by
      obtain ⟨k, g, hg⟩ :=
        hinj (IsFiltered.max i j) (F.map (IsFiltered.leftToMax i j) xi) (F.map (IsFiltered.rightToMax i j) xj)
          (by simp [FunctorToTypes.naturality, h])
      exact ⟨k, IsFiltered.leftToMax i j ≫ g, IsFiltered.rightToMax i j ≫ g, by simpa using hg⟩)
Похожие утверждения