-- 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'
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')))
⊢ ∃ (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'),
  ∃ (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)
Tactic: simp_rw [colimit_eq_iff] at w
Cleared hypotheses: w