awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
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
⊢ 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))
have 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))
Tactic: rw [descColimitType_injective_iff_of_isFiltered]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
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
⊢ (∀ (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))
have mp : (∀ (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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
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'
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨k, f, f', eq⟩ := h _ _ _ _ eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
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))
have 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')))
Tactic: refine ⟨coeq f f', f ≫ coeqHom f f', ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
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))
⊢ 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')))
have 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')))
Tactic: rw [map_comp, comp_apply, eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
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))
⊢ 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')))
have 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'))
Tactic: simp only [← comp_apply, ← map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
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))
⊢ 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'))
have 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'))
Tactic: rw [coeq_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
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) (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))
j j' : J
x : F.obj j
x' : F.obj j'
eq : 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))
have mpr : ∀ (k : J) (g : IsFiltered.max.{v, u} j j' ⟶ k)
  (eq :
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max j j'))) → (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (leftToMax j j')) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max j j')))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max.{v, u} j 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 (IsFiltered.max j j'))) → (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (rightToMax j j')) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max j j')))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max.{v, u} j 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))
          x' :
        (fun (X : Type w₀) ↦ X) (F.obj k))
Tactic: obtain ⟨k, g, eq⟩ := h (max j j') (F.map (leftToMax _ _) x)
      (F.map (rightToMax _ _) x') (by simpa only [c.ι_naturality_apply])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ Eq (α := F.obj j → c.pt)
    (Function.comp (β := F.obj j')
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j')) :
        (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (((const J).obj c.pt).obj j'))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j')))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) :
      (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((const J).obj c.pt).obj j))
have h : ∀ (x : (fun (X : Type u) ↦ X) (F.obj j)),
  Eq (α := c.pt)
    (Function.comp (β := F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j')) :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (((const J).obj c.pt).obj j'))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j'))
        x :
      c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((const J).obj c.pt).obj j))
        x :
      (fun (X : Type u) ↦ X) (obj.{w, u, v, u + 1} (obj (const J) c.pt) j))
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
⊢ c.IsColimit ↔
    Nonempty
      (Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
        ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c))
have mp : c.IsColimit →
  Nonempty
    (Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
      ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
mp :
  c.IsColimit →
    Nonempty
      (Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
        ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c))
⊢ c.IsColimit ↔
    Nonempty
      (Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
        ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c))
have mpr : Nonempty
    (Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
      ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) →
  c.IsColimit
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Colimits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc : c.IsColimit
s : Cocone F
j : J
⊢ CategoryStruct.comp (Y :=
      obj.{w, u, v, u + 1}
        (obj (const J)
          (Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)))
        j)
      (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j)
      (↾fun
          (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
        hc.desc ((F.coconeTypesEquiv.symm : (a : Cocone F) → F.CoconeTypes) s) x) =
    s.ι.app j
have h : ∀ (x : F.obj j),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          obj.{w, u, v, u + 1}
            (obj (const J)
              (Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)))
            j)
          (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j)
          (↾fun
              (x :
                Cocone.pt.{w, u, v, u + 1} (J := J) (F := F)
                  ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
            hc.desc ((F.coconeTypesEquiv.symm : (a : Cocone F) → F.CoconeTypes) s) x)))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app j)).toFun x
Tactic: ext x