{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFiltered C] →
      (O : Finset C) →
        (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) →
          {X : C} → X ∈ O → (X ⟶ CategoryTheory.IsFiltered.sup O H)