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

Tactic:
have kjO : ∀ j, k j ∈ O := fun j => Finset.mem_union.mpr (Or.inl (by simp))

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}
kxO : kx ∈ O
kyO : ky ∈ O
kjO : ∀ (j : J), k j ∈ O
⊢ 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 : (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

Tactic:
dsimp at x 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 : 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

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}
⊢ kx ∈ {kx, ky}

Tactic:
simp

Result:
no goals

Proof state:
case 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
⊢ Function.Injective (colimitLimitToLimitColimit F)

Tactic:
intro x y h

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

Tactic:
classical
  cases nonempty_fintype J
  intro x y h
  obtain ⟨kx, x, rfl⟩ := jointly_surjective' x
  obtain ⟨ky, y, rfl⟩ := jointly_surjective' y
  dsimp at x y
  replace h := fun j => congr_arg (limit.π (curry.obj F ⋙ colim) j) h
  simp? [colimit_eq_iff] at h says
    simp only [Functor.comp_obj, colim_obj, ι_colimitLimitToLimitColimit_π_apply,
      colimit_eq_iff, curry_obj_obj_obj, curry_obj_obj_map] at h
  let k j := (h j).choose
  let f : ∀ j, kx ⟶ k j := fun j => (h j).choose_spec.choose
  let g : ∀ j, ky ⟶ k j := fun j => (h j).choose_spec.choose_spec.choose
  have w :
    ∀ j, F.map ((𝟙 j, f j) :
      (j, kx) ⟶ (j, k j)) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
        F.map ((𝟙 j, g j) : (j, ky) ⟶ (j, k j))
          (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y) :=
    fun j => (h j).choose_spec.choose_spec.choose_spec
  let O : Finset K := Finset.univ.image k ∪ {kx, ky}
  have kxO : kx ∈ O := Finset.mem_union.mpr (Or.inr (by simp))
  have kyO : ky ∈ O := Finset.mem_union.mpr (Or.inr (by simp))
  have kjO : ∀ j, k j ∈ O := fun j => Finset.mem_union.mpr (Or.inl (by simp))
  let H : Finset (Σ' (X Y : K) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
    (Finset.univ.image fun j : J =>
        ⟨kx, k j, kxO, Finset.mem_union.mpr (Or.inl (by simp)), f j⟩) ∪
      Finset.univ.image fun j : J => ⟨ky, k j, kyO, Finset.mem_union.mpr (Or.inl (by simp)), g j⟩
  obtain ⟨S, T, W⟩ := IsFiltered.sup_exists O H
  have fH : ∀ j, (⟨kx, k j, kxO, kjO j, f j⟩ : Σ' (X Y : K) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) ∈ H :=
    fun j =>
    Finset.mem_union.mpr
      (Or.inl
        (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] ))
  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]))
  apply colimit_sound' (T kxO) (T kyO)
  ext j
  simp only [Functor.comp_map, Limit.map_π_apply, curry_obj_map_app, swap_map]
  rw [← W _ _ (fH j), ← W _ _ (gH j)]
  simp [Limit.map_π_apply, w]

Result:
no goals