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

Tactic:
dsimp [colimitFlipCompColimIsoColimitCompColim]

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

Tactic:
simp [Equivalence.counitInv]

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