Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: 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),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (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
pf✝⁵ : HasColimit ((curry.obj F).obj j)
pf✝⁴ : HasLimit ((curry.obj (swap K J ⋙ F)).obj k'')
pf✝³ : HasLimit ((curry.obj (swap K J ⋙ F)).obj k'')
pf✝² : HasColimit ((curry.obj F).obj j)
h :
  ∀ (j j' : J) (f : j ⟶ j'),
    (ConcreteCategory.hom (((curry.obj (swap K J ⋙ F)).obj k'').map f))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j) ≫ F.map (𝟙 j ×ₘ gf (𝟙 j)) ≫ F.map (𝟙 j ×ₘ i (𝟙 j)))) (y j)) =
      (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j') ≫ F.map (𝟙 j' ×ₘ gf (𝟙 j')) ≫ F.map (𝟙 j' ×ₘ i (𝟙 j')))) (y j')
pf✝¹ : HasColimitsOfShape K (Type v)
pf✝ : HasLimit (curry.obj F ⋙ colim)
⊢ ∃ k_1 f g_1,
    (ConcreteCategory.hom (((curry.obj F).obj j).map f))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ i (𝟙 j))))
          ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ gf (𝟙 j)))) ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j))) (y j)))) =
      (ConcreteCategory.hom (((curry.obj F).obj j).map g_1)) (y j)

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

Goal state after:
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),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (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
pf✝⁵ : HasColimit ((curry.obj F).obj j)
pf✝⁴ : HasLimit ((curry.obj (swap K J ⋙ F)).obj k'')
pf✝³ : HasLimit ((curry.obj (swap K J ⋙ F)).obj k'')
pf✝² : HasColimit ((curry.obj F).obj j)
h :
  ∀ (j j' : J) (f : j ⟶ j'),
    (ConcreteCategory.hom (((curry.obj (swap K J ⋙ F)).obj k'').map f))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j) ≫ F.map (𝟙 j ×ₘ gf (𝟙 j)) ≫ F.map (𝟙 j ×ₘ i (𝟙 j)))) (y j)) =
      (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j') ≫ F.map (𝟙 j' ×ₘ gf (𝟙 j')) ≫ F.map (𝟙 j' ×ₘ i (𝟙 j')))) (y j')
pf✝¹ : HasColimitsOfShape K (Type v)
pf✝ : HasLimit (curry.obj F ⋙ colim)
⊢ (ConcreteCategory.hom (((curry.obj F).obj j).map (𝟙 k'')))
      ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ i (𝟙 j))))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ gf (𝟙 j)))) ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j))) (y j)))) =
    (ConcreteCategory.hom (((curry.obj F).obj j).map (g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)