-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem colimitFlipCompColimIsoColimitCompColim_ι_ι_hom (j) (k) :
    colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫
      (colimitFlipCompColimIsoColimitCompColim F).hom =
        (colimit.ι _ k ≫ colimit.ι (F ⋙ colim) j : _ ⟶ colimit (F⋙ 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
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ (colimitFlipCompColimIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j

Tactic:
dsimp [colimitFlipCompColimIsoColimitCompColim]

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
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (F.flip.obj k) j ≫
      colimit.ι (F.flip ⋙ colim) k ≫
        (colimitUncurryIsoColimitCompColim F.flip).inv ≫
          (HasColimit.isoOfNatIso (uncurryObjFlip F)).hom ≫
            (HasColimit.isoOfEquivalence (Prod.braiding K J)
                  (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom ≫
              (colimitUncurryIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ 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
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ (((colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ (colimitUncurryIsoColimitCompColim F.flip).inv) ≫
          (HasColimit.isoOfNatIso (uncurryObjFlip F)).hom) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J)
            (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom) ≫
      (colimitUncurryIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j

Tactic:
simp [Equivalence.unit]

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
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (F.flip.obj k) j ≫
      colimit.ι (F.flip ⋙ colim) k ≫
        (colimitUncurryIsoColimitCompColim F.flip).inv ≫
          (HasColimit.isoOfNatIso (uncurryObjFlip F)).hom ≫
            (HasColimit.isoOfEquivalence (Prod.braiding K J)
                  (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom ≫
              (colimitUncurryIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ 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
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ (((colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ (colimitUncurryIsoColimitCompColim F.flip).inv) ≫
          (HasColimit.isoOfNatIso (uncurryObjFlip F)).hom) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J)
            (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom) ≫
      (colimitUncurryIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j