awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ :
  Nonempty
    (limit (G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙ obj yoneda (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙
        obj yoneda (obj (colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)) i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit (C := Over (colimit F)) (F :=
  (P.cocone.toCostructuredArrow ⋙ CostructuredArrow.toOver (P.F ⋙ yoneda) P.cocone.pt) ⋙ Over.map (colimit.ι F i))
  (mapCocone (Over.map (colimit.ι F i)) P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
⊢ ∃ (k : P.I),
    Nonempty
      (limit
        (G.op ⋙
          Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙
            obj yoneda
              (obj (CostructuredArrow.toOver yoneda (colimit F))
                (obj (CostructuredArrow.pre P.F yoneda (colimit F))
                  (obj (CostructuredArrow.map (colimit.ι F i))
                    (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))

Tactic:
exists_nonempty_limit_obj_of_isColimit F G _ hc _ (Iso.refl _) hi

Premises used: CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_isColimit, CategoryTheory.Functor.op, Quiver.Hom.op, CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.Functor.id, CategoryTheory.Iso.refl, CategoryTheory.CostructuredArrow
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ :
  Nonempty
    (limit (G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙ obj yoneda (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙
        obj yoneda (obj (colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)) i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit (C := Over (colimit F)) (F :=
  (P.cocone.toCostructuredArrow ⋙ CostructuredArrow.toOver (P.F ⋙ yoneda) P.cocone.pt) ⋙ Over.map (colimit.ι F i))
  (mapCocone (Over.map (colimit.ι F i)) P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
obtain :
  ∀ (k : P.I)
    (hk :
      Nonempty
        (limit
          (G.op ⋙
            Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙
              obj yoneda
                (obj (CostructuredArrow.toOver yoneda (colimit F))
                  (obj (CostructuredArrow.pre P.F yoneda (colimit F))
                    (obj (CostructuredArrow.map (colimit.ι F i))
                      (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))),
    ∃ (X : CostructuredArrow yoneda (colimit F)), Nonempty.{v + 1} (limit (G.op ⋙ obj yoneda X))
⊢ ∃ (X : CostructuredArrow yoneda (colimit F)), Nonempty.{v + 1} (limit (G.op ⋙ obj yoneda X))

Tactic:
obtain ⟨k, hk⟩ : ∃ k, Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
      yoneda.obj ((CostructuredArrow.toOver yoneda (colimit F)).obj <|
        (CostructuredArrow.pre P.F yoneda (colimit F)).obj <|
          (map (colimit.ι F i)).obj <| mk _))) :=
    exists_nonempty_limit_obj_of_isColimit F G _ hc _ (Iso.refl _) hi

Premises used: CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.exists_nonempty_limit_obj_of_isColimit, CategoryTheory.Functor.op, CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.Iso.refl, CategoryTheory.Limits.colimit, CategoryTheory.Limits.limit, CategoryTheory.CostructuredArrow.toOver, Nonempty, CategoryTheory.CostructuredArrow.mk, CategoryTheory.CostructuredArrow.pre, CategoryTheory.Limits.IndObjectPresentation.F, CategoryTheory.CostructuredArrow.map, CategoryTheory.Functor.obj, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ :
  Nonempty
    (limit (G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙ obj yoneda (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙
        obj yoneda (obj (colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)) i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit (C := Over (colimit F)) (F :=
  (P.cocone.toCostructuredArrow ⋙ CostructuredArrow.toOver (P.F ⋙ yoneda) P.cocone.pt) ⋙ Over.map (colimit.ι F i))
  (mapCocone (Over.map (colimit.ι F i)) P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙
          obj yoneda
            (obj (CostructuredArrow.toOver yoneda (colimit F))
              (obj (CostructuredArrow.pre P.F yoneda (colimit F))
                (obj (CostructuredArrow.map (colimit.ι F i))
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
have :
  ∀ (htO : FullyFaithful (C := CostructuredArrow yoneda (colimit F)) (CostructuredArrow.toOver yoneda (colimit F))),
    ∃ (X : CostructuredArrow yoneda (colimit F)), Nonempty.{v + 1} (limit (G.op ⋙ obj yoneda X))
⊢ ∃ (X : CostructuredArrow yoneda (colimit F)), Nonempty.{v + 1} (limit (G.op ⋙ obj yoneda X))

Tactic:
have htO : (CostructuredArrow.toOver yoneda (colimit F)).FullyFaithful := .ofFullyFaithful _
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ :
  Nonempty
    (limit (G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙ obj yoneda (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙
        obj yoneda (obj (colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)) i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit (C := Over (colimit F)) (F :=
  (P.cocone.toCostructuredArrow ⋙ CostructuredArrow.toOver (P.F ⋙ yoneda) P.cocone.pt) ⋙ Over.map (colimit.ι F i))
  (mapCocone (Over.map (colimit.ι F i)) P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙
          obj yoneda
            (obj (CostructuredArrow.toOver yoneda (colimit F))
              (obj (CostructuredArrow.pre P.F yoneda (colimit F))
                (obj (CostructuredArrow.map (colimit.ι F i))
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
htO : FullyFaithful (C := CostructuredArrow yoneda (colimit F)) (CostructuredArrow.toOver yoneda (colimit F))
q : (X : CostructuredArrow yoneda (colimit F)) →
  Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙
      obj yoneda (obj (CostructuredArrow.toOver yoneda (colimit F)) X) ≅
    obj uliftYoneda.{max u v, v, max u v} X :=
  fun (X : CostructuredArrow yoneda (colimit F)) ↦
    isoWhiskerLeft (Functor.op (CostructuredArrow.toOver yoneda (colimit F)))
        (Iso.app (Iso.symm uliftYonedaIsoYoneda) (obj (CostructuredArrow.toOver yoneda (colimit F)) X)) ≪≫
      htO.homNatIso X
obtain :
  ∀
    (t' :
      limit
        (G.op ⋙
          obj uliftYoneda.{max u v, v, max u v}
            (obj (CostructuredArrow.pre P.F yoneda (colimit F))
              (obj (CostructuredArrow.map (colimit.ι F i))
                (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))),
    ∃ (X : CostructuredArrow yoneda (colimit F)), Nonempty.{v + 1} (limit (G.op ⋙ obj yoneda X))
⊢ ∃ (X : CostructuredArrow yoneda (colimit F)), Nonempty.{v + 1} (limit (G.op ⋙ obj yoneda X))

Tactic:
obtain ⟨t'⟩ := Nonempty.map (limMap (isoWhiskerLeft G.op (q _)).hom) hk

Premises used: CategoryTheory.Functor.op, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Limits.limMap, Nonempty.map, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ :
  Nonempty
    (limit (G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙ obj yoneda (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙
        obj yoneda (obj (colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)) i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit (C := Over (colimit F)) (F :=
  (P.cocone.toCostructuredArrow ⋙ CostructuredArrow.toOver (P.F ⋙ yoneda) P.cocone.pt) ⋙ Over.map (colimit.ι F i))
  (mapCocone (Over.map (colimit.ι F i)) P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙
          obj yoneda
            (obj (CostructuredArrow.toOver yoneda (colimit F))
              (obj (CostructuredArrow.pre P.F yoneda (colimit F))
                (obj (CostructuredArrow.map (colimit.ι F i))
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
htO : FullyFaithful (C := CostructuredArrow yoneda (colimit F)) (CostructuredArrow.toOver yoneda (colimit F))
q : (X : CostructuredArrow yoneda (colimit F)) →
  Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙
      obj yoneda (obj (CostructuredArrow.toOver yoneda (colimit F)) X) ≅
    obj uliftYoneda.{max u v, v, max u v} X :=
  fun (X : CostructuredArrow yoneda (colimit F)) ↦
    isoWhiskerLeft (Functor.op (CostructuredArrow.toOver yoneda (colimit F)))
        (Iso.app (Iso.symm uliftYonedaIsoYoneda) (obj (CostructuredArrow.toOver yoneda (colimit F)) X)) ≪≫
      htO.homNatIso X
t' :
  limit
    (G.op ⋙
      obj uliftYoneda.{max u v, v, max u v}
        (obj (CostructuredArrow.pre P.F yoneda (colimit F))
          (obj (CostructuredArrow.map (colimit.ι F i))
            (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))
⊢ ∃ (X : CostructuredArrow yoneda (colimit F)), Nonempty.{v + 1} (limit (G.op ⋙ obj yoneda X))

Tactic:
⟨_, ⟨((preservesLimitIso uliftFunctor.{max u v, v} _).inv t').down⟩⟩

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.uliftFunctor, Nonempty.intro, CategoryTheory.preservesLimitIso, Exists.intro, DFunLike.coe, ULift.down, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ :
  Nonempty
    (limit (G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙ obj yoneda (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙
        obj yoneda (obj (colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)) i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit (C := Over (colimit F)) (F :=
  (P.cocone.toCostructuredArrow ⋙ CostructuredArrow.toOver (P.F ⋙ yoneda) P.cocone.pt) ⋙ Over.map (colimit.ι F i))
  (mapCocone (Over.map (colimit.ι F i)) P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙
          obj yoneda
            (obj (CostructuredArrow.toOver yoneda (colimit F))
              (obj (CostructuredArrow.pre P.F yoneda (colimit F))
                (obj (CostructuredArrow.map (colimit.ι F i))
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
htO : FullyFaithful (C := CostructuredArrow yoneda (colimit F)) (CostructuredArrow.toOver yoneda (colimit F))
q : (X : CostructuredArrow yoneda (colimit F)) →
  Functor.op (CostructuredArrow.toOver yoneda (colimit F)) ⋙
      obj yoneda (obj (CostructuredArrow.toOver yoneda (colimit F)) X) ≅
    obj uliftYoneda.{max u v, v, max u v} X :=
  fun (X : CostructuredArrow yoneda (colimit F)) ↦
    isoWhiskerLeft (Functor.op (CostructuredArrow.toOver yoneda (colimit F)))
        (Iso.app (Iso.symm uliftYonedaIsoYoneda) (obj (CostructuredArrow.toOver yoneda (colimit F)) X)) ≪≫
      htO.homNatIso X
t' :
  limit
    (G.op ⋙
      obj uliftYoneda.{max u v, v, max u v}
        (obj (CostructuredArrow.pre P.F yoneda (colimit F))
          (obj (CostructuredArrow.map (colimit.ι F i))
            (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))
⊢ ∃ (X : CostructuredArrow yoneda (colimit F)), Nonempty.{v + 1} (limit (G.op ⋙ obj yoneda X))

Tactic:
exact ⟨_, ⟨((preservesLimitIso uliftFunctor.{max u v, v} _).inv t').down⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
⊢ IsFiltered (CostructuredArrow yoneda (colimit F))

Tactic:
have : IsFiltered (CostructuredArrow yoneda (colimit F)) :=
    IndizationClosedUnderFilteredColimitsAux.isFiltered F hF
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
⊢ IsIndObject (colimit F)

Tactic:
(isIndObject_iff _).mpr ⟨this, ?_⟩

Premises used: Iff.mpr, CategoryTheory.Limits.isIndObject_iff, And.intro
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
refine : FinallySmall (CostructuredArrow yoneda (colimit F))
⊢ IsIndObject (colimit F)

Tactic:
refine (isIndObject_iff _).mpr ⟨this, ?_⟩

Premises used: Iff.mpr, CategoryTheory.Limits.isIndObject_iff, And.intro
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
⊢ ∀ (i : I),
    ∃ (s : Set (CostructuredArrow yoneda (F.obj i))) (_ : Small.{v, max u v} (↑s : Type (max u v))),
      ∀ (i_1 : CostructuredArrow yoneda (F.obj i)), ∃ j ∈ s, Nonempty.{v + 1} (i_1 ⟶ j)

Tactic:
have : ∀ i, ∃ (s : Set (CostructuredArrow yoneda (F.obj i))) (_ : Small.{v} s),
      ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j) :=
    fun i => (hF i).finallySmall.exists_small_weakly_terminal_set
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this_1 : IsFiltered (CostructuredArrow yoneda (colimit F))
this :
  ∀ (i : I),
    ∃ (s : Set (CostructuredArrow yoneda (F.obj i))) (_ : Small.{v, max u v} (↑s : Type (max u v))),
      ∀ (i_1 : CostructuredArrow yoneda (F.obj i)), ∃ j ∈ s, Nonempty.{v + 1} (i_1 ⟶ j)
choose :
  ∀ (s : (i : I) → Set (CostructuredArrow yoneda (F.obj i)))
    (hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v)))
    (j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i))
    (hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i)
    (hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)),
    FinallySmall (CostructuredArrow yoneda (colimit F))
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))

Tactic:
choose s hs j hjs hj using this
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))

Tactic:
finallySmall_of_small_weakly_terminal_set
    (⋃ i, (map (colimit.ι F i)).obj '' (s i)) (fun A => ?_)

Premises used: CategoryTheory.finallySmall_of_small_weakly_terminal_set, Set.image, CategoryTheory.CostructuredArrow.map, Set.iUnion, CategoryTheory.Functor.obj, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
refine :
  ∀ (A : CostructuredArrow yoneda (colimit F)),
    ∃ (j : CostructuredArrow yoneda (colimit F)),
      Membership.mem (γ := Set (CostructuredArrow yoneda (colimit F)))
          (⋃ (i : I), obj (CostructuredArrow.map (colimit.ι F i)) '' s i) j ∧
        Nonempty.{v + 1} (A ⟶ j)
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))

Tactic:
refine finallySmall_of_small_weakly_terminal_set
    (⋃ i, (map (colimit.ι F i)).obj '' (s i)) (fun A => ?_)

Premises used: CategoryTheory.finallySmall_of_small_weakly_terminal_set, Set.image, CategoryTheory.CostructuredArrow.map, Set.iUnion, CategoryTheory.Functor.obj, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
obtain :
  ∀ (i : I) (y : (F.obj i).obj (Opposite.op A.left))
    (hy :
      Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
        ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
          (colimit F).obj (Opposite.op A.left))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
              (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
                (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
            y :
          (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))),
    ∃ (j : CostructuredArrow yoneda (colimit F)),
      Membership.mem (γ := Set (CostructuredArrow yoneda (colimit F)))
          (⋃ (i : I), obj (CostructuredArrow.map (colimit.ι F i)) '' s i) j ∧
        Nonempty.{v + 1} (A ⟶ j)
⊢ ∃ (j : CostructuredArrow yoneda (colimit F)),
    Membership.mem (γ := Set (CostructuredArrow yoneda (colimit F)))
        (⋃ (i : I), obj (CostructuredArrow.map (colimit.ι F i)) '' s i) j ∧
      Nonempty.{v + 1} (A ⟶ j)

Tactic:
obtain ⟨i, y, hy⟩ := FunctorToTypes.jointly_surjective'.{v, v} F _ (yonedaEquiv A.hom)
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
obtain :
  ∀ (x : y' ⟶ j i y'),
    ∃ (j : CostructuredArrow yoneda (colimit F)),
      Membership.mem (γ := Set (CostructuredArrow yoneda (colimit F)))
          (⋃ (i : I), obj (CostructuredArrow.map (colimit.ι F i)) '' s i) j ∧
        Nonempty.{v + 1} (A ⟶ j)
⊢ ∃ (j : CostructuredArrow yoneda (colimit F)),
    Membership.mem (γ := Set (CostructuredArrow yoneda (colimit F)))
        (⋃ (i : I), obj (CostructuredArrow.map (colimit.ι F i)) '' s i) j ∧
      Nonempty.{v + 1} (A ⟶ j)

Tactic:
obtain ⟨x⟩ := hj _ y'