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
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
empty :
  ∃ (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
insert :
  ∀ (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),
    ∃ (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
⊢ ∃ (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

Tactic:
induction H using Finset.induction with
  | empty =>
    obtain ⟨S, f⟩ := inf_objs_exists O
    exact ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩
  | insert h' H' nmf h'' =>
    obtain ⟨X, Y, mX, mY, f⟩ := h'
    obtain ⟨S', T', w'⟩ := h''
    refine ⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, ?_⟩
    intro X' Y' mX' mY' f' mf'
    rw [Category.assoc]
    by_cases h : X = X' ∧ Y = Y'
    · rcases h with ⟨rfl, rfl⟩
      grind [eq_condition]
    · rw [@w' _ _ mX' mY' f' _]
      apply Finset.mem_of_mem_insert_of_ne mf'
      contrapose h
      obtain ⟨rfl, h⟩ := h
      trivial

Premises used: CategoryTheory.Category.assoc, Insert.insert, CategoryTheory.IsCofiltered.inf_objs_exists, CategoryTheory.IsCofiltered.eq_condition, 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) (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
insert :
  ∀ (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),
    ∃ (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
⊢ ∃ (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

Tactic:
classical
  induction H using Finset.induction with
  | empty =>
    obtain ⟨S, f⟩ := inf_objs_exists O
    exact ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩
  | insert h' H' nmf h'' =>
    obtain ⟨X, Y, mX, mY, f⟩ := h'
    obtain ⟨S', T', w'⟩ := h''
    refine ⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, ?_⟩
    intro X' Y' mX' mY' f' mf'
    rw [Category.assoc]
    by_cases h : X = X' ∧ Y = Y'
    · rcases h with ⟨rfl, rfl⟩
      grind [eq_condition]
    · rw [@w' _ _ mX' mY' f' _]
      apply Finset.mem_of_mem_insert_of_ne mf'
      contrapose h
      obtain ⟨rfl, h⟩ := h
      trivial

Premises used: CategoryTheory.Category.assoc, Insert.insert, CategoryTheory.IsCofiltered.inf_objs_exists, CategoryTheory.IsCofiltered.eq_condition, 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))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
mf :
  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 (α := inf O H ⟶ Y) (infTo O H mX ≫ f) (infTo O H mY)

Tactic:
(inf_exists O H).choose_spec.choose_spec mX mY mf

Premises used: CategoryTheory.IsCofiltered.inf, Exists.choose_spec, CategoryTheory.IsCofiltered.infTo, CategoryTheory.IsCofiltered.inf_exists
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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
X Y : J
f : X ⟶ Y
⊢ F.obj X ∈ O

Tactic:
simp [O]
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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
X Y : J
f : X ⟶ Y
⊢ F.obj Y ∈ O

Tactic:
simp [O]
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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
obtain :
  ∀ (Z : C) (f : {X : C} → X ∈ O → (Z ⟶ X))
    (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 mX ≫ f_1 = f mY),
    Nonempty (Cone F)
⊢ Nonempty (Cone F)

Tactic:
obtain ⟨Z, f, w⟩ := inf_exists O H

Premises used: CategoryTheory.IsCofiltered.inf_exists
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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 → (Z ⟶ X)
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 mX ≫ f_1 = f mY
X : J
⊢ F.obj X ∈ O

Tactic:
simp [O]
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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 → (Z ⟶ X)
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 mX ≫ f_1 = f mY
refine :
  ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y),
    Eq (α := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) Z) X ⟶ F.obj Y)
      (Functor.map (Functor.obj (Functor.const J) Z) f_1 ≫ (fun (X : J) ↦ (f ⋯ : Z ⟶ F.obj X)) Y)
      ((fun (X : J) ↦ (f ⋯ : Z ⟶ F.obj X)) X ≫ F.map f_1)
⊢ Nonempty (Cone F)

Tactic:
refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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 → (Z ⟶ X)
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 mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
dsimp : 𝟙 Z ≫ f ⋯ = f ⋯ ≫ F.map g
⊢ Eq (α := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) Z) j ⟶ F.obj j')
    (Functor.map (Functor.obj (Functor.const J) Z) g ≫ (fun (X : J) ↦ (f ⋯ : Z ⟶ F.obj X)) j')
    ((fun (X : J) ↦ (f ⋯ : Z ⟶ F.obj X)) j ≫ F.map g)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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 → (Z ⟶ X)
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 mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
simp : f ⋯ = f ⋯ ≫ F.map g
⊢ 𝟙 Z ≫ f ⋯ = f ⋯ ≫ F.map g

Tactic:
simp only [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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 → (Z ⟶ X)
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 mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
symm : f ⋯ ≫ F.map g = f ⋯
⊢ f ⋯ = f ⋯ ≫ F.map g

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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 → (Z ⟶ X)
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 mX ≫ f_1 = f mY
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 ⋯ ≫ F.map g = f ⋯

Tactic:
apply w
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{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 → (Z ⟶ X)
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 mX ≫ f_1 = f mY
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 : IsCofiltered.{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 → (Z ⟶ X)
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 mX ≫ f_1 = f mY
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 : IsCofiltered.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v, v₁, u, u₁} C D
R : Functor.{v₁, v, u₁, u} D C
h : L ⊣ R
⊢ IsCofiltered.{v₁, u₁} D

Tactic:
{ IsCofilteredOrEmpty.of_left_adjoint h with
    nonempty := IsCofiltered.nonempty.map L.obj }

Premises used: CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint, CategoryTheory.IsCofiltered.mk