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

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
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
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x = colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky y

Tactic:
obtain ⟨S, T, W⟩ := IsFiltered.sup_exists O H

Result:
case intro.intro.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
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
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x = colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky 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),
    limit.π (curry.obj F ⋙ colim) j (colimitLimitToLimitColimit F (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x)) =
      limit.π (curry.obj F ⋙ colim) j (colimitLimitToLimitColimit F (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky y))
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x = colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky y

Tactic:
simp only [Functor.comp_obj, colim_obj, ι_colimitLimitToLimitColimit_π_apply,
  colimit_eq_iff, curry_obj_obj_obj, curry_obj_obj_map] at h

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)
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x = colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky y

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 (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)

Tactic:
rw [← W _ _ (fH j), ← W _ _ (gH j)]

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 (f j ≫ T ⋯)) x) =
    limit.π ((curry.obj (swap K J ⋙ F)).obj S) j (lim.map ((curry.obj (swap K J ⋙ F)).map (g j ≫ T ⋯)) y)