awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_1 :
  Superset (α := Set (F.obj j))
    (Set.range (ι := F.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ij)) : (a : F.obj i) → F.obj j))
    (Set.range (ι := F.obj l)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map li ≫ F.map ij)) : (a : F.obj l) → F.obj j))
⊢ Superset.{u_1} (α := Set ((fun (X : Type u_1) ↦ X) (F.obj j)))
    ((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))))
      (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) l (li ≫ ij)))

Tactic:
simp_rw [F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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
refine_2 :
  Superset (α := Set (F.obj j))
    (Set.range (ι := F.obj k) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map kj)) : (a : F.obj k) → F.obj j))
    (Set.range (ι := F.obj l)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map lk ≫ F.map kj)) : (a : F.obj l) → F.obj 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) 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))))
      (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) l (lk ≫ kj)))

Tactic:
simp_rw [F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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
⊢ Subset (α := Set (F.obj j))
    (Set.range
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ij)) : (a : F.obj i) → F.obj j) ∘ (F.map li).hom'.toFun))
    (Set.range (ι := F.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ij)) : (a : F.obj i) → F.obj j))

Tactic:
Set.range_comp_subset_range _ _

Premises used: Set.range_comp_subset_range
-- 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
⊢ Superset (α := Set (F.obj j))
    (Set.range (ι := F.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ij)) : (a : F.obj i) → F.obj j))
    (Set.range (ι := F.obj l)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map li ≫ F.map ij)) : (a : F.obj l) → F.obj j))

Tactic:
convert! Set.range_comp_subset_range _ _

Premises used: Set.range_comp_subset_range
-- 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
⊢ Subset (α := Set (F.obj j))
    (Set.range
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map kj)) : (a : F.obj k) → F.obj j) ∘ (F.map lk).hom'.toFun))
    (Set.range (ι := F.obj k) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map kj)) : (a : F.obj k) → F.obj j))

Tactic:
Set.range_comp_subset_range _ _

Premises used: Set.range_comp_subset_range
-- 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
⊢ Superset (α := Set (F.obj j))
    (Set.range (ι := F.obj k) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map kj)) : (a : F.obj k) → F.obj j))
    (Set.range (ι := F.obj l)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map lk ≫ F.map kj)) : (a : F.obj l) → F.obj j))

Tactic:
convert! Set.range_comp_subset_range _ _

Premises used: Set.range_comp_subset_range
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
obtain :
  ∀ (t : C) (k₁t : t ⟶ k₁) (k₂t : t ⟶ k₂) (ht : k₁t ≫ f₁ = k₂t ≫ g₁),
    ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂
⊢ ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂

Tactic:
obtain ⟨t, k₁t, k₂t, ht⟩ := cospan f₁ g₁

Premises used: CategoryTheory.IsCofiltered.cospan
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
obtain :
  ∀ (s : C) (ts : s ⟶ t) (hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂),
    ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂
⊢ ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂

Tactic:
obtain ⟨s, ts, hs⟩ := IsCofilteredOrEmpty.cone_maps (k₁t ≫ f₂) (k₂t ≫ g₂)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.IsCofilteredOrEmpty.cone_maps
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
s : C
ts : s ⟶ t
hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂
⊢ (ts ≫ k₁t) ≫ f₁ = (ts ≫ k₂t) ≫ g₁

Tactic:
simp only [Category.assoc, ht]

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
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
s : C
ts : s ⟶ t
hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂
⊢ (ts ≫ k₁t) ≫ f₂ = (ts ≫ k₂t) ≫ g₂

Tactic:
simp only [Category.assoc, hs]

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
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
s : C
ts : s ⟶ t
hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂
⊢ ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂

Tactic:
exact ⟨s, ts ≫ k₁t, ts ≫ k₂t, by simp only [Category.assoc, ht],
    by simp only [Category.assoc, hs]⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v, v₁, u, u₁} C D
inst_3 : L.IsLeftAdjoint
⊢ IsCofilteredOrEmpty.{v₁, u₁} D

Tactic:
of_left_adjoint (Adjunction.ofIsLeftAdjoint L)

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

Tactic:
of_left_adjoint h.toAdjunction

Premises used: CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint, CategoryTheory.Equivalence.toAdjunction
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
⊢ ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (Classical.choice ⋯ ⟶ X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
⊢ ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (S ⟶ X)

Tactic:
exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
h : ∃ (S : C), ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S ⟶ X)
insert :
  ∀ (S' : C) (w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S' ⟶ X)),
    ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ Insert.insert X O' → Nonempty.{v + 1} (S ⟶ X_1)
⊢ ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ Insert.insert X O' → Nonempty.{v + 1} (S ⟶ X_1)

Tactic:
obtain ⟨S', w'⟩ := h
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S' ⟶ X)
h : ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (min.{v, u} X S' ⟶ X_1)
⊢ ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (S ⟶ X_1)

Tactic:
use min X S'

Premises used: CategoryTheory.IsCofiltered.min
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
h : ∀ (nm : Y ∉ O') (mY : Y ∈ insert Y O'), Nonempty.{v + 1} (min.{v, u} Y S' ⟶ Y)
h₁ : ∀ (h : Y ≠ X), Nonempty.{v + 1} (min.{v, u} X S' ⟶ Y)
⊢ Nonempty.{v + 1} (min.{v, u} X S' ⟶ Y)

Tactic:
obtain rfl | h := eq_or_ne Y X

Premises used: eq_or_ne, rfl
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S' ⟶ X)
Y : C
nm : Y ∉ O'
mY : Y ∈ insert Y O'
⊢ Nonempty.{v + 1} (min.{v, u} Y S' ⟶ Y)

Tactic:
⟨minToLeft _ _⟩

Premises used: Nonempty.intro, CategoryTheory.IsCofiltered.minToLeft
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S' ⟶ X)
Y : C
nm : Y ∉ O'
mY : Y ∈ insert Y O'
⊢ Nonempty.{v + 1} (min.{v, u} Y S' ⟶ Y)

Tactic:
exact ⟨minToLeft _ _⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ Nonempty.{v + 1} (min.{v, u} X S' ⟶ Y)

Tactic:
⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩

Premises used: Nonempty.some, Nonempty.intro, CategoryTheory.IsCofiltered.minToRight, CategoryTheory.CategoryStruct.comp, Finset.mem_of_mem_insert_of_ne
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ Nonempty.{v + 1} (min.{v, u} X S' ⟶ Y)

Tactic:
exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (S ⟶ X)
insert :
  ∀ (X : C) (O' : Finset C) (nm : X ∉ O') (h : ∃ (S : C), ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S ⟶ X)),
    ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ Insert.insert X O' → Nonempty.{v + 1} (S ⟶ X_1)
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (S ⟶ X)

Tactic:
induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use min X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨minToLeft _ _⟩
    · exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩

Premises used: Insert.insert, rfl
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (S ⟶ X)
insert :
  ∀ (X : C) (O' : Finset C) (nm : X ∉ O') (h : ∃ (S : C), ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S ⟶ X)),
    ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ Insert.insert X O' → Nonempty.{v + 1} (S ⟶ X_1)
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (S ⟶ X)

Tactic:
classical
  induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use min X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨minToLeft _ _⟩
    · exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩

Premises used: Insert.insert, rfl
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
empty :
  ∀ (S : C) (f : ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (S ⟶ X)),
    ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
      ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
        Membership.mem (γ := Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (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)))) →
          T mX ≫ f = T mY
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      Membership.mem (γ := Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (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)))) →
        T mX ≫ f = T mY

Tactic:
obtain ⟨S, f⟩ := inf_objs_exists O

Premises used: CategoryTheory.IsCofiltered.inf_objs_exists
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (S ⟶ X)
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      Membership.mem (γ := Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (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)))) →
        T mX ≫ f = T mY

Tactic:
exact ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h' : (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)
H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
nmf : h' ∉ H'
h'' :
  ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : 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))) ∈
          H' →
        T mX ≫ f = T mY
insert :
  ∀ (X Y : C) (mX : X ∈ O) (mY : Y ∈ O) (f : X ⟶ Y)
    (nmf :
      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))) ∉
        H'),
    ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
      ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
        PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
              (PSigma.mk (β := fun (Y : C) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y_1
                (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y_1 ∈ O) ×' (X_1 ⟶ Y_1)) mX_1
                  (PSigma.mk (β := fun (x : Y_1 ∈ O) ↦ X_1 ⟶ Y_1) mY_1 f_1))) ∈
            Insert.insert
              (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))))
              H' →
          T mX_1 ≫ f_1 = T mY_1
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : 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))) ∈
          Insert.insert h' H' →
        T mX ≫ f = T mY

Tactic:
obtain ⟨X, Y, mX, mY, f⟩ := h'
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  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))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : 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))) ∈
        H' →
      T' mX ≫ f = T' mY
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y_1
              (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y_1 ∈ O) ×' (X_1 ⟶ Y_1)) mX_1
                (PSigma.mk (β := fun (x : Y_1 ∈ O) ↦ X_1 ⟶ Y_1) mY_1 f_1))) ∈
          insert
            (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))))
            H' →
        T mX_1 ≫ f_1 = T mY_1

Tactic:
⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, ?_⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsCofiltered.eqHom, CategoryTheory.IsCofiltered.eq
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  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))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : 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))) ∈
        H' →
      T' mX ≫ f = T' mY
insert :
  ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y_1
            (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y_1 ∈ O) ×' (X_1 ⟶ Y_1)) mX_1
              (PSigma.mk (β := fun (x : Y_1 ∈ O) ↦ X_1 ⟶ Y_1) mY_1 f_1))) ∈
        Insert.insert
          (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))))
          H' →
      Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y_1)
        ((fun {X_2 : C} (mZ : X_2 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_2)) mX_1 ≫ f_1)
        ((fun {X_2 : C} (mZ : X_2 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_2)) mY_1)
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y_1
              (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y_1 ∈ O) ×' (X_1 ⟶ Y_1)) mX_1
                (PSigma.mk (β := fun (x : Y_1 ∈ O) ↦ X_1 ⟶ Y_1) mY_1 f_1))) ∈
          Insert.insert
            (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))))
            H' →
        T mX_1 ≫ f_1 = T mY_1

Tactic:
refine ⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, ?_⟩