-- 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'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ (k_1 : K) (f_1 : k' ⟶ k_1) (g_1 : k' ⟶ k_1),
      Eq (α := ((obj curry F).obj j').obj k_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map f_1) :
              (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) : (a : F.obj (j', k j')) → F.obj (j', k'))
                (y j') :
              F.obj (j', k')) :
          ((obj curry F).obj j').obj k_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map g_1) :
              (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j)) : (a : F.obj (j, k j)) → F.obj (j', k'))
                (y j) :
              F.obj (j', k')) :
          ((obj curry F).obj j').obj k_1)
kf : {j j' : J} → (j ⟶ j') → K :=
  fun {j j' : J} (f : j ⟶ j') ↦
    ⋯.choose (p := fun (k_1 : K) ↦
      ∃ (f_1 : k' ⟶ k_1) (g_1 : k' ⟶ k_1),
        Eq (α := ((obj curry F).obj j').obj k_1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map f_1) :
                (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) :
                    (a : F.obj (j', k j')) → F.obj (j', k'))
                  (y j') :
                F.obj (j', k')) :
            ((obj curry F).obj j').obj k_1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map g_1) :
                (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j)) : (a : F.obj (j, k j)) → F.obj (j', k'))
                  (y j) :
                F.obj (j', k')) :
            ((obj curry F).obj j').obj k_1))
gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f :=
  fun {j j' : J} (f : j ⟶ j') ↦
    ⋯.choose (p :=
      fun
        (f_1 :
          k' ⟶
            ⋯.choose (p := fun (k_1 : K) ↦
              ∃ (f_1 : k' ⟶ k_1) (g_1 : k' ⟶ k_1),
                Eq (α := ((obj curry F).obj j').obj k_1)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map f_1) :
                        (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) :
                            (a : F.obj (j', k j')) → F.obj (j', k'))
                          (y j') :
                        F.obj (j', k')) :
                    ((obj curry F).obj j').obj k_1)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map g_1) :
                        (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j)) :
                            (a : F.obj (j, k j)) → F.obj (j', k'))
                          (y j) :
                        F.obj (j', k')) :
                    ((obj curry F).obj j').obj k_1))) ↦
      ∃ (g_1 :
        k' ⟶
          ⋯.choose (p := fun (k_1 : K) ↦
            ∃ (f_2 : k' ⟶ k_1) (g_1 : k' ⟶ k_1),
              Eq (α := ((obj curry F).obj j').obj k_1)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map f_2) :
                      (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) :
                          (a : F.obj (j', k j')) → F.obj (j', k'))
                        (y j') :
                      F.obj (j', k')) :
                  ((obj curry F).obj j').obj k_1)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map g_1) :
                      (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j)) :
                          (a : F.obj (j, k j)) → F.obj (j', k'))
                        (y j) :
                      F.obj (j', k')) :
                  ((obj curry F).obj j').obj k_1))),
        Eq (α :=
          ((obj curry F).obj j').obj
            (⋯.choose (p := fun (k_1 : K) ↦
              ∃ (f_2 : k' ⟶ k_1) (g_2 : k' ⟶ k_1),
                Eq (α := ((obj curry F).obj j').obj k_1)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map f_2) :
                        (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) :
                            (a : F.obj (j', k j')) → F.obj (j', k'))
                          (y j') :
                        F.obj (j', k')) :
                    ((obj curry F).obj j').obj k_1)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map g_2) :
                        (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j)) :
                            (a : F.obj (j, k j)) → F.obj (j', k'))
                          (y j) :
                        F.obj (j', k')) :
                    ((obj curry F).obj j').obj k_1))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map f_1) :
                (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj ⋯.choose)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) :
                    (a : F.obj (j', k j')) → F.obj (j', k'))
                  (y j') :
                F.obj (j', k')) :
            ((obj curry F).obj j').obj
              (⋯.choose (p := fun (k_1 : K) ↦
                ∃ (f_2 : k' ⟶ k_1) (g_2 : k' ⟶ k_1),
                  Eq (α := ((obj curry F).obj j').obj k_1)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map f_2) :
                          (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) :
                              (a : F.obj (j', k j')) → F.obj (j', k'))
                            (y j') :
                          F.obj (j', k')) :
                      ((obj curry F).obj j').obj k_1)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map g_2) :
                          (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j)) :
                              (a : F.obj (j, k j)) → F.obj (j', k'))
                            (y j) :
                          F.obj (j', k')) :
                      ((obj curry F).obj j').obj k_1))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map g_1) :
                (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj ⋯.choose)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j)) : (a : F.obj (j, k j)) → F.obj (j', k'))
                  (y j) :
                F.obj (j', k')) :
            ((obj curry F).obj j').obj
              (⋯.choose (p := fun (k_1 : K) ↦
                ∃ (f_2 : k' ⟶ k_1) (g_2 : k' ⟶ k_1),
                  Eq (α := ((obj curry F).obj j').obj k_1)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map f_2) :
                          (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j')) :
                              (a : F.obj (j', k j')) → F.obj (j', k'))
                            (y j') :
                          F.obj (j', k')) :
                      ((obj curry F).obj j').obj k_1)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j').map g_2) :
                          (a : ((curry.obj F).obj j').obj k') → ((curry.obj F).obj j').obj k_1)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j)) :
                              (a : F.obj (j, k j)) → F.obj (j', k'))
                            (y j) :
                          F.obj (j', k')) :
                      ((obj curry F).obj j').obj k_1)))))
hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ {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)))

Tactic:
have wf :
      ∀ {j j'} (f : j ⟶ j'),
        F.map (𝟙 j' ×ₘ (g j' ≫ gf f)) (y j') = F.map (f ×ₘ (g j ≫ hf f)) (y j) :=
      fun {j j'} f => by
      have q :
        ((curry.obj F).obj j').map (gf f) (F.map (𝟙 j' ×ₘ g j') (y j')) =
          ((curry.obj F).obj j').map (hf f) (F.map (f ×ₘ g j) (y j)) :=
        (w f).choose_spec.choose_spec.choose_spec
      convert! q using 1
      · simp [← comp_apply, -types_comp_apply]
      · simp [← comp_apply, -types_comp_apply, ← F.map_comp]