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 : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit (coconeOfCoconeUncurry 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 : Cocone (uncurry.obj F) → Cocone D.coconePoints :=
  fun s ↦
    { pt := s.pt,
      ι :=
        { app := fun j ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (uncurry.obj F)
p : J × K
h1 :
  (D.obj p.1).ι.app p.2 ≫
      (Q p.1).desc
        ((Cocone.precompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).inv).obj
          (Cocone.whisker (Prod.sectR p.1 K) s)) =
    s.ι.app (p.1, p.2)
h2 : (coconeOfCoconeUncurry Q c).ι.app p.1 ≫ P.desc (S s) = (S s).ι.app p.1
⊢ 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 ⊢

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 : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit (coconeOfCoconeUncurry 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 : Cocone (uncurry.obj F) → Cocone D.coconePoints :=
  fun s ↦
    { pt := s.pt,
      ι :=
        { app := fun j ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (uncurry.obj F)
p : J × K
h1 :
  (D.obj p.1).ι.app p.2 ≫
      (Q p.1).desc
        ((Cocone.precompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).inv).obj
          (Cocone.whisker (Prod.sectR p.1 K) s)) =
    s.ι.app (p.1, p.2)
h2 :
  (Q p.1).desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (p.1, k), naturality := ⋯ } } ≫
      P.desc
        { pt := s.pt,
          ι :=
            {
              app := fun j ↦
                (Q j).desc
                  ((Cocone.precompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj j).obj x)) ⋯).inv).obj
                    (Cocone.whisker (Prod.sectR j K) s)),
              naturality := ⋯ } } =
    (Q p.1).desc
      ((Cocone.precompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).inv).obj
        (Cocone.whisker (Prod.sectR p.1 K) s))
⊢ c.ι.app p ≫
      P.desc
        { pt := s.pt,
          ι :=
            {
              app := fun j ↦
                (Q j).desc
                  ((Cocone.precompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj j).obj x)) ⋯).inv).obj
                    (Cocone.whisker (Prod.sectR j K) s)),
              naturality := ⋯ } } =
    s.ι.app p