awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ Eq (α := (colimitCocone F).pt)
      ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
          ((hom (FC := TypeCat.Fun) (t.ι.app i) :
                (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
              xi :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) :
        (colimitCocone F).pt)
      ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
          ((hom (FC := TypeCat.Fun) (t.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
              xj :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) :
        (colimitCocone F).pt) ↔
    Eq (α := (colimitCocone F).pt)
      ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
          ((hom (FC := TypeCat.Fun) (t.ι.app i) :
                (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
              xi :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) :
        (colimitCocone F).pt)
      ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
          ((hom (FC := TypeCat.Fun) (t.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
              xj :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) :
        (colimitCocone F).pt)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1 :
  (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i) =
    (colimitCocone F).pt
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app i) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i))
        xi :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
        ((hom (FC := TypeCat.Fun) (t.ι.app i) :
              (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
            xi :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) :
      (colimitCocone F).pt)

Tactic:
(congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xi).symm

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.Types.colimitCoconeIsColimit, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1 :
  (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i) =
    (colimitCocone F).pt
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app i) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i))
        xi :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
        ((hom (FC := TypeCat.Fun) (t.ι.app i) :
              (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
            xi :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) :
      (colimitCocone F).pt)

Tactic:
exact (congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xi).symm

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.Types.colimitCoconeIsColimit, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1 :
  (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i) =
    (colimitCocone F).pt
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj j))
        xj :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) j))
    ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
        ((hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            xj :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) :
      (colimitCocone F).pt)

Tactic:
(congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xj).symm

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.Types.colimitCoconeIsColimit, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1 :
  (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i) =
    (colimitCocone F).pt
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj j))
        xj :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) j))
    ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
        ((hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            xj :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) :
      (colimitCocone F).pt)

Tactic:
exact (congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xj).symm

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.Types.colimitCoconeIsColimit, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
rw :
  (∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            x :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            y :
          (fun (X : Type u) ↦ X) (F.obj k))) ↔
    ∃ (j : J) (f : i ⟶ j),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            y :
          (fun (X : Type u) ↦ X) (F.obj j))
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
          x :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
          y :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) ↔
    ∃ (j : J) (f : i ⟶ j),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            y :
          (fun (X : Type u) ↦ X) (F.obj j))

Tactic:
rw [isColimit_eq_iff _ ht]

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
mp :
  (∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            x :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            y :
          (fun (X : Type u) ↦ X) (F.obj k))) →
    ∃ (j : J) (f : i ⟶ j),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            y :
          (fun (X : Type u) ↦ X) (F.obj j))
mpr :
  (∃ (j : J) (f : i ⟶ j),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            y :
          (fun (X : Type u) ↦ X) (F.obj j))) →
    ∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            x :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            y :
          (fun (X : Type u) ↦ X) (F.obj k))
⊢ (∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            x :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            y :
          (fun (X : Type u) ↦ X) (F.obj k))) ↔
    ∃ (j : J) (f : i ⟶ j),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            y :
          (fun (X : Type u) ↦ X) (F.obj j))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) x :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) y :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ ∃ (j : J) (f : i ⟶ j),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))

Tactic:
⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩

Premises used: CategoryTheory.IsFiltered.coeqHom, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsFiltered.coeq
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) x :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) y :
      (fun (X : Type u) ↦ X) (F.obj k))
mp :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        x :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        y :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
⊢ ∃ (j : J) (f : i ⟶ j),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))

Tactic:
refine ⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) x :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) y :
      (fun (X : Type u) ↦ X) (F.obj k))
rw :
  ((hom (FC := TypeCat.Fun) (F.map (g ≫ IsFiltered.coeqHom f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
      y :
    (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
| ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
      y :
    (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))

Tactic:
rw [IsFiltered.coeq_condition]

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) x :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) y :
      (fun (X : Type u) ↦ X) (F.obj k))
mp :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        x :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (g ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        y :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        x :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        y :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))

Tactic:
conv_rhs => rw [IsFiltered.coeq_condition]

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) x :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) y :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        x :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (g ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        y :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
j : J
f : i ⟶ j
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j)) x :
      (fun (X : Type u) ↦ X) (F.obj j))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j)) y :
      (fun (X : Type u) ↦ X) (F.obj j))
⊢ ∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          x :
        (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          y :
        (fun (X : Type u) ↦ X) (F.obj k))

Tactic:
⟨j, f, f, h⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
j : J
f : i ⟶ j
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j)) x :
      (fun (X : Type u) ↦ X) (F.obj j))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j)) y :
      (fun (X : Type u) ↦ X) (F.obj j))
⊢ ∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          x :
        (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          y :
        (fun (X : Type u) ↦ X) (F.obj k))

Tactic:
exact ⟨j, f, f, h⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
inst_2 : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
      ((hom (FC := TypeCat.Fun) (colimit.ι F i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (colimit F))
          xi :
        (fun (X : Type u) ↦ X) (colimit F))
      ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
          xj :
        (fun (X : Type u) ↦ X) (colimit F)) ↔
    ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            xi :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj k))
            xj :
          (fun (X : Type u) ↦ X) (F.obj k))

Tactic:
isColimit_eq_iff _ (colimit.isColimit F)

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit