Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: 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'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      (ConcreteCategory.hom (((curry.obj F).obj j').map f_1)) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
        (ConcreteCategory.hom (((curry.obj F).obj j').map g_1)) ((ConcreteCategory.hom (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
j j' : J
f : j ⟶ j'
q :
  (ConcreteCategory.hom (((curry.obj F).obj j').map (gf f))) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
    (ConcreteCategory.hom (((curry.obj F).obj j').map (hf f))) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
⊢ (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)

Tactic:
convert! q using 1

Goal state after:
case e'_2
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'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      (ConcreteCategory.hom (((curry.obj F).obj j').map f_1)) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
        (ConcreteCategory.hom (((curry.obj F).obj j').map g_1)) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
kf : {j j' : J} → (j ⟶ j') → K := ⋯
gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := ⋯
hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := ⋯
j j' : J
f : j ⟶ j'
q :
  (ConcreteCategory.hom (((curry.obj F).obj j').map (gf f))) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
    (ConcreteCategory.hom (((curry.obj F).obj j').map (hf f))) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
e_1✝ : (fun X ↦ X) (F.obj (j', kf f)) = (fun X ↦ X) (((curry.obj F).obj j').obj (kf f))
⊢ (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') =
    (ConcreteCategory.hom (((curry.obj F).obj j').map (gf f))) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j'))

case e'_3
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'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      (ConcreteCategory.hom (((curry.obj F).obj j').map f_1)) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
        (ConcreteCategory.hom (((curry.obj F).obj j').map g_1)) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
kf : {j j' : J} → (j ⟶ j') → K := ⋯
gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := ⋯
hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := ⋯
j j' : J
f : j ⟶ j'
q :
  (ConcreteCategory.hom (((curry.obj F).obj j').map (gf f))) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
    (ConcreteCategory.hom (((curry.obj F).obj j').map (hf f))) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
e_1✝ : (fun X ↦ X) (F.obj (j', kf f)) = (fun X ↦ X) (((curry.obj F).obj j').obj (kf f))
⊢ (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j) =
    (ConcreteCategory.hom (((curry.obj F).obj j').map (hf f))) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))