-- Mathlib/CategoryTheory/Limits/Indization/FilteredColimits.lean
theorem isIndObject_colimit (I : Type v) [SmallCategory I] [IsFiltered I]
    (F : I ⥤ Cᵒᵖ ⥤ Type v) (hF : ∀ i, IsIndObject (F.obj i)) : IsIndObject (colimit F)

Proof state:
case intro.intro.intro.refine_2
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ 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)
j : (i : I) → 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 (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (colimit.ι F i).app (Opposite.op A.left) y
y' : CostructuredArrow yoneda (F.obj i) := mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ A ⟶ (map (colimit.ι F i)).obj y'

Tactic:
refine homMk (𝟙 A.left) (yonedaEquiv.injective ?_)

Result:
case intro.intro.intro.refine_2
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ 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)
j : (i : I) → 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 (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (colimit.ι F i).app (Opposite.op A.left) y
y' : CostructuredArrow yoneda (F.obj i) := mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ yonedaEquiv (yoneda.map (𝟙 A.left) ≫ ((map (colimit.ι F i)).obj y').hom) = yonedaEquiv A.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))

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

Result:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this✝ : IsFiltered (CostructuredArrow yoneda (colimit F))
this :
  ∀ (i : I),
    ∃ s, ∃ (_ : Small.{v, max u v} ↑s), ∀ (i_1 : CostructuredArrow yoneda (F.obj i)), ∃ j ∈ s, Nonempty (i_1 ⟶ j)
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))

Proof state:
case intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ 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)
j : (i : I) → 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 (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (colimit.ι F i).app (Opposite.op A.left) y
y' : CostructuredArrow yoneda (F.obj i) := mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ ∃ j ∈ ⋃ i, (map (colimit.ι F i)).obj '' s i, Nonempty (A ⟶ j)

Tactic:
refine ⟨(map (colimit.ι F i)).obj (j i y'), ?_, ⟨?_⟩⟩

Result:
case intro.intro.intro.refine_1
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ 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)
j : (i : I) → 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 (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (colimit.ι F i).app (Opposite.op A.left) y
y' : CostructuredArrow yoneda (F.obj i) := mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ (map (colimit.ι F i)).obj (j i y') ∈ ⋃ i, (map (colimit.ι F i)).obj '' s i

case intro.intro.intro.refine_2
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ 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)
j : (i : I) → 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 (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (colimit.ι F i).app (Opposite.op A.left) y
y' : CostructuredArrow yoneda (F.obj i) := mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ A ⟶ (map (colimit.ι F i)).obj (j i y')