-- 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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (obj uncurry F)
P : IsLimit (coneOfConeUncurry 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 : Cone (obj uncurry F)) → Cone D.conePoints :=
  fun (s : Cone (obj uncurry F)) ↦
    { pt := s.pt,
      π :=
        { app := fun (j : J) ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (obj uncurry F)
p : J × K
h1 :
  Eq (α := s.pt ⟶ (F.obj p.1).obj p.2)
    (CategoryStruct.comp (Y := Cone.pt (F := F.obj p.1) (D.obj p.1))
        (lift (Q p.1)
          (obj (C := Cone (Prod.sectR p.1 K ⋙ obj uncurry F))
            (Cone.postcompose (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) ⋯)))
            (Cone.whisker (Prod.sectR p.1 K) s)))
        (NatTrans.app (Cone.π (D.obj p.1)) p.2) :
      s.pt ⟶ (F.obj p.1).obj p.2)
    (s.π.app (p.1, p.2) : obj (obj (const (J × K)) s.pt) (p.1, p.2) ⟶ (obj uncurry F).obj (p.1, p.2))
h2 :
  Eq (α := s.pt ⟶ Cone.pt (F := F.obj p.1) (D.obj p.1))
    (CategoryStruct.comp (Y := c.pt)
        (P.lift
            { pt := s.pt,
              π :=
                {
                  app := fun (j : J) ↦
                    (Q j).lift
                      (obj (C := Cone (Prod.sectR j K ⋙ obj uncurry F))
                        (Cone.postcompose (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj j).obj x)) ⋯)))
                        (Cone.whisker (Prod.sectR j K) s)),
                  naturality := ⋯ } } :
          Cone.pt.{v_1, v_3, u_1, u_3} (J := J) (F := D.conePoints)
              { pt := s.pt,
                π :=
                  {
                    app := fun (j : J) ↦
                      (Q j).lift
                        (obj (C := Cone (Prod.sectR j K ⋙ obj uncurry F))
                          (Cone.postcompose
                            (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj j).obj x)) ⋯)))
                          (Cone.whisker (Prod.sectR j K) s)),
                    naturality := ⋯ : NatTrans (obj (const J) s.pt) D.conePoints } :
                Cone D.conePoints } ⟶
            (coneOfConeUncurry Q c).pt)
        (lift (Q p.1) { pt := c.pt, π := { app := fun (k : K) ↦ c.π.app (p.1, k), naturality := ⋯ } } :
          Cone.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 := ⋯ :
                    NatTrans (obj (const K) c.pt) (F.obj p.1) } :
                Cone (F.obj p.1) } ⟶
            Cone.pt (F := F.obj p.1) (D.obj p.1)) :
      s.pt ⟶ Cone.pt (F := F.obj p.1) (D.obj p.1))
    (lift (Q p.1)
        (obj (C := Cone (Prod.sectR p.1 K ⋙ obj uncurry F))
          (Cone.postcompose (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) ⋯)))
          (Cone.whisker (Prod.sectR p.1 K) s)) :
      Cone.pt (F := F.obj p.1)
          (obj (C := Cone (Prod.sectR p.1 K ⋙ obj uncurry F))
            (Cone.postcompose (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) ⋯)))
            (Cone.whisker (Prod.sectR p.1 K) s)) ⟶
        Cone.pt (F := F.obj p.1) (D.obj p.1))
⊢ P.lift
        { pt := s.pt,
          π :=
            {
              app := fun (j : J) ↦
                (Q j).lift
                  (obj (C := Cone (Prod.sectR j K ⋙ obj uncurry F))
                    (Cone.postcompose (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj j).obj x)) ⋯)))
                    (Cone.whisker (Prod.sectR j K) s)),
              naturality := ⋯ } } ≫
      c.π.app p =
    s.π.app p

Tactic:
simp [← h1, ← h2]