-- Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
theorem colimitLimitToLimitColimit_injective :
    Function.Injective (colimitLimitToLimitColimit F)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.w
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h :
  ∀ (j : J),
    ∃ k f g,
      F.map (𝟙 j, f) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
        F.map (𝟙 j, g) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
k : J → K := fun j => ⋯.choose
f : (j : J) → kx ⟶ k j := fun j => ⋯.choose
g : (j : J) → ky ⟶ k j := fun j => ⋯.choose
w :
  ∀ (j : J),
    F.map (𝟙 j, f j) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
      F.map (𝟙 j, g j) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
O : Finset K := Finset.image k Finset.univ ∪ {kx, ky}
kxO : kx ∈ O
kyO : ky ∈ O
kjO : ∀ (j : J), k j ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.image (fun j => ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ ∪
    Finset.image (fun j => ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩) Finset.univ
S : K
T : {X : K} → X ∈ O → (X ⟶ S)
W : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ T mY = T mX
fH : ∀ (j : J), ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩ ∈ H
gH : ∀ (j : J), ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩ ∈ H
j : J
⊢ limit.π ((curry.obj (swap K J ⋙ F)).obj S) j ((curry.obj (swap K J ⋙ F) ⋙ lim).map (T kxO) x) =
    limit.π ((curry.obj (swap K J ⋙ F)).obj S) j ((curry.obj (swap K J ⋙ F) ⋙ lim).map (T kyO) y)

Tactic:
simp only [Functor.comp_map, Limit.map_π_apply, curry_obj_map_app, swap_map]

Result:
case intro.intro.intro.intro.intro.intro.intro.w
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h :
  ∀ (j : J),
    ∃ k f g,
      F.map (𝟙 j, f) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
        F.map (𝟙 j, g) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
k : J → K := fun j => ⋯.choose
f : (j : J) → kx ⟶ k j := fun j => ⋯.choose
g : (j : J) → ky ⟶ k j := fun j => ⋯.choose
w :
  ∀ (j : J),
    F.map (𝟙 j, f j) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
      F.map (𝟙 j, g j) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
O : Finset K := Finset.image k Finset.univ ∪ {kx, ky}
kxO : kx ∈ O
kyO : ky ∈ O
kjO : ∀ (j : J), k j ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.image (fun j => ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ ∪
    Finset.image (fun j => ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩) Finset.univ
S : K
T : {X : K} → X ∈ O → (X ⟶ S)
W : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ T mY = T mX
fH : ∀ (j : J), ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩ ∈ H
gH : ∀ (j : J), ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩ ∈ H
j : J
⊢ limit.π ((curry.obj (swap K J ⋙ F)).obj S) j (lim.map ((curry.obj (swap K J ⋙ F)).map (T kxO)) x) =
    limit.π ((curry.obj (swap K J ⋙ F)).obj S) j (lim.map ((curry.obj (swap K J ⋙ F)).map (T kyO)) y)

Proof state:
case intro.intro.intro.intro.intro
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h :
  ∀ (j : J),
    ∃ k f g,
      F.map (𝟙 j, f) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
        F.map (𝟙 j, g) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
k : J → K := fun j => ⋯.choose
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x = colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky y

Tactic:
let f : ∀ j, kx ⟶ k j := fun j => (h j).choose_spec.choose

Result:
case intro.intro.intro.intro.intro
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h :
  ∀ (j : J),
    ∃ k f g,
      F.map (𝟙 j, f) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
        F.map (𝟙 j, g) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
k : J → K := fun j => ⋯.choose
f : (j : J) → kx ⟶ k j := fun j => ⋯.choose
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x = colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky y

Proof state:
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h :
  ∀ (j : J),
    ∃ k f g,
      F.map (𝟙 j, f) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
        F.map (𝟙 j, g) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
k : J → K := fun j => ⋯.choose
f : (j : J) → kx ⟶ k j := fun j => ⋯.choose
g : (j : J) → ky ⟶ k j := fun j => ⋯.choose
w :
  ∀ (j : J),
    F.map (𝟙 j, f j) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
      F.map (𝟙 j, g j) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
O : Finset K := Finset.image k Finset.univ ∪ {kx, ky}
kxO : kx ∈ O
kyO : ky ∈ O
kjO : ∀ (j : J), k j ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.image (fun j => ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ ∪
    Finset.image (fun j => ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩) Finset.univ
S : K
T : {X : K} → X ∈ O → (X ⟶ S)
W : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ T mY = T mX
fH : ∀ (j : J), ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩ ∈ H
j : J
⊢ ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩ ∈ Finset.image (fun j => ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩) Finset.univ

Tactic:
simp only [true_and, Finset.mem_univ, eq_self_iff_true, exists_prop_of_true,
  Finset.mem_image, heq_iff_eq]

Result:
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h :
  ∀ (j : J),
    ∃ k f g,
      F.map (𝟙 j, f) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
        F.map (𝟙 j, g) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
k : J → K := fun j => ⋯.choose
f : (j : J) → kx ⟶ k j := fun j => ⋯.choose
g : (j : J) → ky ⟶ k j := fun j => ⋯.choose
w :
  ∀ (j : J),
    F.map (𝟙 j, f j) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
      F.map (𝟙 j, g j) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y)
O : Finset K := Finset.image k Finset.univ ∪ {kx, ky}
kxO : kx ∈ O
kyO : ky ∈ O
kjO : ∀ (j : J), k j ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.image (fun j => ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ ∪
    Finset.image (fun j => ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩) Finset.univ
S : K
T : {X : K} → X ∈ O → (X ⟶ S)
W : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ T mY = T mX
fH : ∀ (j : J), ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩ ∈ H
j : J
⊢ ∃ a, ⟨ky, ⟨k a, ⟨kyO, ⟨⋯, g a⟩⟩⟩⟩ = ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩