-- Mathlib/CategoryTheory/Limits/Indization/FilteredColimits.lean
theorem isFiltered [IsFiltered I] (hF : ∀ i, IsIndObject (F.obj i)) :
    IsFiltered (CostructuredArrow yoneda (colimit F))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
⊢ ∀ (j j' : Jᵒᵖ) (f : j ⟶ j'),
    (G.op ⋙ (toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))).map f
        ((fun j => Over.mkIdTerminal.from (Opposite.unop ((toOver yoneda (colimit F)).op.obj (G.op.obj j)))) j) =
      (fun j => Over.mkIdTerminal.from (Opposite.unop ((toOver yoneda (colimit F)).op.obj (G.op.obj j)))) j'

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Tactic:
obtain ⟨i, hi⟩ := exists_nonempty_limit_obj_of_isColimit F G _
  (colimit.isColimitToOver F) _ (Iso.refl _) h₁

Result:
case intro
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ toOver F (colimit F)).obj i)))
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Proof state:
case intro.mk'.intro
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Tactic:
obtain ⟨k, hk⟩ : ∃ k, Nonempty (limit (G.op ⋙ (toOver yoneda (colimit F)).op ⋙
    yoneda.obj ((toOver yoneda (colimit F)).obj <|
      (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

Result:
case intro.mk'.intro.intro
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        (toOver yoneda (colimit F)).op ⋙
          yoneda.obj
            ((toOver yoneda (colimit F)).obj
              ((pre P.F yoneda (colimit F)).obj
                ((map (colimit.ι F i)).obj (mk (P.cocone.toCostructuredArrow.obj k).hom))))))
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Proof state:
case intro
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ toOver F (colimit F)).obj i)))
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Tactic:
obtain ⟨⟨P⟩⟩ := hF i

Result:
case intro.mk'.intro
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Proof state:
case intro.mk'.intro
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Tactic:
let hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map _) (Over.isColimitToOver P.coconeIsColimit)

Result:
case intro.mk'.intro
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))