awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h : Function.Injective (F.descColimitType c)
j j' : J
x : F.obj j
x' : F.obj j'
eq : c.ι j x = c.ι j' x'
this : F.ιColimitType j x = F.ιColimitType j' x'
mp mp₁ mp₂ mp₃ :
  ∀
    (this :
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))),
    ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
              (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x' :
          (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          x :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
            (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
          x' :
        (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
rwa [ιColimitType_eq_iff_of_isFiltered] at this

Premises used: CategoryTheory.Functor.ιColimitType_eq_iff_of_isFiltered
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
x x' : F.ColimitType
eq : F.descColimitType c x = F.descColimitType c x'
mpr :
  ∀ (i : J) (x : F.obj i) (eq : F.descColimitType c (F.ιColimitType i x) = F.descColimitType c x'),
    F.ιColimitType i x = x'
⊢ x = x'

Tactic:
obtain ⟨i, x, rfl⟩ := F.ιColimitType_jointly_surjective x

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
x' : F.ColimitType
i : J
x : F.obj i
eq : F.descColimitType c (F.ιColimitType i x) = F.descColimitType c x'
mpr :
  ∀ (i' : J) (x' : F.obj i')
    (eq : F.descColimitType c (F.ιColimitType i x) = F.descColimitType c (F.ιColimitType i' x')),
    F.ιColimitType i x = F.ιColimitType i' x'
⊢ F.ιColimitType i x = x'

Tactic:
obtain ⟨i', x', rfl⟩ := F.ιColimitType_jointly_surjective x'

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
i : J
x : F.obj i
i' : J
x' : F.obj i'
eq : c.ι i x = c.ι i' x'
mpr :
  ∀ (k : J) (f : i ⟶ k) (f' : i' ⟶ k)
    (eq :
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj i)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
              (a : (fun (X : Type w₀) ↦ X) (F.obj i')) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x' :
          (fun (X : Type w₀) ↦ X) (F.obj k))),
    F.ιColimitType i x = F.ιColimitType i' x'
⊢ F.ιColimitType i x = F.ιColimitType i' x'

Tactic:
obtain ⟨k, f, f', eq⟩ := h _ _ _ _ eq
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
i : J
x : F.obj i
i' : J
x' : F.obj i'
eq_1 : c.ι i x = c.ι i' x'
k : J
f : i ⟶ k
f' : i' ⟶ k
eq :
  Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj i)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj i')) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x' :
      (fun (X : Type w₀) ↦ X) (F.obj k))
mpr :
  F.ιColimitType k
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj i)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x) =
    F.ιColimitType i' x'
mpr₁ :
  F.ιColimitType k
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj i')) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x') =
    F.ιColimitType i' x'
mpr₂ mpr₃ : F.ιColimitType i' x' = F.ιColimitType i' x'
⊢ F.ιColimitType i x = F.ιColimitType i' x'

Tactic:
rw [← F.ιColimitType_map f x, eq, F.ιColimitType_map]

Premises used: CategoryTheory.Functor.ιColimitType_map
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
rw :
  (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' →
        ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
          Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x :
              (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x' :
              (fun (X : Type w₀) ↦ X) (F.obj k))) ↔
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' →
        ∃ (k : J) (f : j ⟶ k),
          Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x :
              (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x' :
              (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ Function.Injective (F.descColimitType c) ↔
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' →
        ∃ (k : J) (f : j ⟶ k),
          Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x :
              (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x' :
              (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
rw [descColimitType_injective_iff_of_isFiltered]

Premises used: CategoryTheory.Functor.CoconeTypes.descColimitType_injective_iff_of_isFiltered
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
j : J
x x' : F.obj j
eq : c.ι j x = c.ι j x'
mp :
  ∀ (k : J) (f f' : j ⟶ k)
    (eq :
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
              (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x' :
          (fun (X : Type w₀) ↦ X) (F.obj k))),
    ∃ (k : J) (f : j ⟶ k),
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x' :
          (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ ∃ (k : J) (f : j ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          x :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          x' :
        (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
obtain ⟨k, f, f', eq⟩ := h _ _ _ _ eq
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
j : J
x x' : F.obj j
eq_1 : c.ι j x = c.ι j x'
k : J
f f' : j ⟶ k
eq :
  Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x' :
      (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ ∃ (k : J) (f : j ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          x :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          x' :
        (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
⟨coeq f f', f ≫ coeqHom f f', ?_⟩

Premises used: CategoryTheory.IsFiltered.coeqHom, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsFiltered.coeq
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
j : J
x x' : F.obj j
eq_1 : c.ι j x = c.ι j x'
k : J
f f' : j ⟶ k
eq :
  Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x' :
      (fun (X : Type w₀) ↦ X) (F.obj k))
mp :
  Eq (α := (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ≫ coeqHom f f')) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
        x :
      (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ≫ coeqHom f f')) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
        x' :
      (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
⊢ ∃ (k : J) (f : j ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          x :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          x' :
        (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
j : J
x x' : F.obj j
eq_1 : c.ι j x = c.ι j x'
k : J
f f' : j ⟶ k
eq :
  Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x' :
      (fun (X : Type w₀) ↦ X) (F.obj k))
mp :
  Eq (α := (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (coeqHom f f')) : (a : F.obj k) → F.obj (coeq f f'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
              (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x' :
          (fun (X : Type w₀) ↦ X) (F.obj k)) :
      F.obj (coeq f f'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f ≫ F.map (coeqHom f f')) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
        x' :
      (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
⊢ Eq (α := (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ≫ coeqHom f f')) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
        x :
      (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ≫ coeqHom f f')) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
        x' :
      (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))

Tactic:
rw [map_comp, comp_apply, eq]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h :
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
j : J
x x' : F.obj j
eq_1 : c.ι j x = c.ι j x'
k : J
f f' : j ⟶ k
eq :
  Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        x' :
      (fun (X : Type w₀) ↦ X) (F.obj k))
mp :
  Eq (α := F.obj (coeq f f'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f' ≫ coeqHom f f')) : (a : F.obj j) → F.obj (coeq f f')) x' :
      F.obj (coeq f f'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ≫ coeqHom f f')) : (a : F.obj j) → F.obj (coeq f f')) x' :
      F.obj (coeq f f'))
⊢ Eq (α := (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (coeqHom f f')) : (a : F.obj k) → F.obj (coeq f f'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
              (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            x' :
          (fun (X : Type w₀) ↦ X) (F.obj k)) :
      F.obj (coeq f f'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f ≫ F.map (coeqHom f f')) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
        x' :
      (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))

Tactic:
simp only [← comp_apply, ← map_comp]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp