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

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'
j j' : J
f : j ⟶ j'
t : (f, g j) = (f, 𝟙 (k j)) ≫ (𝟙 j', g j)
⊢ colimit.ι ((curry.obj F).obj j') k' (F.map (𝟙 j', g j') (y j')) =
    colimit.ι ((curry.obj F).obj j') k' (F.map (f, g j) (y j))

Tactic:
erw [Colimit.w_apply, t, FunctorToTypes.map_comp_apply, Colimit.w_apply, e,
  ← Limit.w_apply.{u₁, v, u₁} f, ← e]

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'
j j' : J
f : j ⟶ j'
t : (f, g j) = (f, 𝟙 (k j)) ≫ (𝟙 j', g j)
⊢ (curry.obj F ⋙ colim).map f (colimit.ι ((curry.obj F).obj j) (k j) (y j)) =
    colimit.ι ((curry.obj F).obj j') (k j) (F.map (f, 𝟙 (k j)) (y j))

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⟩⟩⟩⟩}
⊢ ∃ a, colimitLimitToLimitColimit F a = x

Tactic:
obtain ⟨k'', i', s'⟩ := IsFiltered.sup_exists O H

Result:
case intro.intro
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
⊢ ∃ a, colimitLimitToLimitColimit F a = x

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
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)
⊢ ∃ a, colimitLimitToLimitColimit F a = x

Tactic:
clear w

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)
⊢ ∃ a, colimitLimitToLimitColimit F a = x

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
⊢ ∃ a, colimitLimitToLimitColimit F a = x

Tactic:
let hf : ∀ {j j'} (f : j ⟶ j'), k' ⟶ kf f := fun f =>
  (w f).choose_spec.choose_spec.choose

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
⊢ ∃ a, colimitLimitToLimitColimit F a = x