awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v, v₁, u, u₁} C D
inst_3 : L.IsLeftAdjoint
⊢ IsCofiltered.{v₁, u₁} D

Tactic:
of_left_adjoint (Adjunction.ofIsLeftAdjoint L)

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.IsCofiltered.of_left_adjoint
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
h : Equivalence.{v, v₁, u, u₁} C D
⊢ IsCofiltered.{v₁, u₁} D

Tactic:
of_left_adjoint h.toAdjunction

Premises used: CategoryTheory.IsCofiltered.of_left_adjoint, CategoryTheory.Equivalence.toAdjunction
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
e : Equivalence.{v, v₁, u, u₁} C D
⊢ IsCofiltered.{v, u} C ↔ IsCofiltered.{v₁, u₁} D

Tactic:
⟨fun _ ↦ .of_equivalence e, fun _ ↦ .of_equivalence e.symm⟩

Premises used: Iff.intro, CategoryTheory.Equivalence.symm, CategoryTheory.IsCofiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
⊢ IsCofiltered.{v, u} C

Tactic:
have : IsCofiltered C := { nonempty := ⟨i⟩ }
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered.{v, u} C
intro : ∀ (val : Fintype I), ∃ (k : C) (fki : k ⟶ i) (g : (x : I) → k ⟶ j x), ∀ (x : I), g x ≫ f x = fki
⊢ ∃ (k : C) (fki : k ⟶ i) (g : (x : I) → k ⟶ j x), ∀ (x : I), g x ≫ f x = fki

Tactic:
cases nonempty_fintype I

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered.{v, u} C
val : Fintype I
x : I
⊢ j x ∈ insert i (Finset.image j Finset.univ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered.{v, u} C
val : Fintype I
x : I
⊢ i ∈ insert i (Finset.image j Finset.univ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered.{v, u} C
val : Fintype I
intro :
  ∀ (k : C) (fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (k ⟶ X))
    (hk :
      ∀ {X Y : C} (mX : X ∈ insert i (Finset.image j Finset.univ)) (mY : Y ∈ insert i (Finset.image j Finset.univ))
        {f_1 : X ⟶ Y},
        Membership.mem (γ :=
            Finset
              ((X : C) ×'
                (Y : C) ×'
                  (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                    (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)))
            (Finset.image
              (fun (x : I) ↦
                PSigma.mk (β := fun (X : C) ↦
                  (Y : C) ×'
                    (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                      (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
                  (j x)
                  (PSigma.mk (β := fun (Y : C) ↦
                    (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×'
                      (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (j x ⟶ Y))
                    i
                    (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦
                      (_ : i ∈ insert i (Finset.image j Finset.univ)) ×' (j x ⟶ i)) ⋯
                      (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦ j x ⟶ i) ⋯ (f x)))))
              Finset.univ)
            (PSigma.mk (β := fun (X : C) ↦
              (Y : C) ×'
                (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
              X
              (PSigma.mk (β := fun (Y : C) ↦
                (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
                Y
                (PSigma.mk (β := fun (x : X ∈ insert i (Finset.image j Finset.univ)) ↦
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ insert i (Finset.image j Finset.univ)) ↦ X ⟶ Y) mY f_1)))) →
          fk mX ≫ f_1 = fk mY),
    ∃ (k : C) (fki : k ⟶ i) (g : (x : I) → k ⟶ j x), ∀ (x : I), g x ≫ f x = fki
⊢ ∃ (k : C) (fki : k ⟶ i) (g : (x : I) → k ⟶ j x), ∀ (x : I), g x ≫ f x = fki

Tactic:
obtain ⟨k, fk, hk⟩ := IsCofiltered.inf_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨j x, i, by simp, by simp, f x⟩)

Premises used: Finset.univ, Insert.insert, PSigma.mk, Finset.image, CategoryTheory.IsCofiltered.inf_exists
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered.{v, u} C
val : Fintype I
k : C
fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (k ⟶ X)
hk :
  ∀ {X Y : C} (mX : X ∈ insert i (Finset.image j Finset.univ)) (mY : Y ∈ insert i (Finset.image j Finset.univ))
    {f_1 : X ⟶ Y},
    Membership.mem (γ :=
        Finset
          ((X : C) ×'
            (Y : C) ×'
              (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)))
        (Finset.image
          (fun (x : I) ↦
            PSigma.mk (β := fun (X : C) ↦
              (Y : C) ×'
                (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
              (j x)
              (PSigma.mk (β := fun (Y : C) ↦
                (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (j x ⟶ Y))
                i
                (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦
                  (_ : i ∈ insert i (Finset.image j Finset.univ)) ×' (j x ⟶ i)) ⋯
                  (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦ j x ⟶ i) ⋯ (f x)))))
          Finset.univ)
        (PSigma.mk (β := fun (X : C) ↦
          (Y : C) ×'
            (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
              (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
          X
          (PSigma.mk (β := fun (Y : C) ↦
            (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
              (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
            Y
            (PSigma.mk (β := fun (x : X ∈ insert i (Finset.image j Finset.univ)) ↦
              (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ insert i (Finset.image j Finset.univ)) ↦ X ⟶ Y) mY f_1)))) →
      fk mX ≫ f_1 = fk mY
⊢ ∃ (k : C) (fki : k ⟶ i) (g : (x : I) → k ⟶ j x), ∀ (x : I), g x ≫ f x = fki

Tactic:
⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩

Premises used: Finset.mem_univ, congrArg, true_or, Finset.mem_image._simp_1, Exists, exists_apply_eq_apply._simp_1, funext, And, congr, eq_self, Exists.intro, PSigma.mk, of_eq_true, Finset.mem_univ._simp_1, congrFun', Or, Finset.mem_insert._simp_1, Finset.mem_image_of_mem, or_true, Eq, true_and, Eq.trans
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered.{v, u} C
val : Fintype I
k : C
fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (k ⟶ X)
hk :
  ∀ {X Y : C} (mX : X ∈ insert i (Finset.image j Finset.univ)) (mY : Y ∈ insert i (Finset.image j Finset.univ))
    {f_1 : X ⟶ Y},
    Membership.mem (γ :=
        Finset
          ((X : C) ×'
            (Y : C) ×'
              (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)))
        (Finset.image
          (fun (x : I) ↦
            PSigma.mk (β := fun (X : C) ↦
              (Y : C) ×'
                (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
              (j x)
              (PSigma.mk (β := fun (Y : C) ↦
                (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (j x ⟶ Y))
                i
                (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦
                  (_ : i ∈ insert i (Finset.image j Finset.univ)) ×' (j x ⟶ i)) ⋯
                  (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦ j x ⟶ i) ⋯ (f x)))))
          Finset.univ)
        (PSigma.mk (β := fun (X : C) ↦
          (Y : C) ×'
            (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
              (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
          X
          (PSigma.mk (β := fun (Y : C) ↦
            (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
              (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
            Y
            (PSigma.mk (β := fun (x : X ∈ insert i (Finset.image j Finset.univ)) ↦
              (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ insert i (Finset.image j Finset.univ)) ↦ X ⟶ Y) mY f_1)))) →
      fk mX ≫ f_1 = fk mY
⊢ ∃ (k : C) (fki : k ⟶ i) (g : (x : I) → k ⟶ j x), ∀ (x : I), g x ≫ f x = fki

Tactic:
exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered.{v, u} C
intro : ∀ (val : Fintype I), ∃ (k : C) (fki : k ⟶ i) (g : (x : I) → k ⟶ j x), ∀ (x : I), g x ≫ f x = fki
intro₁ :
  ∀ (val : Fintype I) (k : C) (fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (k ⟶ X))
    (hk :
      ∀ {X Y : C} (mX : X ∈ insert i (Finset.image j Finset.univ)) (mY : Y ∈ insert i (Finset.image j Finset.univ))
        {f_1 : X ⟶ Y},
        Membership.mem (γ :=
            Finset
              ((X : C) ×'
                (Y : C) ×'
                  (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                    (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)))
            (Finset.image
              (fun (x : I) ↦
                PSigma.mk (β := fun (X : C) ↦
                  (Y : C) ×'
                    (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                      (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
                  (j x)
                  (PSigma.mk (β := fun (Y : C) ↦
                    (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×'
                      (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (j x ⟶ Y))
                    i
                    (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦
                      (_ : i ∈ insert i (Finset.image j Finset.univ)) ×' (j x ⟶ i)) ⋯
                      (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦ j x ⟶ i) ⋯ (f x)))))
              Finset.univ)
            (PSigma.mk (β := fun (X : C) ↦
              (Y : C) ×'
                (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
              X
              (PSigma.mk (β := fun (Y : C) ↦
                (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
                Y
                (PSigma.mk (β := fun (x : X ∈ insert i (Finset.image j Finset.univ)) ↦
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ insert i (Finset.image j Finset.univ)) ↦ X ⟶ Y) mY f_1)))) →
          fk mX ≫ f_1 = fk mY),
    ∃ (k : C) (fki : k ⟶ i) (g : (x : I) → k ⟶ j x), ∀ (x : I), g x ≫ f x = fki
⊢ ∃ (k : C) (fki : k ⟶ i) (g : (x : I) → k ⟶ j x), ∀ (x : I), g x ≫ f x = fki

Tactic:
classical
  cases nonempty_fintype I
  obtain ⟨k, fk, hk⟩ := IsCofiltered.inf_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨j x, i, by simp, by simp, f x⟩)
  exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
obtain : ∀ (c : Cone.{w, v, w, u} (Functor.empty C)), Nonempty C
⊢ Nonempty C

Tactic:
obtain ⟨c⟩ := h (Functor.empty _)

Premises used: CategoryTheory.Functor.empty
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
c : Cone.{w, v, w, u} (Functor.empty C)
⊢ Nonempty C

Tactic:
⟨c.pt⟩

Premises used: CategoryTheory.Limits.Cone.pt, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
c : Cone.{w, v, w, u} (Functor.empty C)
⊢ Nonempty C

Tactic:
exact ⟨c.pt⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
⊢ Nonempty C

Tactic:
have : Nonempty C := by
    obtain ⟨c⟩ := h (Functor.empty _)
    exact ⟨c.pt⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
⊢ IsCofilteredOrEmpty.{v, u} C

Tactic:
⟨?_, ?_⟩

Premises used: CategoryTheory.IsCofilteredOrEmpty.mk
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
refine_1 : ∀ (X Y : C), ∃ (W : C) (x : W ⟶ X) (x : W ⟶ Y), True
refine_2 : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ (W : C) (h : W ⟶ X), h ≫ f = h ≫ g
⊢ IsCofilteredOrEmpty.{v, u} C

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
refine_1 :
  ∀ (c : Cone.{w, v, w, u} (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)), ∃ (W : C) (x : W ⟶ X) (x : W ⟶ Y), True
⊢ ∃ (W : C) (x : W ⟶ X) (x : W ⟶ Y), True

Tactic:
obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ULift.downFunctor, CategoryTheory.ULiftHom.down, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
c : Cone.{w, v, w, u} (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
⊢ ∃ (W : C) (x : W ⟶ X) (x : W ⟶ Y), True

Tactic:
⟨c.pt, c.π.app ⟨⟨WalkingPair.left⟩⟩, c.π.app ⟨⟨WalkingPair.right⟩⟩, trivial⟩

Premises used: CategoryTheory.Limits.Cone.π, trivial, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.Cone.pt, CategoryTheory.Discrete.mk, Exists.intro, ULift.up, CategoryTheory.Limits.WalkingPair.left, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
c : Cone.{w, v, w, u} (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
⊢ ∃ (W : C) (x : W ⟶ X) (x : W ⟶ Y), True

Tactic:
exact ⟨c.pt, c.π.app ⟨⟨WalkingPair.left⟩⟩, c.π.app ⟨⟨WalkingPair.right⟩⟩, trivial⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
refine_2 : ∀ (c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)), ∃ (W : C) (h : W ⟶ X), h ≫ f = h ≫ g
⊢ ∃ (W : C) (h : W ⟶ X), h ≫ f = h ≫ g

Tactic:
obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ULift.downFunctor, CategoryTheory.ULiftHom.down, CategoryTheory.Limits.parallelPair
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ (W : C) (h : W ⟶ X), h ≫ f = h ≫ g

Tactic:
⟨c.pt, c.π.app ⟨WalkingParallelPair.zero⟩, ?_⟩

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.Cone.pt, Exists.intro, ULift.up, CategoryTheory.NatTrans.app, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
refine_2 :
  Eq (α := c.pt ⟶ Y) (c.π.app { down := WalkingParallelPair.zero } ≫ f : c.pt ⟶ Y)
    (c.π.app { down := WalkingParallelPair.zero } ≫ g : c.pt ⟶ Y)
⊢ ∃ (W : C) (h : W ⟶ X), h ≫ f = h ≫ g

Tactic:
refine ⟨c.pt, c.π.app ⟨WalkingParallelPair.zero⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.left } ≫
      c.π.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.π.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
        { down := WalkingParallelPairHom.left :
          ULift.{w, 0}
            (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
              ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) }

Tactic:
have h₁ := c.π.naturality ⟨WalkingParallelPairHom.left⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.left } ≫
      c.π.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.π.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
        { down := WalkingParallelPairHom.left :
          ULift.{w, 0}
            (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
              ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) }
⊢ Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.right } ≫
      c.π.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.π.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
        { down := WalkingParallelPairHom.right :
          ULift.{w, 0}
            (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
              ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) }

Tactic:
have h₂ := c.π.naturality ⟨WalkingParallelPairHom.right⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.left } ≫
      c.π.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.π.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
        { down := WalkingParallelPairHom.left :
          ULift.{w, 0}
            (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
              ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) }
h₂ :
  Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.right } ≫
      c.π.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.π.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
        { down := WalkingParallelPairHom.right :
          ULift.{w, 0}
            (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
              ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) }
⊢ Eq (α := c.pt ⟶ Y) (c.π.app { down := WalkingParallelPair.zero } ≫ f : c.pt ⟶ Y)
    (c.π.app { down := WalkingParallelPair.zero } ≫ g : c.pt ⟶ Y)

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
⊢ IsCofilteredOrEmpty.{v, u} C

Tactic:
have : IsCofilteredOrEmpty C := by
    refine ⟨?_, ?_⟩
    · intro X Y
      obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
      exact ⟨c.pt, c.π.app ⟨⟨WalkingPair.left⟩⟩, c.π.app ⟨⟨WalkingPair.right⟩⟩, trivial⟩
    · intro X Y f g
      obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
      refine ⟨c.pt, c.π.app ⟨WalkingParallelPair.zero⟩, ?_⟩
      have h₁ := c.π.naturality ⟨WalkingParallelPairHom.left⟩
      have h₂ := c.π.naturality ⟨WalkingParallelPairHom.right⟩
      simp_all
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this_1 : Nonempty C
this : IsCofilteredOrEmpty.{v, u} C
⊢ IsCofiltered.{v, u} C

Tactic:
apply IsCofiltered.mk

Premises used: CategoryTheory.IsCofiltered.mk