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₀)
x y : (j : J) × F.obj j
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
f' : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  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 x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
rw rw₁ :
  Eq.{w₀ + 1} (α :=
    F.obj
      (Sigma.fst (β := fun (j : J) ↦ F.obj j)
        (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (x.snd (β := fun (j : J) ↦ F.obj j))))))
    (Sigma.snd (β := fun (j : J) ↦ F.obj j)
      (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x.snd (β := fun (j : J) ↦ F.obj j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) →
          (fun (X : Type w₀) ↦ X)
            (F.obj
              ⟨k,
                  (ConcreteCategory.hom (F.map f) :
                      (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                    x.snd⟩.fst))
      (x.snd (β := fun (j : J) ↦ F.obj j)))
⊢ Eq.{w₀ + 1} (α :=
    F.obj
      (Sigma.fst (β := fun (j : J) ↦ F.obj j)
        (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
              (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (y.snd (β := fun (j : J) ↦ F.obj j))))))
    (Sigma.snd (β := fun (j : J) ↦ F.obj j)
      (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y.snd (β := fun (j : J) ↦ F.obj j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) →
          (fun (X : Type w₀) ↦ X)
            (F.obj
              ⟨k,
                  (ConcreteCategory.hom (F.map f') :
                      (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                    y.snd⟩.fst))
      (x.snd (β := fun (j : J) ↦ F.obj j)))

Tactic:
rw [← h]
-- 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₀)
x y : (j : J) × F.obj j
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
f' : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  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 x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ Relation.EqvGen F.ColimitTypeRel x
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j))))

Tactic:
exact .rel _ _ ⟨f, by rw [← h]⟩
-- 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₀)
x y : (j : J) × F.obj j
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
f' : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  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 x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ Relation.EqvGen F.ColimitTypeRel
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j))))
    y

Tactic:
.symm _ _ (.rel _ _ ⟨f', rfl⟩)

Premises used: Exists.intro, Relation.EqvGen.rel, Relation.EqvGen.symm, 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₀)
x y : (j : J) × F.obj j
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
f' : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  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 x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ Relation.EqvGen F.ColimitTypeRel
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j))))
    y

Tactic:
exact .symm _ _ (.rel _ _ ⟨f', 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₀)
j j' : J
x : F.obj j
y : F.obj j'
rw :
  Relation.EqvGen F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)
      (Sigma.mk (β := fun (j : J) ↦ F.obj j) j' y) ↔
    ∃ (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))
            y :
          (fun (X : Type w₀) ↦ X) (F.obj k))
rw₁ rw₂ :
  (∃ (k : J) (f : (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x).fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g :
      (Sigma.mk (β := fun (j : J) ↦ F.obj j) j' y).fst (β := fun (j : J) ↦ F.obj 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, x⟩.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            ((Sigma.mk (β := fun (j : J) ↦ F.obj j) j x).snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj ⟨j', y⟩.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            ((Sigma.mk (β := fun (j : J) ↦ F.obj j) j' y).snd (β := fun (j : J) ↦ F.obj j)) :
          (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))
            y :
          (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ F.ιColimitType j x = F.ιColimitType j' y ↔
    ∃ (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))
            y :
          (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
rw [ιColimitType_eq_iff, eqvGen_colimitTypeRel_iff_of_isFiltered]

Premises used: CategoryTheory.Functor.eqvGen_colimitTypeRel_iff_of_isFiltered, CategoryTheory.Functor.ιColimitType_eq_iff
-- 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₀)
j : J
x y : F.obj j
rw :
  (∃ (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))
            y :
          (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))
            y :
          (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ F.ιColimitType j x = F.ιColimitType j y ↔
    ∃ (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))
            y :
          (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
rw [ιColimitType_eq_iff_of_isFiltered]

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₀)
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h :
  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))
        y :
      (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))
          y :
        (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₀)
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h :
  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))
        y :
      (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')))
        y :
      (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))
          y :
        (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₀)
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h :
  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))
        y :
      (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')))
        y :
      (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')))
        y :
      (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))

Tactic:
nth_rw 2 [coeq_condition]

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- 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₀)
j : J
x y : F.obj j
k : J
f f' : j ⟶ k
h :
  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))
        y :
      (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ 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')))
        y :
      (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))

Tactic:
simp [h]
-- 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₀)
j : J
x y : F.obj j
k : J
f : j ⟶ k
h :
  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))
        y :
      (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))
          y :
        (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
⟨k, f, f, h⟩

Premises used: Exists.intro
-- 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₀)
j : J
x y : F.obj j
k : J
f : j ⟶ k
h :
  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))
        y :
      (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))
          y :
        (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
exact ⟨k, f, f, h⟩
-- 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
mp :
  Function.Injective (F.descColimitType c) →
    ∀ (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))
mpr :
  (∀ (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))) →
    Function.Injective (F.descColimitType c)
⊢ Function.Injective (F.descColimitType c) ↔
    ∀ (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))

Tactic:
constructor
-- 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'
⊢ F.ιColimitType j x = F.ιColimitType j' x'

Tactic:
have : F.ιColimitType j x = F.ιColimitType j' x' := h eq