awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ j₄ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
f₄ : j₄ ⟶ k₁
g₄ : j₄ ⟶ k₂
s : C
α : k₁ ⟶ s
β : k₂ ⟶ s
H :
  ∀ (i : Fin (Nat.succ 0).succ.succ.succ),
    Eq (α := ![j₁, j₂, j₃, j₄] i ⟶ s)
      (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ.succ) ↦ ![j₁, j₂, j₃, j₄] i ⟶ k₁) f₁
            (Fin.cons (α := fun (i : Fin 3) ↦ ![j₁, j₂, j₃, j₄] i.succ ⟶ k₁) f₂
              (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ ⟶ k₁) f₃
                (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ.succ ⟶ k₁) f₄ fun (a : Fin 0) ↦
                  nomatch a)))
            i ≫
          α :
        ![j₁, j₂, j₃, j₄] i ⟶ s)
      (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ.succ) ↦ ![j₁, j₂, j₃, j₄] i ⟶ k₂) g₁
            (Fin.cons (α := fun (i : Fin 3) ↦ ![j₁, j₂, j₃, j₄] i.succ ⟶ k₂) g₂
              (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ ⟶ k₂) g₃
                (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ.succ ⟶ k₂) g₄ fun (a : Fin 0) ↦
                  nomatch a)))
            i ≫
          β :
        ![j₁, j₂, j₃, j₄] i ⟶ s)
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β ∧ f₄ ≫ α = g₄ ≫ β

Tactic:
exact ⟨s, α, β, H 0, H 1, H 2, H 3⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
obtain :
  ∀ (l' : C) (k₁l : k₁ ⟶ l') (k₂l : k₂ ⟶ l') (hl : f₂ ≫ k₁l = f₃ ≫ k₂l),
    ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β

Tactic:
obtain ⟨l', k₁l, k₂l, hl⟩ := span f₂ f₃

Premises used: CategoryTheory.IsFiltered.span
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
obtain :
  ∀ (s : C) (ls : l ⟶ s) (l's : l' ⟶ s) (hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's) (hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's),
    ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β

Tactic:
obtain ⟨s, ls, l's, hs₁, hs₂⟩ := bowtie g₁ (f₁ ≫ k₁l) g₂ (f₄ ≫ k₂l)

Premises used: CategoryTheory.IsFiltered.bowtie, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ f₂ ≫ k₁l ≫ l's = f₃ ≫ k₂l ≫ l's

Tactic:
simp only [← Category.assoc, hl]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
refine_1 : f₁ ≫ k₁l ≫ l's = g₁ ≫ ls
refine_2 : f₄ ≫ k₂l ≫ l's = g₂ ≫ ls
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β

Tactic:
refine ⟨s, k₁l ≫ l's, ls, k₂l ≫ l's, ?_, by simp only [← Category.assoc, hl], ?_⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ f₁ ≫ k₁l ≫ l's = g₁ ≫ ls

Tactic:
simp only [hs₁, hs₂, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ f₄ ≫ k₂l ≫ l's = g₂ ≫ ls

Tactic:
simp only [hs₁, hs₂, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
⊢ IsFiltered.{v, u} C

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

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 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{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 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{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 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{v, u} C
val : Fintype I
intro :
  ∀ (k : C) (fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (X ⟶ k))
    (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))
                  i
                  (PSigma.mk (β := fun (Y : C) ↦
                    (_ : i ∈ insert i (Finset.image j Finset.univ)) ×'
                      (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ Y))
                    (j x)
                    (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦
                      (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ j x)) ⋯
                      (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦ i ⟶ j x) ⋯ (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)))) →
          f_1 ≫ fk mY = fk mX),
    ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
⊢ ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik

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

Premises used: Finset.univ, Insert.insert, PSigma.mk, CategoryTheory.IsFiltered.sup_exists, Finset.image
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{v, u} C
val : Fintype I
k : C
fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (X ⟶ k)
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))
              i
              (PSigma.mk (β := fun (Y : C) ↦
                (_ : i ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ Y))
                (j x)
                (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦
                  (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ j x)) ⋯
                  (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦ i ⟶ j x) ⋯ (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)))) →
      f_1 ≫ fk mY = fk mX
⊢ ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik

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 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{v, u} C
val : Fintype I
k : C
fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (X ⟶ k)
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))
              i
              (PSigma.mk (β := fun (Y : C) ↦
                (_ : i ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ Y))
                (j x)
                (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦
                  (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ j x)) ⋯
                  (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦ i ⟶ j x) ⋯ (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)))) →
      f_1 ≫ fk mY = fk mX
⊢ ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik

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 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{v, u} C
intro : ∀ (val : Fintype I), ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
intro₁ :
  ∀ (val : Fintype I) (k : C) (fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (X ⟶ k))
    (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))
                  i
                  (PSigma.mk (β := fun (Y : C) ↦
                    (_ : i ∈ insert i (Finset.image j Finset.univ)) ×'
                      (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ Y))
                    (j x)
                    (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦
                      (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ j x)) ⋯
                      (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦ i ⟶ j x) ⋯ (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)))) →
          f_1 ≫ fk mY = fk mX),
    ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
⊢ ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik

Tactic:
classical
  cases nonempty_fintype I
  obtain ⟨k, fk, hk⟩ := sup_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨i, j x, 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
α : Type u
inst_1 : SemilatticeInf α
X Y : α
f g : X ⟶ Y
h : ULift.down.{u, 0} (𝟙 X ≫ f) = ULift.down.{u, 0} (𝟙 X ≫ g)
⊢ 𝟙 X ≫ f = 𝟙 X ≫ g

Tactic:
apply ULift.ext

Premises used: ULift.ext
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : SemilatticeInf α
X Y : α
f g : X ⟶ Y
⊢ ULift.down.{u, 0} (𝟙 X ≫ f) = ULift.down.{u, 0} (𝟙 X ≫ g)

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
X Y : α
f g : X ⟶ Y
h : ULift.down.{u, 0} (𝟙 X ≫ f) = ULift.down.{u, 0} (𝟙 X ≫ g)
⊢ 𝟙 X ≫ f = 𝟙 X ≫ g

Tactic:
apply ULift.ext

Premises used: ULift.ext
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
X Y : α
f g : X ⟶ Y
⊢ ULift.down.{u, 0} (𝟙 X ≫ f) = ULift.down.{u, 0} (𝟙 X ≫ g)

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : SemilatticeInf α
inst_2 : OrderBot α
⊢ IsCofiltered α

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : SemilatticeInf α
inst_2 : OrderTop α
⊢ IsCofiltered α

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x Y : Discrete PUnit.{u_1 + 1}
⊢ { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = x.as

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x Y : Discrete PUnit.{u_1 + 1}
⊢ { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = Y.as

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
h :
  Eq (α := PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = Y.as))
    (ULift.down.{u_1, 0}
      ({ down := { down := ⋯ : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
          ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
        f))
    (ULift.down.{u_1, 0}
      ({ down := { down := ⋯ : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
          ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
        g))
⊢ Eq (α := { as := PUnit.unit : Discrete PUnit.{u_1 + 1} } ⟶ Y)
    ({ down := { down := ⋯ : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
        ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
      f)
    ({ down := { down := ⋯ : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
        ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
      g)

Tactic:
apply ULift.ext

Premises used: ULift.ext
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ Eq (α := PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = Y.as))
    (ULift.down.{u_1, 0}
      ({ down := { down := ⋯ : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
          ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
        f))
    (ULift.down.{u_1, 0}
      ({ down := { down := ⋯ : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
          ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
        g))

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
j j' : C
f f' : j ⟶ j'
⊢ Eq (α := eq f f' ⟶ j') (eqHom f f' ≫ f) (eqHom f f' ≫ f')

Tactic:
(IsCofilteredOrEmpty.cone_maps f f').choose_spec.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.IsCofilteredOrEmpty.cone_maps, CategoryTheory.IsCofiltered.eqHom, CategoryTheory.IsCofiltered.eq
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
i j j' : C
f : j ⟶ i
f' : j' ⟶ i
K : C
G : K ⟶ j
G' : K ⟶ j'
h : True
k : C
e : k ⟶ K
he : e ≫ G ≫ f = e ≫ G' ≫ f'
⊢ (e ≫ G) ≫ f = (e ≫ G') ≫ f'

Tactic:
simpa only [Category.assoc] using he

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
j : C
x x_1 : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ ∃ (z : (i : C) ×' (i ⟶ j)),
    (fun (x1 x2 : Set ((fun (X : Type u_1) ↦ X) (F.obj j))) ↦ x1 ⊇ x2)
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) i ij))
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          z) ∧
      (fun (x1 x2 : Set ((fun (X : Type u_1) ↦ X) (F.obj j))) ↦ x1 ⊇ x2)
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) k kj))
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          z)

Tactic:
⟨⟨l, lk ≫ kj⟩, e ▸ ?_, ?_⟩

Premises used: Eq.rec, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, PSigma.mk