Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit (coneOfConeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cone (uncurry.obj F) → Cone D.conePoints :=
  fun s ↦
    { pt := s.pt,
      π :=
        { app := fun j ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (uncurry.obj F)
p : J × K
h1 :
  (Q p.1).lift
        ((Cone.postcompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).hom).obj
          (Cone.whisker (Prod.sectR p.1 K) s)) ≫
      (D.obj p.1).π.app p.2 =
    s.π.app (p.1, p.2)
h2 : P.lift (S s) ≫ (coneOfConeUncurry Q c).π.app p.1 = (S s).π.app p.1
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p

Tactic:
dsimp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj, NatTrans.id_app,
        Functor.const_obj_obj, DiagramOfCones.conePoints_obj, DiagramOfCones.conePoints_map,
        Functor.const_obj_map, id_eq, Cone.postcompose_obj_pt, Cone.whisker_pt,
        Cone.postcompose_obj_π, Cone.whisker_π, NatTrans.comp_app, whiskerLeft_app,
        NatIso.ofComponents_hom_app, Iso.refl_hom, Prod.sectL_obj, Prod.sectL_map, eq_mp_eq_cast,
        eq_mpr_eq_cast, coneOfConeUncurry_pt, coneOfConeUncurry_π_app, S, E] at h2 ⊢

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit (coneOfConeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cone (uncurry.obj F) → Cone D.conePoints :=
  fun s ↦
    { pt := s.pt,
      π :=
        { app := fun j ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (uncurry.obj F)
p : J × K
h1 :
  (Q p.1).lift
        ((Cone.postcompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).hom).obj
          (Cone.whisker (Prod.sectR p.1 K) s)) ≫
      (D.obj p.1).π.app p.2 =
    s.π.app (p.1, p.2)
h2 :
  P.lift
        { pt := s.pt,
          π :=
            {
              app := fun j ↦
                (Q j).lift
                  ((Cone.postcompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj j).obj x)) ⋯).hom).obj
                    (Cone.whisker (Prod.sectR j K) s)),
              naturality := ⋯ } } ≫
      (Q p.1).lift { pt := c.pt, π := { app := fun k ↦ c.π.app (p.1, k), naturality := ⋯ } } =
    (Q p.1).lift
      ((Cone.postcompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).hom).obj
        (Cone.whisker (Prod.sectR p.1 K) s))
⊢ P.lift
        { pt := s.pt,
          π :=
            {
              app := fun j ↦
                (Q j).lift
                  ((Cone.postcompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj j).obj x)) ⋯).hom).obj
                    (Cone.whisker (Prod.sectR j K) s)),
              naturality := ⋯ } } ≫
      c.π.app p =
    s.π.app p