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

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 (Cocone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
c : Cocone F
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
exact ⟨c.pt, ⟨(limitCompYonedaIsoCocone F c.pt).inv c.ι⟩⟩

Result:
no goals

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

Tactic:
rw [IsFiltered.iff_cocone_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 (Cocone F)) ↔
    ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C),
      ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

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 (Cocone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj 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 (Cocone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
c : Cocone F
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ (∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔
    ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C),
      ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj 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 (Cocone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj 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.op ⋙ yoneda.obj X))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cocone F)

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.op ⋙ yoneda.obj X))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cocone 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.op ⋙ yoneda.obj X))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
pt : C
ι : limit (F.op ⋙ yoneda.obj pt)
⊢ Nonempty (Cocone 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.op ⋙ yoneda.obj X))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
pt : C
ι : limit (F.op ⋙ yoneda.obj pt)
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨⟨pt, (limitCompYonedaIsoCocone F pt).hom ι⟩⟩

Result:
no goals