-- Mathlib/CategoryTheory/Limits/Filtered.lean
theorem IsCofiltered.iff_nonempty_limit : IsCofiltered C ↔
    ∀ {J : Type v} [SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ IsCofiltered C ↔
    ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C),
      ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Tactic:
rw [IsCofiltered.iff_cone_nonempty.{v}]

Result:
C : Type u
inst✝ : Category.{v, u} C
⊢ (∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C),
      ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C),
    ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cone F)

Tactic:
obtain ⟨pt, ⟨π⟩⟩ := h F

Result:
case refine_2.intro.intro
C : Type u
inst✝ : Category.{v, u} C
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C),
    ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
pt : C
π : limit (F ⋙ coyoneda.obj (op pt))
⊢ Nonempty (Cone F)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ (∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C),
      ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Tactic:
refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

case refine_2
C : Type u
inst✝ : Category.{v, u} C
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C),
    ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cone F)

Proof state:
case refine_2.intro.intro
C : Type u
inst✝ : Category.{v, u} C
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C),
    ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
pt : C
π : limit (F ⋙ coyoneda.obj (op pt))
⊢ Nonempty (Cone F)

Tactic:
exact ⟨⟨pt, (limitCompCoyonedaIsoCone F pt).hom π⟩⟩

Result:
no goals

Proof state:
case refine_1.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
c : Cone F
⊢ ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Tactic:
exact ⟨c.pt, ⟨(limitCompCoyonedaIsoCone F c.pt).inv c.π⟩⟩

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Tactic:
obtain ⟨c⟩ := h F

Result:
case refine_1.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
c : Cone F
⊢ ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))