awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
⊢ ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
have refine_1 : ∀ (c : Cocone F), ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
Tactic: obtain ⟨c⟩ := h F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F.op ⋙ Functor.obj yoneda X))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cocone F)
have refine_2 : ∀ (pt : C) (ι : limit (F.op ⋙ Functor.obj yoneda pt)), Nonempty (Cocone F)
Tactic: obtain ⟨pt, ⟨ι⟩⟩ := h F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsCofiltered.{v, u} C ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
have rw : (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
Tactic: rw [IsCofiltered.iff_cone_nonempty.{v}]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
have refine_1 : ∀ (h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) (J : Type v)
  (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C),
  ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
Tactic: refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
refine_1 :
  ∀ (h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) (J : Type v)
    (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
⊢ (∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
have refine_2 : ∀
  (h :
    ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
      ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X))))
  (J : Type v) (x : SmallCategory J) (x_1 : FinCategory J) (F : J ⥤ C), Nonempty (Cone F)
Tactic: refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
⊢ ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
have refine_1 : ∀ (c : Cone F), ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
Tactic: obtain ⟨c⟩ := h F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Filtered (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h :
  ∀ {J : Type v} [inst_1 : SmallCategory J] [FinCategory J] (F : J ⥤ C),
    ∃ (X : C), Nonempty.{v + 1} (limit (F ⋙ Functor.obj coyoneda (op X)))
J : Type v
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cone F)
have refine_2 : ∀ (pt : C) (π : limit (F ⋙ Functor.obj coyoneda (op pt))), Nonempty (Cone F)
Tactic: obtain ⟨pt, ⟨π⟩⟩ := h F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (hypothesis)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
⊢ ∃ (a : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimitLimitToLimitColimit F) :
          (a : (fun (X : Type v) ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))) →
            (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim)))
        a =
      x
have z : ∀ (j : J),
  ∃ (j_1 : K) (y : ((obj curry F).obj j).obj j_1),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) j_1) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj j_1)) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          y :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
Tactic: have z := fun j => jointly_surjective' (limit.π (curry.obj F ⋙ Limits.colim) j x)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K := IsFiltered.sup.{v₂, u₂} (Finset.image k Finset.univ) ∅
⊢ ∃ (a : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimitLimitToLimitColimit F) :
          (a : (fun (X : Type v) ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))) →
            (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim)))
        a =
      x
have have : ∀ (g : (j : J) → k j ⟶ k'),
  ∃ (a : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimitLimitToLimitColimit F) :
          (a : (fun (X : Type v) ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))) →
            (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim)))
        a =
      x
Tactic: have g : ∀ j, k j ⟶ k' := fun j => IsFiltered.toSup (Finset.univ.image k) ∅ (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K := IsFiltered.sup.{v₂, u₂} (Finset.image k Finset.univ) ∅
g : (j : J) → k j ⟶ k'
⊢ ∃ (a : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimitLimitToLimitColimit F) :
          (a : (fun (X : Type v) ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))) →
            (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim)))
        a =
      x
have clear_value : ∀ (k' : K) (g : (j : J) → k j ⟶ k'),
  ∃ (a : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimitLimitToLimitColimit F) :
          (a : (fun (X : Type v) ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))) →
            (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim)))
        a =
      x
Tactic: clear_value k'
Cleared hypotheses: k', g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
j j' : J
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j') k') :
          (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j').obj k')) →
            (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) :
              (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', k')))
            (y j') :
          (fun (X : Type v) ↦ X) (F.obj (j', k'))) :
      (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j') k') :
          (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j').obj k')) →
            (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ 𝟙 (k j)) ≫ F.map (𝟙 j' ×ₘ g j)) :
              (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k')))
            (y j) :
          (fun (X : Type v) ↦ X) (F.obj (j', k'))) :
      (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j')))
have simp : Eq (α := colimit ((obj curry F).obj j'))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j') (k j')) :
        (a : ((curry.obj F).obj j').obj (k j')) → colimit ((curry.obj F).obj j'))
      (y j') :
    colimit ((obj curry F).obj j'))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j') (k j)) :
        (a : ((curry.obj F).obj j').obj (k j)) → colimit ((curry.obj F).obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ 𝟙 (k j))) :
            (a : ((curry.obj F).obj j).obj (k j)) → ((curry.obj F).obj j').obj (k j))
          (y j) :
        ((obj curry F).obj j').obj (k j)) :
    colimit ((obj curry F).obj j'))
Tactic: simp only [← curry_obj_obj_map, ← curry_obj_obj_obj, comp_apply, colimit.w_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
j j' : J
f : j ⟶ j'
⊢ Eq (α := colimit ((obj curry F).obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j') (k j')) :
          (a : ((curry.obj F).obj j').obj (k j')) → colimit ((curry.obj F).obj j'))
        (y j') :
      colimit ((obj curry F).obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j') (k j)) :
          (a : ((curry.obj F).obj j').obj (k j)) → colimit ((curry.obj F).obj j'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ 𝟙 (k j))) :
              (a : ((curry.obj F).obj j).obj (k j)) → ((curry.obj F).obj j').obj (k j))
            (y j) :
          ((obj curry F).obj j').obj (k j)) :
      colimit ((obj curry F).obj j'))
have rw : Eq (α := colimit ((obj curry F).obj j'))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((obj curry F ⋙ colim).map f) :
        (a : (curry.obj F ⋙ colim).obj j) → (curry.obj F ⋙ colim).obj j')
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j))) :
    (obj curry F ⋙ colim).obj j')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j') (k j)) :
        (a : ((curry.obj F).obj j').obj (k j)) → colimit ((curry.obj F).obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ 𝟙 (k j))) :
            (a : ((curry.obj F).obj j).obj (k j)) → ((curry.obj F).obj j').obj (k j))
          (y j) :
        ((obj curry F).obj j').obj (k j)) :
    colimit ((obj curry F).obj j'))
Tactic: rw [e, ← limit.w_apply _ f, ← e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (hypothesis)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
⊢ ∃ (a : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimitLimitToLimitColimit F) :
          (a : (fun (X : Type v) ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))) →
            (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim)))
        a =
      x
have w : ∀ {j j' : J} (f : j ⟶ j'),
  Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j') k') :
          (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j').obj k')) →
            (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) :
              (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', k')))
            (y j') :
          (fun (X : Type v) ↦ X) (F.obj (j', k'))) :
      (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j') k') :
          (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j').obj k')) →
            (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j')))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j)) :
              (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k')))
            (y j) :
          (fun (X : Type v) ↦ X) (F.obj (j', k'))) :
      (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j')))
Tactic: have w :
      ∀ {j j' : J} (f : j ⟶ j'),
        colimit.ι ((curry.obj F).obj j') k' (F.map (𝟙 j' ×ₘ g j') (y j')) =
          colimit.ι ((curry.obj F).obj j') k' (F.map (f ×ₘ g j) (y j)) := by
      intro j j' f
      nth_rw 2 [← Bifunctor.diagonal']
      simp only [← curry_obj_obj_map, ← curry_obj_obj_obj, comp_apply, colimit.w_apply]
      rw [e, ← limit.w_apply _ f, ← e]
      simp [-curry_obj_obj_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (hypothesis)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
O : Finset K :=
  (Finset.biUnion Finset.univ fun (j : J) ↦
      Finset.biUnion Finset.univ fun (j' : J) ↦ Finset.image.{u₁, u₂} (α := j ⟶ j') kf Finset.univ) ∪
    {k'}
⊢ ∃ (a : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimitLimitToLimitColimit F) :
          (a : (fun (X : Type v) ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))) →
            (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim)))
        a =
      x
have kfO : ∀ {j j' : J} (f : j ⟶ j'), kf f ∈ O
Tactic: have kfO : ∀ {j j'} (f : j ⟶ j'), kf f ∈ O := fun {j} {j'} f =>
      Finset.mem_union.mpr
        (Or.inl
          (Finset.mem_biUnion.mpr ⟨j, Finset.mem_univ j,
            Finset.mem_biUnion.mpr ⟨j', Finset.mem_univ j',
              Finset.mem_image.mpr ⟨f, Finset.mem_univ _, rfl⟩⟩⟩))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (hypothesis)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
O : Finset K :=
  (Finset.biUnion Finset.univ fun (j : J) ↦
      Finset.biUnion Finset.univ fun (j' : J) ↦ Finset.image.{u₁, u₂} (α := j ⟶ j') kf Finset.univ) ∪
    {k'}
kfO : ∀ {j j' : J} (f : j ⟶ j'), kf f ∈ O
⊢ ∃ (a : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimitLimitToLimitColimit F) :
          (a : (fun (X : Type v) ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))) →
            (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim)))
        a =
      x
have k'O : k' ∈ O
Tactic: have k'O : k' ∈ O := Finset.mem_union.mpr (Or.inr (Finset.mem_singleton.mpr rfl))