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

Proof state:
case 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
y : colimit (curry.obj (swap K J ⋙ F) ⋙ lim)
kx : K
x : (curry.obj (swap K J ⋙ F) ⋙ lim).obj kx
h : colimitLimitToLimitColimit F (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x) = colimitLimitToLimitColimit F y
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x = y

Tactic:
obtain ⟨ky, y, rfl⟩ := jointly_surjective' y

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

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 :
  colimitLimitToLimitColimit F (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x) =
    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:
replace h := fun j => congr_arg (limit.π (curry.obj F ⋙ colim) j) 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),
    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

Proof state:
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
fH : ∀ (j : J), ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩ ∈ H
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x = colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky y

Tactic:
have gH :
  ∀ j, (⟨ky, k j, kyO, kjO j, g j⟩ : Σ' (X Y : K) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) ∈ H :=
  fun j =>
  Finset.mem_union.mpr
    (Or.inr
      (by
        simp only [true_and, Finset.mem_univ, eq_self_iff_true, exists_prop_of_true,
          Finset.mem_image, heq_iff_eq]
        refine ⟨j, ?_⟩
        simp only [heq_iff_eq]))

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
fH : ∀ (j : J), ⟨kx, ⟨k j, ⟨kxO, ⟨⋯, f j⟩⟩⟩⟩ ∈ H
gH : ∀ (j : J), ⟨ky, ⟨k j, ⟨kyO, ⟨⋯, g j⟩⟩⟩⟩ ∈ H
⊢ 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),
    ∃ 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)
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx x = colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky y

Tactic:
let O : Finset K := Finset.univ.image k ∪ {kx, ky}

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