-- Mathlib/CategoryTheory/Limits/Indization/FilteredColimits.lean
theorem exists_nonempty_limit_obj_of_colimit [IsFiltered K]
    (h : Nonempty <| limit <| 𝒢 ⋙ yoneda.obj (colimit H)) :
    ∃ k, Nonempty <| limit <| 𝒢 ⋙ yoneda.obj (H.obj k)

Proof state:
case intro
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
t₂ : limit
  (colimit
    (H ⋙
      yoneda ⋙
        (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj (G.op ⋙ (toOver yoneda (colimit F)).op))) :=
  limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom t
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
let t₃ := (colimitLimitIso (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢).flip).inv t₂

Result:
case intro
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
t₂ : limit
  (colimit
    (H ⋙
      yoneda ⋙
        (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj (G.op ⋙ (toOver yoneda (colimit F)).op))) :=
  limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom t
t₃ : colimit
  (limit
    (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
            (G.op ⋙ (toOver yoneda (colimit F)).op)).flip) :=
  (colimitLimitIso
        (H ⋙
            yoneda ⋙
              (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                (G.op ⋙ (toOver yoneda (colimit F)).op)).flip).inv
    t₂
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
h : Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H)))
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
obtain ⟨t⟩ := h

Result:
case intro
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Proof state:
case intro.intro.intro
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
t₂ : limit
  (colimit
    (H ⋙
      yoneda ⋙
        (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj (G.op ⋙ (toOver yoneda (colimit F)).op))) :=
  limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom t
t₃ : colimit
  (limit
    (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
            (G.op ⋙ (toOver yoneda (colimit F)).op)).flip) :=
  (colimitLimitIso
        (H ⋙
            yoneda ⋙
              (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                (G.op ⋙ (toOver yoneda (colimit F)).op)).flip).inv
    t₂
k : K
y✝ :
  (limit
        (H ⋙
            yoneda ⋙
              (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                (G.op ⋙ (toOver yoneda (colimit F)).op)).flip).obj
    k
z : limit
  ((H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj (G.op ⋙ (toOver yoneda (colimit F)).op)).flip ⋙
    (evaluation K (Type (max u v))).obj k) :=
  (limitObjIsoLimitCompEvaluation
        (H ⋙
            yoneda ⋙
              (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                (G.op ⋙ (toOver yoneda (colimit F)).op)).flip
        k).hom
    y✝
y : (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj (G.op ⋙ (toOver yoneda (colimit F)).op)).flip ⋙
    (evaluation K (Type (max u v))).obj k ≅
  (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj (G.op ⋙ (toOver yoneda (colimit F)).op)).obj
    k :=
  flipCompEvaluation
    (H ⋙
      yoneda ⋙ (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj (G.op ⋙ (toOver yoneda (colimit F)).op))
    k
⊢ limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k))

Tactic:
exact (lim.mapIso y).hom z

Result:
no goals

Proof state:
case intro
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
let t₂ := limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom t

Result:
case intro
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
t₂ : limit
  (colimit
    (H ⋙
      yoneda ⋙
        (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj (G.op ⋙ (toOver yoneda (colimit F)).op))) :=
  limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom t
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))