awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteLimits F
inst_3 : PreservesFiniteColimits F
⊢ (of F).obj (P := exactFunctor C D) = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteLimits F
⊢ Functor.obj (forget C D) (of F) = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteColimits F
⊢ Functor.obj (forget C D) (of F) = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteLimits F
inst_3 : PreservesFiniteColimits F
⊢ Functor.obj (forget C D) (of F) = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ PreservesFiniteLimits (F.obj (P := leftExactFunctor C D))

Tactic:
F.property

Premises used: CategoryTheory.leftExactFunctor, CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ PreservesFiniteColimits (F.obj (P := rightExactFunctor C D))

Tactic:
F.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ PreservesFiniteLimits (F.obj (P := exactFunctor C D))

Tactic:
F.property.1

Premises used: CategoryTheory.leftExactFunctor, CategoryTheory.ObjectProperty.FullSubcategory.property, And.left
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ PreservesFiniteColimits (F.obj (P := exactFunctor C D))

Tactic:
F.property.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, And.right, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
G : LeftExactFunctor.{v₂, v₃, u₂, u₃} D E
dsimp : leftExactFunctor C E (F.obj (P := leftExactFunctor C D) ⋙ G.obj (P := leftExactFunctor D E))
⊢ leftExactFunctor C E
    (Functor.obj (forget D E ⋙ Functor.obj (Functor.whiskeringLeft C D E) (F.obj (P := leftExactFunctor C D))) G)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
G : LeftExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ leftExactFunctor C E (F.obj (P := leftExactFunctor C D) ⋙ G.obj (P := leftExactFunctor D E))

Tactic:
comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.leftExactFunctor, CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
G : LeftExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ leftExactFunctor C E (F.obj (P := leftExactFunctor C D) ⋙ G.obj (P := leftExactFunctor D E))

Tactic:
exact comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : LeftExactFunctor.{v₂, v₃, u₂, u₃} D E
G : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
dsimp : leftExactFunctor C E (G.obj (P := leftExactFunctor C D) ⋙ F.obj (P := leftExactFunctor D E))
⊢ leftExactFunctor C E
    (Functor.obj (forget C D ⋙ Functor.obj (Functor.whiskeringRight C D E) (F.obj (P := leftExactFunctor D E))) G)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : LeftExactFunctor.{v₂, v₃, u₂, u₃} D E
G : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ leftExactFunctor C E (G.obj (P := leftExactFunctor C D) ⋙ F.obj (P := leftExactFunctor D E))

Tactic:
comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.leftExactFunctor, CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : LeftExactFunctor.{v₂, v₃, u₂, u₃} D E
G : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ leftExactFunctor C E (G.obj (P := leftExactFunctor C D) ⋙ F.obj (P := leftExactFunctor D E))

Tactic:
exact comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
G : RightExactFunctor.{v₂, v₃, u₂, u₃} D E
dsimp : rightExactFunctor C E (F.obj (P := rightExactFunctor C D) ⋙ G.obj (P := rightExactFunctor D E))
⊢ rightExactFunctor C E
    (Functor.obj (forget D E ⋙ Functor.obj (Functor.whiskeringLeft C D E) (F.obj (P := rightExactFunctor C D))) G)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
G : RightExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ rightExactFunctor C E (F.obj (P := rightExactFunctor C D) ⋙ G.obj (P := rightExactFunctor D E))

Tactic:
comp_preservesFiniteColimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
G : RightExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ rightExactFunctor C E (F.obj (P := rightExactFunctor C D) ⋙ G.obj (P := rightExactFunctor D E))

Tactic:
exact comp_preservesFiniteColimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : RightExactFunctor.{v₂, v₃, u₂, u₃} D E
G : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
dsimp : rightExactFunctor C E (G.obj (P := rightExactFunctor C D) ⋙ F.obj (P := rightExactFunctor D E))
⊢ rightExactFunctor C E
    (Functor.obj (forget C D ⋙ Functor.obj (Functor.whiskeringRight C D E) (F.obj (P := rightExactFunctor D E))) G)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : RightExactFunctor.{v₂, v₃, u₂, u₃} D E
G : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ rightExactFunctor C E (G.obj (P := rightExactFunctor C D) ⋙ F.obj (P := rightExactFunctor D E))

Tactic:
comp_preservesFiniteColimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : RightExactFunctor.{v₂, v₃, u₂, u₃} D E
G : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ rightExactFunctor C E (G.obj (P := rightExactFunctor C D) ⋙ F.obj (P := rightExactFunctor D E))

Tactic:
exact comp_preservesFiniteColimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
G : ExactFunctor.{v₂, v₃, u₂, u₃} D E
dsimp : leftExactFunctor C E (F.obj (P := exactFunctor C D) ⋙ G.obj (P := exactFunctor D E))
⊢ leftExactFunctor C E
    (Functor.obj (forget D E ⋙ Functor.obj (Functor.whiskeringLeft C D E) (F.obj (P := exactFunctor C D))) G)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
G : ExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ leftExactFunctor C E (F.obj (P := exactFunctor C D) ⋙ G.obj (P := exactFunctor D E))

Tactic:
comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.leftExactFunctor, CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
G : ExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ leftExactFunctor C E (F.obj (P := exactFunctor C D) ⋙ G.obj (P := exactFunctor D E))

Tactic:
exact comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
G : ExactFunctor.{v₂, v₃, u₂, u₃} D E
dsimp : rightExactFunctor C E (F.obj (P := exactFunctor C D) ⋙ G.obj (P := exactFunctor D E))
⊢ rightExactFunctor C E
    (Functor.obj (forget D E ⋙ Functor.obj (Functor.whiskeringLeft C D E) (F.obj (P := exactFunctor C D))) G)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
G : ExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ rightExactFunctor C E (F.obj (P := exactFunctor C D) ⋙ G.obj (P := exactFunctor D E))

Tactic:
comp_preservesFiniteColimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
G : ExactFunctor.{v₂, v₃, u₂, u₃} D E
⊢ rightExactFunctor C E (F.obj (P := exactFunctor C D) ⋙ G.obj (P := exactFunctor D E))

Tactic:
exact comp_preservesFiniteColimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₂, v₃, u₂, u₃} D E
G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
dsimp : leftExactFunctor C E (G.obj (P := exactFunctor C D) ⋙ F.obj (P := exactFunctor D E))
⊢ leftExactFunctor C E
    (Functor.obj (forget C D ⋙ Functor.obj (Functor.whiskeringRight C D E) (F.obj (P := exactFunctor D E))) G)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₂, v₃, u₂, u₃} D E
G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ leftExactFunctor C E (G.obj (P := exactFunctor C D) ⋙ F.obj (P := exactFunctor D E))

Tactic:
comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.leftExactFunctor, CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₂, v₃, u₂, u₃} D E
G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ leftExactFunctor C E (G.obj (P := exactFunctor C D) ⋙ F.obj (P := exactFunctor D E))

Tactic:
exact comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₂, v₃, u₂, u₃} D E
G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
dsimp : rightExactFunctor C E (G.obj (P := exactFunctor C D) ⋙ F.obj (P := exactFunctor D E))
⊢ rightExactFunctor C E
    (Functor.obj (forget C D ⋙ Functor.obj (Functor.whiskeringRight C D E) (F.obj (P := exactFunctor D E))) G)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₂, v₃, u₂, u₃} D E
G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ rightExactFunctor C E (G.obj (P := exactFunctor C D) ⋙ F.obj (P := exactFunctor D E))

Tactic:
comp_preservesFiniteColimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Limits.ExactFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : ExactFunctor.{v₂, v₃, u₂, u₃} D E
G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ rightExactFunctor C E (G.obj (P := exactFunctor C D) ⋙ F.obj (P := exactFunctor D E))

Tactic:
exact comp_preservesFiniteColimits _ _

Premises used: CategoryTheory.Limits.comp_preservesFiniteColimits
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
rw :
  (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
⊢ IsFiltered.{v, u} C ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))

Tactic:
rw [IsFiltered.iff_cocone_nonempty.{v}]
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
⊢ (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))

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

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
refine_1 :
  ∀ (h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) (J : Type v)
    (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
refine_2 :
  ∀
    (h :
      ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
        ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X)))
    (J : Type v) (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C), Nonempty (Cocone F)
⊢ (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))

Tactic:
refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
refine_1 : ∀ (c : Cocone F), ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
⊢ ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))

Tactic:
obtain ⟨c⟩ := h F
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
c : Cocone F
⊢ ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))

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

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.limitCompYonedaIsoCocone, Nonempty.intro, CategoryTheory.Limits.Cocone.ι, Exists.intro, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
c : Cocone F
⊢ ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))

Tactic:
exact ⟨c.pt, ⟨(limitCompYonedaIsoCocone F c.pt).inv c.ι⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
refine_2 : ∀ (pt : C) (ι : limit (F.op ⋙ Functor.obj yoneda pt)), Nonempty (Cocone F)
⊢ Nonempty (Cocone F)

Tactic:
obtain ⟨pt, ⟨ι⟩⟩ := h F
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
pt : C
ι : limit (F.op ⋙ Functor.obj yoneda pt)
⊢ Nonempty (Cocone F)

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

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Limits.limitCompYonedaIsoCocone, Nonempty.intro, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
pt : C
ι : limit (F.op ⋙ Functor.obj yoneda pt)
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨⟨pt, (limitCompYonedaIsoCocone F pt).hom ι⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
rw :
  (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
⊢ IsCofiltered.{v, u} C ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))

Tactic:
rw [IsCofiltered.iff_cone_nonempty.{v}]
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
⊢ (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))

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

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
refine_1 :
  ∀ (h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) (J : Type v)
    (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
refine_2 :
  ∀
    (h :
      ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
        ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X))))
    (J : Type v) (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C), Nonempty (Cone F)
⊢ (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))

Tactic:
refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
refine_1 : ∀ (c : Cone F), ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
⊢ ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))

Tactic:
obtain ⟨c⟩ := h F
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
c : Cone F
⊢ ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))

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

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Cone.pt, Nonempty.intro, Exists.intro, CategoryTheory.Limits.limitCompCoyonedaIsoCone, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
c : Cone F
⊢ ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))

Tactic:
exact ⟨c.pt, ⟨(limitCompCoyonedaIsoCone F c.pt).inv c.π⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
refine_2 : ∀ (pt : C) (π : limit (F ⋙ Functor.obj coyoneda (op pt))), Nonempty (Cone F)
⊢ Nonempty (Cone F)

Tactic:
obtain ⟨pt, ⟨π⟩⟩ := h F
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
pt : C
π : limit (F ⋙ Functor.obj coyoneda (op pt))
⊢ Nonempty (Cone F)

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

Premises used: CategoryTheory.ConcreteCategory.hom, Nonempty.intro, CategoryTheory.Limits.limitCompCoyonedaIsoCone, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Limits.Cone.mk
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
pt : C
π : limit (F ⋙ Functor.obj coyoneda (op pt))
⊢ Nonempty (Cone F)

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