awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
J : Type w
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{w, v, w, u} J C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun (X : J) ↦
    Finset.biUnion Finset.univ fun (Y : J) ↦
      Finset.image
        (fun (f : X ⟶ Y) ↦
          PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
            (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
              (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) ⋯
                (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) ⋯ (F.map f)))))
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
        H →
      f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
a :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj j)
      (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj j ∈ O) ×' (_ : Y ∈ O) ×' (F.obj j ⟶ Y)) (F.obj j')
        (PSigma.mk (β := fun (x : F.obj j ∈ O) ↦ (_ : F.obj j' ∈ O) ×' (F.obj j ⟶ F.obj j')) ⋯
          (PSigma.mk (β := fun (x : F.obj j' ∈ O) ↦ F.obj j ⟶ F.obj j') ⋯ (F.map g)))) ∈
    H
⊢ F.map g ≫ f ⋯ = f ⋯

Tactic:
apply w
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
J : Type w
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{w, v, w, u} J C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun (X : J) ↦
    Finset.biUnion Finset.univ fun (Y : J) ↦
      Finset.image
        (fun (f : X ⟶ Y) ↦
          PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
            (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
              (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) ⋯
                (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) ⋯ (F.map f)))))
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
        H →
      f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ HEq (α :=
    (Y : C) ×'
      (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ×' (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ Y))
    (PSigma.mk (β := fun (Y : C) ↦
      (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ×' (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ Y))
      (F.obj j')
      (PSigma.mk (β := fun (x : F.obj j ∈ Finset.image F.obj Finset.univ) ↦
        (_ : F.obj j' ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ F.obj j')) ⋯
        (PSigma.mk (β := fun (x : F.obj j' ∈ Finset.image F.obj Finset.univ) ↦ F.obj j ⟶ F.obj j') ⋯ (F.map g))))
    (β :=
    (Y : C) ×'
      (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ×' (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ Y))
    (PSigma.mk (β := fun (Y : C) ↦
      (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ×' (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ Y))
      (F.obj j')
      (PSigma.mk (β := fun (x : F.obj j ∈ Finset.image F.obj Finset.univ) ↦
        (_ : F.obj j' ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ F.obj j')) ⋯
        (PSigma.mk (β := fun (x : F.obj j' ∈ Finset.image F.obj Finset.univ) ↦ F.obj j ⟶ F.obj j') ⋯ (F.map g))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
J : Type w
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{w, v, w, u} J C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun (X : J) ↦
    Finset.biUnion Finset.univ fun (Y : J) ↦
      Finset.image
        (fun (f : X ⟶ Y) ↦
          PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
            (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
              (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) ⋯
                (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) ⋯ (F.map f)))))
        Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
        H →
      f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ ∃ (a : J),
    F.obj a = F.obj j ∧
      ∃ (x : J) (x_1 : a ⟶ x),
        HEq (α :=
          (Y : C) ×'
            (_ : F.obj a ∈ Finset.image F.obj Finset.univ) ×' (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj a ⟶ Y))
          (PSigma.mk (β := fun (Y : C) ↦
            (_ : F.obj a ∈ Finset.image F.obj Finset.univ) ×' (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj a ⟶ Y))
            (F.obj x)
            (PSigma.mk (β := fun (x_2 : F.obj a ∈ Finset.image F.obj Finset.univ) ↦
              (_ : F.obj x ∈ Finset.image F.obj Finset.univ) ×' (F.obj a ⟶ F.obj x)) ⋯
              (PSigma.mk (β := fun (x_2 : F.obj x ∈ Finset.image F.obj Finset.univ) ↦ F.obj a ⟶ F.obj x) ⋯
                (F.map x_1))))
          (β :=
          (Y : C) ×'
            (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ×' (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ Y))
          (PSigma.mk (β := fun (Y : C) ↦
            (_ : F.obj j ∈ Finset.image F.obj Finset.univ) ×' (_ : Y ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ Y))
            (F.obj j')
            (PSigma.mk (β := fun (x : F.obj j ∈ Finset.image F.obj Finset.univ) ↦
              (_ : F.obj j' ∈ Finset.image F.obj Finset.univ) ×' (F.obj j ⟶ F.obj j')) ⋯
              (PSigma.mk (β := fun (x : F.obj j' ∈ Finset.image F.obj Finset.univ) ↦ F.obj j ⟶ F.obj j') ⋯ (F.map g))))

Tactic:
exact ⟨j, rfl, j', g, by simp⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v₁, v, u₁, u} D C
R : Functor.{v, v₁, u, u₁} C D
h : L ⊣ R
⊢ IsFiltered.{v₁, u₁} D

Tactic:
{ IsFilteredOrEmpty.of_right_adjoint h with
    nonempty := IsFiltered.nonempty.map R.obj }

Premises used: CategoryTheory.IsFiltered.mk, CategoryTheory.IsFilteredOrEmpty.of_right_adjoint
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
R : Functor.{v, v₁, u, u₁} C D
inst_3 : R.IsRightAdjoint
⊢ IsFiltered.{v₁, u₁} D

Tactic:
of_right_adjoint (Adjunction.ofIsRightAdjoint R)

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

Tactic:
of_right_adjoint h.symm.toAdjunction

Premises used: CategoryTheory.IsFiltered.of_right_adjoint, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Equivalence.symm
-- 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
⊢ IsFiltered.{v, u} C ↔ IsFiltered.{v₁, u₁} D

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

Premises used: CategoryTheory.IsFiltered.of_equivalence, Iff.intro, CategoryTheory.Equivalence.symm
-- 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 (Cocone F)
obtain : ∀ (c : Cocone.{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 (Cocone F)
c : Cocone.{w, v, w, u} (Functor.empty C)
⊢ Nonempty C

Tactic:
⟨c.pt⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.Cocone.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 (Cocone F)
c : Cocone.{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 (Cocone 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 (Cocone F)
this : Nonempty C
⊢ IsFilteredOrEmpty.{v, u} C

Tactic:
⟨?_, ?_⟩

Premises used: CategoryTheory.IsFilteredOrEmpty.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 (Cocone F)
this : Nonempty C
refine_1 : ∀ (X Y : C), ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), True
refine_2 : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ IsFilteredOrEmpty.{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 (Cocone F)
this : Nonempty C
X Y : C
refine_1 :
  ∀ (c : Cocone.{w, v, w, u} (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)), ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), True
⊢ ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), 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 (Cocone F)
this : Nonempty C
X Y : C
c : Cocone.{w, v, w, u} (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
⊢ ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), True

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

Premises used: trivial, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Cocone.ι, Exists.intro, ULift.up, CategoryTheory.Limits.WalkingPair.left, CategoryTheory.NatTrans.app, CategoryTheory.Limits.Cocone.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 (Cocone F)
this : Nonempty C
X Y : C
c : Cocone.{w, v, w, u} (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
⊢ ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), 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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
refine_2 : ∀ (c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)), ∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ ∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h

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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h

Tactic:
⟨c.pt, c.ι.app ⟨WalkingParallelPair.one⟩, ?_⟩

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.Cocone.ι, Exists.intro, ULift.up, CategoryTheory.NatTrans.app, CategoryTheory.Limits.Cocone.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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
refine_2 :
  Eq (α := X ⟶ c.pt) (f ≫ c.ι.app { down := WalkingParallelPair.one }) (g ≫ c.ι.app { down := WalkingParallelPair.one })
⊢ ∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h

Tactic:
refine ⟨c.pt, c.ι.app ⟨WalkingParallelPair.one⟩, ?_⟩
-- 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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ (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 }) } ≫
      c.ι.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.ι.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.left }

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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  (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 }) } ≫
      c.ι.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.ι.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.left }
⊢ (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 }) } ≫
      c.ι.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.ι.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.right }

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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  (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 }) } ≫
      c.ι.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.ι.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.left }
h₂ :
  (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 }) } ≫
      c.ι.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.ι.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.right }
⊢ Eq (α := X ⟶ c.pt) (f ≫ c.ι.app { down := WalkingParallelPair.one }) (g ≫ c.ι.app { down := WalkingParallelPair.one })

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 (Cocone F)
this : Nonempty C
⊢ IsFilteredOrEmpty.{v, u} C

Tactic:
have : IsFilteredOrEmpty 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.one⟩, ?_⟩
      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 (Cocone F)
this_1 : Nonempty C
this : IsFilteredOrEmpty.{v, u} C
⊢ IsFiltered.{v, u} C

Tactic:
apply IsFiltered.mk

Premises used: CategoryTheory.IsFiltered.mk
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
⊢ IsFiltered.{v, u} C

Tactic:
of_cocone_nonempty.{v} C fun F => ⟨colimit.cocone F⟩

Premises used: Nonempty.intro, CategoryTheory.IsFiltered.of_cocone_nonempty, CategoryTheory.Limits.colimit.cocone
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
⊢ IsFiltered.{v, u} C

Tactic:
of_isTerminal _ terminalIsTerminal

Premises used: CategoryTheory.IsFiltered.of_isTerminal, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsFiltered.{v, u} C ↔
    ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)

Tactic:
⟨fun _ _ _ _ F => cocone_nonempty F, of_cocone_nonempty C⟩

Premises used: CategoryTheory.IsFiltered.cocone_nonempty, CategoryTheory.IsFiltered.of_cocone_nonempty, Iff.intro
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ Eq (α := j₁ ⟶ coeq₃ f g h) (f ≫ coeq₃Hom f g h) (g ≫ coeq₃Hom f g h)

Tactic:
simp only [coeq₃Hom, ← Category.assoc, coeq_condition f g]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsFiltered.coeq₃Hom, CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
dsimp :
  Eq (α := j₁ ⟶ coeq₃ f g h)
    (g ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
    (h ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
⊢ Eq (α := j₁ ⟶ coeq₃ f g h) (g ≫ coeq₃Hom f g h) (h ≫ coeq₃Hom f g h)

Tactic:
dsimp [coeq₃Hom]

Premises used: CategoryTheory.IsFiltered.coeq₃Hom
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
a :
  (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
    coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
| coeqHom f g ≫
    leftToMax (coeq f g) (coeq g h) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))

Tactic:
rw [← Category.assoc, coeq_condition _ _]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
slice_lhs :
  Eq (α := j₁ ⟶ coeq₃ f g h)
    (g ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
    (h ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
⊢ Eq (α := j₁ ⟶ coeq₃ f g h)
    (g ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
    (h ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))

Tactic:
slice_lhs 2 4 => rw [← Category.assoc, coeq_condition _ _]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsFiltered.coeq_condition