-- 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)
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))
k : J → K :=
  fun (j : J) ↦
    ⋯.choose (p := fun (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)))
y : (j : J) → F.obj (j, k j) :=
  fun (j : J) ↦
    ⋯.choose (p :=
      fun
        (y :
          ((obj curry F).obj j).obj
            (⋯.choose (p := fun (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))))) ↦
      Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (colimit.ι ((obj curry F).obj j)
                  (⋯.choose (p := fun (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))))) :
              (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj ⋯.choose)) →
                (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)))
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))
clear_value :
  ∀ (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))),
    ∃ (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 y