-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom {j} {k} :
    colimit.ι _ j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
      (colimitCurrySwapCompColimIsoColimitCurryCompColim G).hom =
        (colimit.ι _ k ≫ colimit.ι (curry.obj G ⋙ colim) j : _ ⟶ colimit (curry.obj G⋙ colim))

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ ((colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
          colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
            (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
      (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Tactic:
simp

Result:
no goals

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
      colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫ (colimitCurrySwapCompColimIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Tactic:
dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
      colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
        ((colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv ≫
            (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
          (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
      colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
        ((colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv ≫
            (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
          (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Tactic:
slice_lhs 1 3 => simp only []

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ ((colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
          colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
            (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
      (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j