awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{w', w, v, u} C
I : Type w
inst_2 : Category.{w', w} I
inst_3 : IsCofiltered.{w', w} I
⊢ HasLimitsOfShape.{w', w, v, u} I C

Tactic:
HasCofilteredLimitsOfSize.HasLimitsOfShape _

Premises used: CategoryTheory.Limits.HasCofilteredLimitsOfSize.HasLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{w', w, v, u} C
I : Type w
inst_2 : Category.{w', w} I
inst_3 : IsFiltered.{w', w} I
⊢ HasColimitsOfShape.{w', w, v, u} I C

Tactic:
HasFilteredColimitsOfSize.HasColimitsOfShape _

Premises used: CategoryTheory.Limits.HasFilteredColimitsOfSize.HasColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCofilteredLimitsOfSize.{max w' w₂', max w w₂, v, u} C
⊢ HasCofilteredLimitsOfSize.{w', w, v, u} C

Tactic:
hasCofilteredLimitsOfSize_of_univLE.{w', w, max w' w₂', max w w₂}

Premises used: CategoryTheory.Limits.hasCofilteredLimitsOfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Limits.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFilteredColimitsOfSize.{max w' w₂', max w w₂, v, u} C
⊢ HasFilteredColimitsOfSize.{w', w, v, u} C

Tactic:
hasFilteredColimitsOfSize_of_univLE.{w', w, max w' w₂', max w w₂}

Premises used: CategoryTheory.Limits.hasFilteredColimitsOfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
j : J
G : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
x y : (G ⋙ lim).obj j
w :
  ∀ (k : K),
    Eq (α := (fun (X : Type v) ↦ X) ((G.obj j).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (G.obj j) k) :
            (a : (fun (X : Type v) ↦ X) (limit (G.obj j))) → (fun (X : Type v) ↦ X) ((G.obj j).obj k))
          x :
        (fun (X : Type v) ↦ X) ((G.obj j).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (G.obj j) k) :
            (a : (fun (X : Type v) ↦ X) (limit (G.obj j))) → (fun (X : Type v) ↦ X) ((G.obj j).obj k))
          y :
        (fun (X : Type v) ↦ X) ((G.obj j).obj k))
⊢ x = y

Tactic:
limit_ext _ x y w

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.Types.limit_ext
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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)
⊢ ∀ (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)
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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) ∅
j : J
⊢ k j ∈ Finset.image k Finset.univ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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) ∅
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
⊢ ∃ (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)
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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'
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
⊢ ∃ (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'
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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'
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'))
⊢ 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:
rw [e, ← limit.w_apply _ f, ← e]

Premises used: CategoryTheory.Limits.limit.w_apply
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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) ((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:
simp [-curry_obj_obj_obj]

Premises used: CategoryTheory.Functor.curry_obj_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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 ×ₘ 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]
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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'}
⊢ ∀ {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⟩⟩⟩))
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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
⊢ k' ∈ O

Tactic:
have k'O : k' ∈ O := Finset.mem_union.mpr (Or.inr (Finset.mem_singleton.mpr rfl))
-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
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)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
apply : (obj curry (swap K J ⋙ F) ⋙ lim).obj k''
⊢ (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))

Tactic:
apply colimit.ι (curry.obj (swap K J ⋙ F) ⋙ Limits.lim) k'' _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.comp, CategoryTheory.Limits.lim, CategoryTheory.Functor.curry, CategoryTheory.Prod.swap, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.Limits.colimit.ι