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

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'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      ((curry.obj F).obj j').map f_1 (F.map (𝟙 j', g j') (y j')) = ((curry.obj F).obj j').map g_1 (F.map (f, g j) (y j))
kf : {j j' : J} → (j ⟶ j') → K := fun {j j'} f => ⋯.choose
gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f => ⋯.choose
hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f => ⋯.choose
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)
⊢ ∃ a, colimitLimitToLimitColimit F a = x

Tactic:
clear_value kf gf hf

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)
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'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      ((curry.obj F).obj j').map f_1 (F.map (𝟙 j', g j') (y j')) = ((curry.obj F).obj j').map g_1 (F.map (f, g j) (y j))
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)
⊢ ∃ 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)
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' : J
f : j ⟶ j'
⊢ F.map (𝟙 j', i f) (F.map (𝟙 j', g j' ≫ gf f) (y j')) = F.map (𝟙 j', g j' ≫ gf f ≫ i f) (y j')

Tactic:
rw [← FunctorToTypes.map_comp_apply, prod_comp, id_comp, assoc]

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)
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'
⊢ ∀ {j j' : J} (f : j ⟶ j'),
    colimit.ι ((curry.obj F).obj j') k' (F.map (𝟙 j', g j') (y j')) =
      colimit.ι ((curry.obj F).obj j') k' (F.map (f, g j) (y j))

Tactic:
intro j j' f

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)
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'
j j' : J
f : j ⟶ j'
⊢ colimit.ι ((curry.obj F).obj j') k' (F.map (𝟙 j', g j') (y j')) =
    colimit.ι ((curry.obj F).obj j') k' (F.map (f, g j) (y j))

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'
j j' : J
f : j ⟶ j'
⊢ colimit.ι ((curry.obj F).obj j') k' (F.map (𝟙 j', g j') (y j')) =
    colimit.ι ((curry.obj F).obj j') k' (F.map (f, g j) (y j))

Tactic:
have t : (f, g j) =
    (((f, 𝟙 (k j)) : (j, k j) ⟶ (j', k j)) ≫ (𝟙 j', g j) : (j, k j) ⟶ (j', k')) := by
  simp only [id_comp, comp_id, prod_comp]

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)
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'
j j' : J
f : j ⟶ j'
t : (f, g j) = (f, 𝟙 (k j)) ≫ (𝟙 j', g j)
⊢ colimit.ι ((curry.obj F).obj j') k' (F.map (𝟙 j', g j') (y j')) =
    colimit.ι ((curry.obj F).obj j') k' (F.map (f, g j) (y j))

Proof state:
case 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'
j j' : J
f : j ⟶ j'
⊢ F.map (f, g j ≫ gf (𝟙 j) ≫ i (𝟙 j)) (y j) = F.map (𝟙 j', g j' ≫ gf (𝟙 j') ≫ i (𝟙 j')) (y j')

Tactic:
calc
  F.map ((f, g j ≫ gf (𝟙 j) ≫ i (𝟙 j)) : (j, k j) ⟶ (j', k'')) (y j) =
      F.map ((f, g j ≫ hf f ≫ i f) : (j, k j) ⟶ (j', k'')) (y j) := by
    rw [s (𝟙 j) f]
  _ =
      F.map ((𝟙 j', i f) : (j', kf f) ⟶ (j', k''))
        (F.map ((f, g j ≫ hf f) : (j, k j) ⟶ (j', kf f)) (y j)) := by
    rw [← FunctorToTypes.map_comp_apply, prod_comp, comp_id, assoc]
  _ =
      F.map ((𝟙 j', i f) : (j', kf f) ⟶ (j', k''))
        (F.map ((𝟙 j', g j' ≫ gf f) : (j', k j') ⟶ (j', kf f)) (y j')) := by
    rw [← wf f]
  _ = F.map ((𝟙 j', g j' ≫ gf f ≫ i f) : (j', k j') ⟶ (j', k'')) (y j') := by
    rw [← FunctorToTypes.map_comp_apply, prod_comp, id_comp, assoc]
  _ = F.map ((𝟙 j', g j' ≫ gf (𝟙 j') ≫ i (𝟙 j')) : (j', k j') ⟶ (j', k'')) (y j') := by
    rw [s f (𝟙 j'), ← s (𝟙 j') (𝟙 j')]

Result:
no goals