awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Over.{v₁, u₁} c
s s' : obj (forget c) x ⟶ x_1
h : Eq (α := IsCofiltered.eq s s' ⟶ x_1) (IsCofiltered.eqHom s s' ≫ s) (IsCofiltered.eqHom s s' ≫ s')
⊢ Eq (α := obj (forget c) (mk (Y := IsCofiltered.eq s s') (IsCofiltered.eqHom s s' ≫ x.hom)) ⟶ x_1)
    (Functor.map (forget c) (homMk (IsCofiltered.eqHom s s') ⋯) ≫ s)
    (Functor.map (forget c) (homMk (IsCofiltered.eqHom s s') ⋯) ≫ s')

Tactic:
simp only [forget_obj, mk_left, forget_map, homMk_left]

Premises used: CategoryTheory.Over.mk_left, CategoryTheory.Over.homMk_left, CategoryTheory.Over.forget_obj, CategoryTheory.Over.forget_map
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Over.{v₁, u₁} c
s s' : obj (forget c) x ⟶ x_1
h h₁ : Eq (α := IsCofiltered.eq s s' ⟶ x_1) (IsCofiltered.eqHom s s' ≫ s') (IsCofiltered.eqHom s s' ≫ s')
⊢ Eq (α := IsCofiltered.eq s s' ⟶ x_1) (IsCofiltered.eqHom s s' ≫ s) (IsCofiltered.eqHom s s' ≫ s')

Tactic:
rw [IsCofiltered.eq_condition]

Premises used: CategoryTheory.IsCofiltered.eq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
a :
  Eq (α := PUnit.{v₁ + 1})
    (((colimitCompCoyonedaIso F d).toEquiv : (a : colimit (F ⋙ coyoneda.obj (op d))) → PUnit.{v₁ + 1})
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
              (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
                (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
            s :
          (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))) :
      PUnit.{v₁ + 1})
    (((colimitCompCoyonedaIso F d).toEquiv : (a : colimit (F ⋙ coyoneda.obj (op d))) → PUnit.{v₁ + 1})
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
              (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
                (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
            s' :
          (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))) :
      PUnit.{v₁ + 1})
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))

Tactic:
apply (Final.colimitCompCoyonedaIso F d).toEquiv.injective

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Functor.Final.colimitCompCoyonedaIso, Equiv.injective
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ Eq (α := PUnit.{v₁ + 1})
    (((colimitCompCoyonedaIso F d).toEquiv : (a : colimit (F ⋙ coyoneda.obj (op d))) → PUnit.{v₁ + 1})
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
              (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
                (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
            s :
          (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))) :
      PUnit.{v₁ + 1})
    (((colimitCompCoyonedaIso F d).toEquiv : (a : colimit (F ⋙ coyoneda.obj (op d))) → PUnit.{v₁ + 1})
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
              (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
                (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
            s' :
          (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))) :
      PUnit.{v₁ + 1})

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))

Tactic:
have : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s' := by
    apply (Final.colimitCompCoyonedaIso F d).toEquiv.injective
    subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
obtain :
  ∀ (c' : C) (t₁ t₂ : c ⟶ c')
    (h :
      Eq (α := (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₁) :
              (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
                (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
            s :
          (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₂) :
              (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
                (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
            s' :
          (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))),
    ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
obtain ⟨c', t₁, t₂, h⟩ := (Types.FilteredColimit.colimit_eq_iff.{v₁, v₁, v₁} _).mp this
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
c' : C
t₁ t₂ : c ⟶ c'
h :
  Eq (α := (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₁) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₂) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s' :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
⟨IsFiltered.coeq t₁ t₂, t₁ ≫ IsFiltered.coeqHom t₁ t₂, ?_⟩

Premises used: CategoryTheory.IsFiltered.coeqHom, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsFiltered.coeq
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
c' : C
t₁ t₂ : c ⟶ c'
h :
  Eq (α := (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₁) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₂) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s' :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
refine :
  Eq (α := d ⟶ F.obj (IsFiltered.coeq t₁ t₂)) (s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
    (s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
refine ⟨IsFiltered.coeq t₁ t₂, t₁ ≫ IsFiltered.coeqHom t₁ t₂, ?_⟩
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
c' : C
t₁ t₂ : c ⟶ c'
h :
  Eq (α := (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₁) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₂) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s' :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
rw : s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂)
| s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂)

Tactic:
rw [IsFiltered.coeq_condition t₁ t₂]

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
c' : C
t₁ t₂ : c ⟶ c'
h :
  Eq (α := (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₁) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₂) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s' :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
conv_rhs :
  Eq (α := d ⟶ F.obj (IsFiltered.coeq t₁ t₂)) (s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
    (s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂))
⊢ Eq (α := d ⟶ F.obj (IsFiltered.coeq t₁ t₂)) (s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
    (s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))

Tactic:
conv_rhs => rw [IsFiltered.coeq_condition t₁ t₂]

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
c' : C
t₁ t₂ : c ⟶ c'
h : s ≫ F.map t₁ = s' ≫ F.map t₂
⊢ Eq (α := d ⟶ F.obj (IsFiltered.coeq t₁ t₂)) (s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
    (s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂))

Tactic:
simp [reassoc_of% h]
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
⊢ F.Final ↔
    (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
⟨fun hF => ⟨?_, ?_⟩, fun h => final_of_exists_of_isFiltered F h.1 h.2⟩

Premises used: CategoryTheory.Functor.final_of_exists_of_isFiltered, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
refine_1 : ∀ (hF : F.Final) (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
refine_2 : ∀ (hF : F.Final) {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
⊢ F.Final ↔
    (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
refine ⟨fun hF => ⟨?_, ?_⟩, fun h => final_of_exists_of_isFiltered F h.1 h.2⟩
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
hF : F.Final
d : D
⊢ Nonempty (StructuredArrow d F)

Tactic:
IsConnected.is_nonempty

Premises used: CategoryTheory.IsConnected.is_nonempty
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
hF : F.Final
d : D
refine_1 : ∀ (f : StructuredArrow d F), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
⊢ ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)

Tactic:
obtain ⟨f⟩ : Nonempty (StructuredArrow d F) := IsConnected.is_nonempty

Premises used: CategoryTheory.IsConnected.is_nonempty, Nonempty, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
hF : F.Final
d : D
f : StructuredArrow d F
⊢ ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)

Tactic:
⟨_, ⟨f.hom⟩⟩

Premises used: CategoryTheory.StructuredArrow.hom, Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
hF : F.Final
d : D
f : StructuredArrow d F
⊢ ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)

Tactic:
exact ⟨_, ⟨f.hom⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
⊢ IsFilteredOrEmpty (AsSmall C)

Tactic:
have : IsFilteredOrEmpty (AsSmall.{max u₁ v₁ u₂ v₂} C) := .of_equivalence s₁
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
this : IsFilteredOrEmpty (AsSmall C)
d : D
c : C
s s' : d ⟶ F.obj c
refine_2 :
  ∀ (c' : AsSmall C) (t : { down := c : ULift.{max (max u₁ v₁ u₂ v₂) v₁, u₁} C } ⟶ c')
    (ht :
      Eq (α := obj AsSmall.up d ⟶ (s₁.inverse ⋙ F ⋙ s₂.functor).obj c')
        (map AsSmall.up s ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t)
        (map AsSmall.up s' ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t)),
    ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
obtain ⟨c', t, ht⟩ := Functor.Final.exists_coeq_of_locally_small (s₁.inverse ⋙ F ⋙ s₂.functor)
      (AsSmall.up.map s) (AsSmall.up.map s')

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map, CategoryTheory.AsSmall.up, CategoryTheory.Functor.Final.exists_coeq_of_locally_small, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
this : IsFilteredOrEmpty (AsSmall C)
d : D
c : C
s s' : d ⟶ F.obj c
c' : AsSmall C
t : { down := c : ULift.{max (max u₁ v₁ u₂ v₂) v₁, u₁} C } ⟶ c'
ht :
  Eq (α := obj AsSmall.up d ⟶ (s₁.inverse ⋙ F ⋙ s₂.functor).obj c')
    (map AsSmall.up s ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t) (map AsSmall.up s' ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t)
⊢ Eq (α := s₂.functor.obj d ⟶ s₂.functor.obj (F.obj (obj AsSmall.down c')))
    (s₂.functor.map (s ≫ F.map (map AsSmall.down t))) (s₂.functor.map (s' ≫ F.map (map AsSmall.down t)))

Tactic:
simp_all [s₁, s₂]
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
this : IsFilteredOrEmpty (AsSmall C)
d : D
c : C
s s' : d ⟶ F.obj c
c' : AsSmall C
t : { down := c : ULift.{max (max u₁ v₁ u₂ v₂) v₁, u₁} C } ⟶ c'
ht :
  Eq (α := obj AsSmall.up d ⟶ (s₁.inverse ⋙ F ⋙ s₂.functor).obj c')
    (map AsSmall.up s ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t) (map AsSmall.up s' ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t)
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
exact ⟨AsSmall.down.obj c', AsSmall.down.map t, s₂.functor.map_injective (by simp_all [s₁, s₂])⟩
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
⊢ F.Initial ↔
    (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'

Tactic:
⟨fun hF => ?_, fun h => initial_of_exists_of_isCofiltered F h.1 h.2⟩

Premises used: CategoryTheory.Functor.initial_of_exists_of_isCofiltered, And.right, And.left, Iff.intro
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
refine :
  ∀ (hF : F.Initial),
    (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
⊢ F.Initial ↔
    (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'

Tactic:
refine ⟨fun hF => ?_, fun h => initial_of_exists_of_isCofiltered F h.1 h.2⟩
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
hF : F.Initial
⊢ ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)

Tactic:
obtain ⟨h₁, h₂⟩ := F.op.final_iff_of_isFiltered.mp inferInstance

Premises used: CategoryTheory.Functor.op, inferInstance, Iff.mp, CategoryTheory.Functor.final_iff_of_isFiltered