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

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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 G).obj j) k ≫
      colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitCurrySwapCompColimIsoColimitCurryCompColim G).inv =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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 G).obj j) k ≫
      colimit.ι (curry.obj G ⋙ colim) j ≫
        (colimitIsoColimitCurryCompColim G).inv ≫
          (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv ≫
            (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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
⊢ (𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
simp

Result:
no goals

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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
⊢ (G.map ((Prod.braiding K J).counitInv.app (j, k)) ≫
        (Iso.refl (Prod.swap K J ⋙ G)).hom.app ((Prod.braiding K J).inverse.obj (j, k)) ≫
          colimit.ι (Prod.swap K J ⋙ G) ((Prod.braiding K J).inverse.obj (j, k))) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
dsimp [Equivalence.counitInv]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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
⊢ (G.map (𝟙 j, 𝟙 k) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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 G).obj j) k ≫
      colimit.ι (curry.obj G ⋙ colim) j ≫
        (colimitIsoColimitCurryCompColim G).inv ≫
          (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv ≫
            (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
slice_lhs 1 3 => simp only []

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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 G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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 G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
rw [colimitIsoColimitCurryCompColim_ι_ι_inv, HasColimit.isoOfEquivalence_inv_π]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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
⊢ (G.map ((Prod.braiding K J).counitInv.app (j, k)) ≫
        (Iso.refl (Prod.swap K J ⋙ G)).hom.app ((Prod.braiding K J).inverse.obj (j, k)) ≫
          colimit.ι (Prod.swap K J ⋙ G) ((Prod.braiding K J).inverse.obj (j, k))) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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
⊢ (G.map (𝟙 j, 𝟙 k) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
rw [CategoryTheory.Bifunctor.map_id]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, 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
⊢ (𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k