-- 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 (α := Cocone.pt (F := F.obj p.1) (D.obj p.1) ⟶ s.pt)
    (CategoryStruct.comp (Y := c.pt)
        (desc (Q p.1) { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (p.1, k), naturality := ⋯ } } :
          Cocone.pt (F := F.obj p.1) (D.obj p.1) ⟶
            Cocone.pt.{v_2, v_3, u_2, u_3} (J := K) (F := F.obj p.1)
              { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (p.1, k), naturality := ⋯ } })
        (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 := ⋯ } }) :
      Cocone.pt (F := F.obj p.1) (D.obj p.1) ⟶ s.pt)
    (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)) :
      Cocone.pt (F := F.obj p.1) (D.obj p.1) ⟶
        Cocone.pt (F := F.obj 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)))
⊢ 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

Tactic:
simp [← h1, ← h2]