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₀)
j : J
x y : F.obj j
⊢ 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))
have 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))
Tactic: rw [ιColimitType_eq_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₀)
j : J
x y : F.obj j
⊢ (∃ (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))
have mp : (∃ (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))
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₀)
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))
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')))
      y :
    (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₀)
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')))
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')))
      y :
    (fun (X : Type w₀) ↦ X) (F.obj (coeq f f')))
Tactic: nth_rw 2 [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
⊢ 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))
have 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))
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
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))
⊢ 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))
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (hypothesis)
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'
⊢ ∃ (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 this : F.ιColimitType j x = F.ιColimitType j' x'
Tactic: have : F.ιColimitType j x = F.ιColimitType j' x' := 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 : 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'
⊢ ∃ (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 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))
Tactic: rwa [ιColimitType_eq_iff_of_isFiltered] at this
Cleared hypotheses: this
-- 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))
x x' : F.ColimitType
eq : F.descColimitType c x = F.descColimitType c x'
⊢ x = x'
have mpr : ∀ (i : J) (x : F.obj i) (eq : F.descColimitType c (F.ιColimitType i x) = F.descColimitType c x'),
  F.ιColimitType i x = x'
Tactic: obtain ⟨i, x, rfl⟩ := F.ιColimitType_jointly_surjective x
Cleared hypotheses: x, 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))
x' : F.ColimitType
i : J
x : F.obj i
eq : F.descColimitType c (F.ιColimitType i x) = F.descColimitType c x'
⊢ F.ιColimitType i x = x'
have 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'
Tactic: obtain ⟨i', x', rfl⟩ := F.ιColimitType_jointly_surjective x'
Cleared hypotheses: x', 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))
i : J
x : F.obj i
i' : J
x' : F.obj i'
eq : c.ι i x = c.ι i' x'
⊢ F.ιColimitType i x = F.ιColimitType i' x'
have 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'
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))
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))
⊢ F.ιColimitType i x = F.ιColimitType i' x'
have 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'
Tactic: rw [← F.ιColimitType_map f x, eq, F.ιColimitType_map]
-- 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))
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'
⊢ F.ιColimitType i x = F.ιColimitType i' x'
have 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'
Tactic: rw [← F.ιColimitType_map f x, eq, F.ιColimitType_map]
-- 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))
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'
⊢ F.ιColimitType i x = F.ιColimitType i' x'
have mpr₂ : F.ιColimitType i' x' = F.ιColimitType i' x'
Tactic: rw [← F.ιColimitType_map f x, eq, F.ιColimitType_map]