-- 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 : k' ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun (j : J) ↦
    Finset.biUnion Finset.univ fun (j' : J) ↦
      Finset.biUnion Finset.univ fun (f : j ⟶ j') ↦
        {PSigma.mk (β := fun (X : K) ↦ (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) k'
            (PSigma.mk (β := fun (Y : K) ↦ (_ : k' ∈ O) ×' (_ : Y ∈ O) ×' (k' ⟶ Y)) (kf f)
              (PSigma.mk (β := fun (x : k' ∈ O) ↦ (_ : kf f ∈ O) ×' (k' ⟶ kf f)) k'O
                (PSigma.mk (β := fun (x : kf f ∈ O) ↦ k' ⟶ kf f) ⋯ (gf f)))),
          PSigma.mk (β := fun (X : K) ↦ (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) k'
            (PSigma.mk (β := fun (Y : K) ↦ (_ : k' ∈ O) ×' (_ : Y ∈ O) ×' (k' ⟶ Y)) (kf f)
              (PSigma.mk (β := fun (x : k' ∈ O) ↦ (_ : kf f ∈ O) ×' (k' ⟶ kf f)) k'O
                (PSigma.mk (β := fun (x : kf f ∈ O) ↦ k' ⟶ kf f) ⋯ (hf f))))}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' :
  ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : K) ↦ (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : K) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H →
      f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j' : J} (f : j ⟶ j') ↦ i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ PSigma.mk (β := fun (X : K) ↦ (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) k'
      (PSigma.mk (β := fun (Y : K) ↦ (_ : k' ∈ O) ×' (_ : Y ∈ O) ×' (k' ⟶ Y)) (kf f)
        (PSigma.mk (β := fun (x : k' ∈ O) ↦ (_ : kf f ∈ O) ×' (k' ⟶ kf f)) k'O
          (PSigma.mk (β := fun (x : kf f ∈ O) ↦ k' ⟶ kf f) ⋯ (gf f)))) ∈
    H

Tactic:
exact Finset.mem_biUnion.mpr ⟨j₁, Finset.mem_univ _,
          Finset.mem_biUnion.mpr ⟨j₂, Finset.mem_univ _,
            Finset.mem_biUnion.mpr ⟨f, Finset.mem_univ _, by
              -- This works by `simp`, but has very high variation in heartbeats.
              rw [Finset.mem_insert, PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq,
                PSigma.mk.injEq, heq_eq_eq, PSigma.mk.injEq, heq_eq_eq, eq_self, true_and, eq_self,
                true_and, eq_self, true_and, eq_self, true_and, Finset.mem_singleton, eq_self,
                true_or]
              trivial⟩⟩⟩

Premises used: Iff.mpr, Finset.mem_univ, And.intro, Exists.intro, Finset.mem_biUnion