-- Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
theorem colimitLimitToLimitColimit_surjective :
    Function.Surjective (colimitLimitToLimitColimit F)

Proof state:
case a
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e : ∀ (j : J), colimit.ι ((curry.obj F).obj j) (k j) (y j) = limit.π (curry.obj F ⋙ colim) j x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
hf gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf : ∀ {j j' : J} (f : j ⟶ j'), F.map (𝟙 j', g j' ≫ gf f) (y j') = F.map (f, g j ≫ hf f) (y j)
O : Finset K := (Finset.univ.biUnion fun j => Finset.univ.biUnion fun j' => Finset.image 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.univ.biUnion fun j =>
    Finset.univ.biUnion fun j' =>
      Finset.univ.biUnion fun f => {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f => i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ ⟨k', ⟨kf f', ⟨k'O, ⟨⋯, hf 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
      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,
        or_true]
      trivial⟩⟩⟩

Result:
no goals

Proof state:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e : ∀ (j : J), colimit.ι ((curry.obj F).obj j) (k j) (y j) = limit.π (curry.obj F ⋙ colim) j x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
hf gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf : ∀ {j j' : J} (f : j ⟶ j'), F.map (𝟙 j', g j' ≫ gf f) (y j') = F.map (f, g j ≫ hf f) (y j)
O : Finset K := (Finset.univ.biUnion fun j => Finset.univ.biUnion fun j' => Finset.image 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.univ.biUnion fun j =>
    Finset.univ.biUnion fun j' =>
      Finset.univ.biUnion fun f => {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f => i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩ ∈ {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}

Tactic:
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]

Result:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e : ∀ (j : J), colimit.ι ((curry.obj F).obj j) (k j) (y j) = limit.π (curry.obj F ⋙ colim) j x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
hf gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf : ∀ {j j' : J} (f : j ⟶ j'), F.map (𝟙 j', g j' ≫ gf f) (y j') = F.map (f, g j ≫ hf f) (y j)
O : Finset K := (Finset.univ.biUnion fun j => Finset.univ.biUnion fun j' => Finset.image 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.univ.biUnion fun j =>
    Finset.univ.biUnion fun j' =>
      Finset.univ.biUnion fun f => {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f => i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ True

Proof state:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e : ∀ (j : J), colimit.ι ((curry.obj F).obj j) (k j) (y j) = limit.π (curry.obj F ⋙ colim) j x
k' : K
g : (j : J) → k j ⟶ k'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      ((curry.obj F).obj j').map f_1 (F.map (𝟙 j', g j') (y j')) = ((curry.obj F).obj j').map g_1 (F.map (f, g j) (y j))
kf : {j j' : J} → (j ⟶ j') → K := fun {j j'} f => ⋯.choose
gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f => ⋯.choose
hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f => ⋯.choose
j j' : J
f : j ⟶ j'
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))
⊢ F.map (𝟙 j', g j' ≫ gf f) (y j') = F.map (f, g j ≫ hf f) (y j)

Tactic:
rw [curry_obj_obj_map, curry_obj_obj_map] at q

Result:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e : ∀ (j : J), colimit.ι ((curry.obj F).obj j) (k j) (y j) = limit.π (curry.obj F ⋙ colim) j x
k' : K
g : (j : J) → k j ⟶ k'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      ((curry.obj F).obj j').map f_1 (F.map (𝟙 j', g j') (y j')) = ((curry.obj F).obj j').map g_1 (F.map (f, g j) (y j))
kf : {j j' : J} → (j ⟶ j') → K := fun {j j'} f => ⋯.choose
gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f => ⋯.choose
hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f => ⋯.choose
j j' : J
f : j ⟶ j'
q : F.map (𝟙 j', gf f) (F.map (𝟙 j', g j') (y j')) = F.map (𝟙 j', hf f) (F.map (f, g j) (y j))
⊢ F.map (𝟙 j', g j' ≫ gf f) (y j') = F.map (f, g j ≫ hf f) (y j)