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

Proof state:
case intro.intro.h.w
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)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j : J
⊢ ∃ k_1 f g_1, F.map (𝟙 j, f) (F.map (𝟙 j, g j ≫ gf (𝟙 j) ≫ i (𝟙 j)) (y j)) = F.map (𝟙 j, g_1) (y j)

Tactic:
refine ⟨k'', 𝟙 k'', g j ≫ gf (𝟙 j) ≫ i (𝟙 j), ?_⟩

Result:
case intro.intro.h.w
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)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j : J
⊢ F.map (𝟙 j, 𝟙 k'') (F.map (𝟙 j, g j ≫ gf (𝟙 j) ≫ i (𝟙 j)) (y j)) = F.map (𝟙 j, g j ≫ gf (𝟙 j) ≫ i (𝟙 j)) (y j)

Proof state:
case intro.intro.h
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)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ colimitLimitToLimitColimit F
      (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) k''
        (id (Limit.mk ((curry.obj (swap K J ⋙ F)).obj k'') (fun j => F.map (𝟙 j, g j ≫ gf (𝟙 j) ≫ i (𝟙 j)) (y j)) ⋯))) =
    x

Tactic:
apply limit_ext

Result:
case intro.intro.h.w
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)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ ∀ (j : J),
    limit.π (curry.obj F ⋙ colim) j
        (colimitLimitToLimitColimit F
          (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) k''
            (id
              (Limit.mk ((curry.obj (swap K J ⋙ F)).obj k'') (fun j => F.map (𝟙 j, g j ≫ gf (𝟙 j) ≫ i (𝟙 j)) (y j))
                ⋯)))) =
      limit.π (curry.obj F ⋙ colim) j 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'
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
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f => i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ True

Tactic:
trivial

Result:
no goals

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)
z : ∀ (j : J), ∃ j_1 y, colimit.ι ((curry.obj F).obj j) j_1 y = limit.π (curry.obj F ⋙ colim) j x
k : J → K := fun j => ⋯.choose
⊢ ∃ a, colimitLimitToLimitColimit F a = x

Tactic:
let y : ∀ j, F.obj (j, k j) := fun j => (z j).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)
z : ∀ (j : J), ∃ j_1 y, colimit.ι ((curry.obj F).obj j) j_1 y = limit.π (curry.obj F ⋙ colim) j x
k : J → K := fun j => ⋯.choose
y : (j : J) → F.obj (j, k j) := fun j => ⋯.choose
⊢ ∃ 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)
z : ∀ (j : J), ∃ j_1 y, colimit.ι ((curry.obj F).obj j) j_1 y = limit.π (curry.obj F ⋙ colim) j x
⊢ ∃ a, colimitLimitToLimitColimit F a = x

Tactic:
let k : J → K := fun j => (z j).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)
z : ∀ (j : J), ∃ j_1 y, colimit.ι ((curry.obj F).obj j) j_1 y = limit.π (curry.obj F ⋙ colim) j x
k : J → K := fun j => ⋯.choose
⊢ ∃ a, colimitLimitToLimitColimit F a = x