-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit (coconeOfCoconeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ obj uncurry F ≅ F.obj j :=
  fun (j : J) ↦ NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((Prod.sectR j K ⋙ obj uncurry F).obj x)) ⋯
S : (s : Cocone (obj uncurry F)) → Cocone D.coconePoints :=
  fun (s : Cocone (obj uncurry F)) ↦
    { pt := s.pt,
      ι :=
        { app := fun (j : J) ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (obj uncurry F)
p : J × K
h1 :
  Eq (α := (F.obj p.1).obj p.2 ⟶ s.pt)
    (CategoryStruct.comp (Y := Cocone.pt (F := F.obj p.1) (D.obj p.1)) (NatTrans.app (Cocone.ι (D.obj p.1)) p.2)
        (desc (Q p.1)
          (obj (C := Cocone (Prod.sectR p.1 K ⋙ obj uncurry F))
            (Cocone.precompose (Iso.inv (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) ⋯)))
            (Cocone.whisker (Prod.sectR p.1 K) s))) :
      (F.obj p.1).obj p.2 ⟶ s.pt)
    (s.ι.app (p.1, p.2) : (obj uncurry F).obj (p.1, p.2) ⟶ obj (obj (const (J × K)) s.pt) (p.1, p.2))
h2 :
  Eq (α := D.coconePoints.obj p.1 ⟶ (S s).pt) ((coconeOfCoconeUncurry Q c).ι.app p.1 ≫ P.desc (S s)) ((S s).ι.app p.1)
dsimp :
  c.ι.app p ≫
      P.desc
        { pt := s.pt,
          ι :=
            {
              app := fun (j : J) ↦
                (Q j).desc
                  (obj (C := Cocone (Prod.sectR j K ⋙ obj uncurry F))
                    (Cocone.precompose (Iso.inv (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj j).obj x)) ⋯)))
                    (Cocone.whisker (Prod.sectR j K) s)),
              naturality := ⋯ } } =
    s.ι.app p
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p

Tactic:
dsimp only [DiagramOfCocones.coconePoints_obj, Functor.comp_obj, Prod.sectR_obj,
        uncurry_obj_obj, NatTrans.id_app, Functor.const_obj_obj, DiagramOfCocones.coconePoints_map,
        Functor.const_obj_map, id_eq, Cocone.precompose_obj_pt, Cocone.whisker_pt,
        Cocone.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app, NatIso.ofComponents_inv_app,
        Iso.refl_inv, whiskerLeft_app, Prod.sectL_obj, Prod.sectL_map, eq_mp_eq_cast,
        eq_mpr_eq_cast, coconeOfCoconeUncurry_pt, coconeOfCoconeUncurry_ι_app, S, E] at h2 ⊢

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.Cocone.whisker_pt, CategoryTheory.Prod.sectL_obj, CategoryTheory.Limits.Cocone.whisker_ι, CategoryTheory.NatIso.ofComponents_inv_app, eq_mp_eq_cast, CategoryTheory.Limits.DiagramOfCocones.coconePoints_map, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.uncurry_obj_obj, CategoryTheory.Limits.Cocone.precompose_obj_ι, CategoryTheory.Iso.refl_inv, CategoryTheory.Prod.sectR_obj, CategoryTheory.Prod.sectL_map, CategoryTheory.NatTrans.id_app, CategoryTheory.Limits.DiagramOfCocones.coconePoints_obj, CategoryTheory.Limits.coconeOfCoconeUncurry_pt, CategoryTheory.Limits.coconeOfCoconeUncurry_ι_app, eq_mpr_eq_cast, CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.const_obj_map, id_eq, CategoryTheory.Limits.Cocone.precompose_obj_pt