Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: 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 ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.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 ⋙
        (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
          yoneda.obj
            ((CostructuredArrow.toOver yoneda (colimit F)).obj
              ((pre P.F yoneda (colimit F)).obj
                ((CostructuredArrow.map (colimit.ι F i)).obj
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
htO : (CostructuredArrow.toOver yoneda (colimit F)).FullyFaithful
q : (X : CostructuredArrow yoneda (colimit F)) →
  (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj ((CostructuredArrow.toOver yoneda (colimit F)).obj X) ≅
    uliftYoneda.{max u v, v, max u v}.obj X :=
  fun X ↦
    (CostructuredArrow.toOver yoneda (colimit F)).op.isoWhiskerLeft
        (uliftYonedaIsoYoneda.symm.app ((CostructuredArrow.toOver yoneda (colimit F)).obj X)) ≪≫
      htO.homNatIso X
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

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

Goal state after:
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 ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.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 ⋙
        (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
          yoneda.obj
            ((CostructuredArrow.toOver yoneda (colimit F)).obj
              ((pre P.F yoneda (colimit F)).obj
                ((CostructuredArrow.map (colimit.ι F i)).obj
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
htO : (CostructuredArrow.toOver yoneda (colimit F)).FullyFaithful
q : (X : CostructuredArrow yoneda (colimit F)) →
  (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj ((CostructuredArrow.toOver yoneda (colimit F)).obj X) ≅
    uliftYoneda.{max u v, v, max u v}.obj X :=
  fun X ↦
    (CostructuredArrow.toOver yoneda (colimit F)).op.isoWhiskerLeft
        (uliftYonedaIsoYoneda.symm.app ((CostructuredArrow.toOver yoneda (colimit F)).obj X)) ≪≫
      htO.homNatIso X
t' :
  limit
    (G.op ⋙
      uliftYoneda.{max u v, v, max u v}.obj
        ((pre P.F yoneda (colimit F)).obj
          ((CostructuredArrow.map (colimit.ι F i)).obj
            (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))