-- 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'
j : J
pf : HasColimit ((obj curry F).obj j)
pf_1 : HasColimit ((obj curry F).obj j)
pf_2 : HasColimitsOfShape.{v₂, u₂, v, v + 1} K (Type v)
pf_3 : HasLimit ((obj curry (swap K J ⋙ F)).obj k'')
pf_4 : HasLimitsOfShape J (Type v)
h :
  ∀ (j j' : J) (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (((obj curry (swap K J ⋙ F)).obj k'').obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry (swap K J ⋙ F)).obj k'').map f) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj (swap K J ⋙ F)).obj k'').obj j)) →
              (fun (X : Type v) ↦ X) (((curry.obj (swap K J ⋙ F)).obj k'').obj j'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ i (𝟙 j))) :
                (a : F.obj (j, kf (𝟙 j))) → F.obj (j, k''))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ gf (𝟙 j))) :
                    (a : F.obj (j, k')) → F.obj (j, kf (𝟙 j)))
                  ((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')) :
                F.obj (j, kf (𝟙 j))) :
            F.obj (j, k'')) :
        (fun (X : Type v) ↦ X) (((obj curry (swap K J ⋙ F)).obj k'').obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ i (𝟙 j'))) :
            (a : F.obj (j', kf (𝟙 j'))) → F.obj (j', k''))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ gf (𝟙 j'))) :
                (a : F.obj (j', k')) → F.obj (j', kf (𝟙 j')))
              ((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')) :
            F.obj (j', kf (𝟙 j'))) :
        F.obj (j', k''))
pf_5 : HasLimit (obj curry F ⋙ colim)
h₁ :
  Eq (α := (fun (X : Type v) ↦ X) (((obj curry F).obj j).obj k''))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j).map (𝟙 k'')) :
          (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj k'')) →
            (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj k''))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ i (𝟙 j))) :
              (a : ((curry.obj F).obj j).obj (kf (𝟙 j))) → ((curry.obj F).obj j).obj k'')
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ gf (𝟙 j))) :
                  (a : ((curry.obj F).obj j).obj k') → ((curry.obj F).obj j).obj (kf (𝟙 j)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ g j)) :
                      (a : ((curry.obj F).obj j).obj (k j)) → ((curry.obj F).obj j).obj k')
                    (y j) :
                  ((obj curry F).obj j).obj k') :
              ((obj curry F).obj j).obj (kf (𝟙 j))) :
          ((obj curry F).obj j).obj k'') :
      (fun (X : Type v) ↦ X) (((obj curry F).obj j).obj k''))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j).map (g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
          (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
            (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj k''))
        (y j) :
      (fun (X : Type v) ↦ X) (((obj curry F).obj j).obj k''))
⊢ ∃ (k_1 : K) (f : k'' ⟶ k_1) (g_1 : k j ⟶ k_1),
    Eq (α := (fun (X : Type v) ↦ X) (((obj curry F).obj j).obj k_1))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j).map f) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj k'')) →
              (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj k_1))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ i (𝟙 j))) :
                (a : ((curry.obj F).obj j).obj (kf (𝟙 j))) → ((curry.obj F).obj j).obj k'')
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ gf (𝟙 j))) :
                    (a : ((curry.obj F).obj j).obj k') → ((curry.obj F).obj j).obj (kf (𝟙 j)))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ g j)) :
                        (a : ((curry.obj F).obj j).obj (k j)) → ((curry.obj F).obj j).obj k')
                      (y j) :
                    ((obj curry F).obj j).obj k') :
                ((obj curry F).obj j).obj (kf (𝟙 j))) :
            ((obj curry F).obj j).obj k'') :
        (fun (X : Type v) ↦ X) (((obj curry F).obj j).obj k_1))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry F).obj j).map g_1) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj k_1))
          (y j) :
        (fun (X : Type v) ↦ X) (((obj curry F).obj j).obj k_1))

Tactic:
refine ⟨k'', 𝟙 k'', g j ≫ gf (𝟙 j) ≫ i (𝟙 j), ?_⟩