awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
n : SimplexCategory
⊢ HasLimit (J :=
    WidePullbackShape
      (ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n))
    (WidePullbackShape.wideCospan (Functor.obj (incl C) T)
      (fun
          (x :
            ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) ↦
        U)
      fun
        (x :
          ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) ↦
      (isTerminalIncl T hT).from U)

Tactic:
⟨⟨_, WidePullbackCone.isLimitOfFan  _ (U.isLimitPowerFan _)
    (isTerminalIncl T hT)⟩⟩

Premises used: CategoryTheory.Limits.FormalCoproduct.isTerminalIncl, Nonempty.intro, CategoryTheory.Limits.FormalCoproduct.isLimitPowerFan, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.WidePullbackCone.isLimitOfFan
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
n : SimplexCategoryᵒᵖ
i :
  ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC := fun (X : SimplexCategory) ↦
    Fin (X.len + 1)) (Opposite.unop n)
⊢ Eq (α := Functor.obj U.cech n ⟶ U)
    (Iso.hom (U.cechIsoCechNerveApp hT n) ≫
      WidePullback.π
        (fun
            (x :
              ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
          (isTerminalIncl T hT).from U)
        i)
    (U.powerπ i)

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ _

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Limits.Fan.proj, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.FormalCoproduct.power, CategoryTheory.Limits.FormalCoproduct.powerπ
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
X Y : SimplexCategoryᵒᵖ
f : X ⟶ Y
⊢ ∀ (j : Fin ((Opposite.unop Y).len + 1)),
    Eq (α := Functor.obj U.cech X ⟶ (Arrow.mk ((isTerminalIncl T hT).from U)).left)
      (CategoryStruct.comp (Y :=
          widePullback (Arrow.mk ((isTerminalIncl T hT).from U)).right
            (fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).left)
            fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom)
          (Functor.map U.cech f ≫
            Iso.hom
              ((fun (x : SimplexCategoryᵒᵖ) ↦
                  (U.cechIsoCechNerveApp hT x :
                    Functor.obj U.cech x ≅ (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj x))
                Y))
          (WidePullback.π (fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom)
            j) :
        Functor.obj U.cech X ⟶ (Arrow.mk ((isTerminalIncl T hT).from U)).left)
      ((Iso.hom
              ((fun (x : SimplexCategoryᵒᵖ) ↦
                  (U.cechIsoCechNerveApp hT x :
                    Functor.obj U.cech x ≅ (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj x))
                X) ≫
            (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.map f) ≫
          WidePullback.π (fun (x : Fin ((Opposite.unop Y).len + 1)) ↦ (Arrow.mk ((isTerminalIncl T hT).from U)).hom) j :
        Functor.obj U.cech X ⟶ (Arrow.mk ((isTerminalIncl T hT).from U)).left)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
h :
  ∀ (n : SimplexCategoryᵒᵖ),
    NatTrans.app
        (Functor.map (𝟭 (SimplicialObject (FormalCoproduct.{w, u} C))) (Iso.hom (U.cechIsoCechNerve hT)) ≫
          (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve.hom)
        n =
      ((SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).hom ≫
            Functor.map (SimplicialObject.const (FormalCoproduct.{w, u} C))
              (Iso.hom (Iso.refl (SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).right))).app
        n
⊢ Functor.map (𝟭 (SimplicialObject (FormalCoproduct.{w, u} C))) (Iso.hom (U.cechIsoCechNerve hT)) ≫
      (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve.hom =
    (SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).hom ≫
      Functor.map (SimplicialObject.const (FormalCoproduct.{w, u} C))
        (Iso.hom (Iso.refl (SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).right))

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
n : SimplexCategoryᵒᵖ
⊢ NatTrans.app
      (Functor.map (𝟭 (SimplicialObject (FormalCoproduct.{w, u} C))) (Iso.hom (U.cechIsoCechNerve hT)) ≫
        (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve.hom)
      n =
    ((SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).hom ≫
          Functor.map (SimplicialObject.const (FormalCoproduct.{w, u} C))
            (Iso.hom (Iso.refl (SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).right))).app
      n

Tactic:
apply (isTerminalIncl _ hT).hom_ext

Premises used: CategoryTheory.Limits.FormalCoproduct.isTerminalIncl, CategoryTheory.Limits.IsTerminal.hom_ext
-- 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)
j : J
k k' : K
f : k ⟶ k'
⊢ Eq.{v_3 + 1} (α := obj.{v_2, v_3, u_2, u_3} (obj (const K) c.pt) k ⟶ (F.obj j).obj k')
    (Functor.map (obj (const K) c.pt) f ≫ c.π.app (j, k')) (c.π.app (j, k) ≫ (F.obj j).map f)

Tactic:
simpa using @NatTrans.naturality _ _ _ _ _ _ c.π (j, k) (j, k') (𝟙 j, f)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.CategoryStruct.id, Prod.mk, CategoryTheory.NatTrans.naturality
-- 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)
j j' : J
f : j ⟶ j'
k : K
⊢ Eq (α := obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j ⟶ (F.obj j').obj k)
    ((Functor.map (obj (const J) c.pt) f ≫
        (Q j').lift { pt := c.pt, π := { app := fun (k : K) ↦ c.π.app (j', k), naturality := ⋯ } }) ≫
      (D.obj j').π.app k)
    (((Q j).lift { pt := c.pt, π := { app := fun (k : K) ↦ c.π.app (j, k), naturality := ⋯ } } ≫ D.conePoints.map f) ≫
      (D.obj j').π.app k)

Tactic:
simpa using @NatTrans.naturality _ _ _ _ _ _ c.π (j, k) (j', k) (f, 𝟙 k)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.CategoryStruct.id, Prod.mk, CategoryTheory.NatTrans.naturality
-- 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 (obj curry G)
Q : (j : J) → IsLimit (D.obj j)
c : Cone G
x j' : J
x_1 : x ⟶ j'
⊢ ∀ (j : K),
    Eq (α := obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) x ⟶ ((obj curry G).obj j').obj j)
      ((Functor.map (obj (const J) c.pt) x_1 ≫
          (Q j').lift { pt := c.pt, π := { app := fun (k : K) ↦ c.π.app (j', k), naturality := ⋯ } }) ≫
        (D.obj j').π.app j)
      (((Q x).lift { pt := c.pt, π := { app := fun (k : K) ↦ c.π.app (x, k), naturality := ⋯ } } ≫
          D.conePoints.map x_1) ≫
        (D.obj j').π.app j)

Tactic:
simp
-- 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)
j : J
k k' : K
f : k ⟶ k'
dsimp : Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.obj j).map f ≫ c.ι.app (j, k')) (c.ι.app (j, k) ≫ 𝟙 c.pt)
⊢ Eq (α := (F.obj j).obj k ⟶ obj.{v_2, v_3, u_2, u_3} (obj (const K) c.pt) k') ((F.obj j).map f ≫ c.ι.app (j, k'))
    (c.ι.app (j, k) ≫ Functor.map (obj (const K) c.pt) f)

Tactic:
dsimp
-- 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)
j : J
k k' : K
f : k ⟶ k'
simp : Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.obj j).map f ≫ c.ι.app (j, k')) (c.ι.app (j, k))
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.obj j).map f ≫ c.ι.app (j, k')) (c.ι.app (j, k) ≫ 𝟙 c.pt)

Tactic:
simp only [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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)
j : J
k k' : K
f : k ⟶ k'
arg : (F.obj j).map f
| (F.obj j).map f ≫ c.ι.app (j, k')

Tactic:
arg 1
-- 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)
j : J
k k' : K
f : k ⟶ k'
⊢ (F.obj j).map f = (F.map (𝟙 j)).app k ≫ (F.obj j).map f

Tactic:
simp
-- 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)
j : J
k k' : K
f : k ⟶ k'
arg arg₁ : (F.obj j).map f
| (F.obj j).map f ≫ c.ι.app (j, k')

Tactic:
arg 1; equals (F.map (𝟙 _)).app _ ≫ (F.obj j).map f =>
                      simp

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- 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)
j : J
k k' : K
f : k ⟶ k'
conv_lhs : Eq (α := (F.obj j).obj k ⟶ c.pt) (((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k')) (c.ι.app (j, k))
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.obj j).map f ≫ c.ι.app (j, k')) (c.ι.app (j, k))

Tactic:
conv_lhs =>
                    arg 1; equals (F.map (𝟙 _)).app _ ≫ (F.obj j).map f =>
                      simp

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- 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)
j : J
k k' : K
f : k ⟶ k'
arg : (F.map (𝟙 j)).app k ≫ (F.obj j).map f
| ((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k')

Tactic:
arg 1
-- 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)
j : J
k k' : K
f : k ⟶ k'
rw : (obj uncurry F).map (𝟙 j ×ₘ f)
| (F.map (𝟙 j)).app k ≫ (F.obj j).map f

Tactic:
rw [← uncurry_obj_map F (𝟙 j ×ₘ f)]

Premises used: CategoryTheory.Prod.mkHom, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.uncurry_obj_map
-- 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)
j : J
k k' : K
f : k ⟶ k'
arg : (obj uncurry F).map (𝟙 j ×ₘ f)
| ((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k')

Tactic:
arg 1; rw [← uncurry_obj_map F (𝟙 j ×ₘ f)]

Premises used: CategoryTheory.Prod.mkHom, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.uncurry_obj_map
-- 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)
j : J
k k' : K
f : k ⟶ k'
conv_lhs : (obj uncurry F).map (𝟙 j ×ₘ f) ≫ c.ι.app (j, k') = c.ι.app (j, k)
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) (((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k')) (c.ι.app (j, k))

Tactic:
conv_lhs => arg 1; rw [← uncurry_obj_map F (𝟙 j ×ₘ f)]

Premises used: CategoryTheory.Prod.mkHom, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.uncurry_obj_map
-- 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)
j : J
k k' : K
f : k ⟶ k'
rw rw₁ :
  Eq (α := (F.obj j).obj k ⟶ c.pt) (c.ι.app (j, k) : (obj uncurry F).obj (j, k) ⟶ obj (obj (const (J × K)) c.pt) (j, k))
    (c.ι.app (j, k))
⊢ (obj uncurry F).map (𝟙 j ×ₘ f) ≫ c.ι.app (j, k') = c.ι.app (j, k)

Tactic:
rw [c.w]

Premises used: CategoryTheory.Limits.Cocone.w
-- 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)
j j' : J
f : j ⟶ j'
dsimp :
  ∀ (j_1 : K),
    Eq (α := (F.obj j).obj j_1 ⟶ c.pt)
      ((D.obj j).ι.app j_1 ≫
          (D.map f).hom ≫ (Q j').desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j', k), naturality := ⋯ } } :
        (F.obj j).obj j_1 ⟶ c.pt)
      ((D.obj j).ι.app j_1 ≫
          CategoryStruct.comp (Y := c.pt)
            ((Q j).desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } } :
              (D.obj j).pt ⟶
                Cocone.pt.{v_2, v_3, u_2, u_3} (J := K) (F := F.obj j)
                  { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } })
            (𝟙 c.pt) :
        (F.obj j).obj j_1 ⟶ c.pt)
⊢ ∀ (j_1 : K),
    Eq (α := (F.obj j).obj j_1 ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j')
      ((D.obj j).ι.app j_1 ≫
          D.coconePoints.map f ≫
            (Q j').desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j', k), naturality := ⋯ } } :
        (F.obj j).obj j_1 ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j')
      ((D.obj j).ι.app j_1 ≫
          CategoryStruct.comp (Y := obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j)
            ((Q j).desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } } :
              (D.obj j).pt ⟶
                Cocone.pt.{v_2, v_3, u_2, u_3} (J := K) (F := F.obj j)
                  { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } })
            (Functor.map (obj (const J) c.pt) f) :
        (F.obj j).obj j_1 ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j')

Tactic:
dsimp
-- 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)
j j' : J
f : j ⟶ j'
k : K
simp : Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.map f).app k ≫ c.ι.app (j', k)) (c.ι.app (j, k))
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt)
    ((D.obj j).ι.app k ≫
        (D.map f).hom ≫ (Q j').desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j', k), naturality := ⋯ } } :
      (F.obj j).obj k ⟶ c.pt)
    ((D.obj j).ι.app k ≫
        CategoryStruct.comp (Y := c.pt)
          ((Q j).desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } } :
            (D.obj j).pt ⟶
              Cocone.pt.{v_2, v_3, u_2, u_3} (J := K) (F := F.obj j)
                { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } })
          (𝟙 c.pt) :
      (F.obj j).obj k ⟶ c.pt)

Tactic:
simp only [Limits.CoconeMorphism.w_assoc, Limits.Cocone.precompose_obj_ι,
              Limits.IsColimit.fac, NatTrans.comp_app, Category.comp_id,
              Category.assoc]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Limits.CoconeMorphism.w_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cocone.precompose_obj_ι, CategoryTheory.NatTrans.comp_app
-- 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)
j j' : J
f : j ⟶ j'
k : K
⊢ Eq (α := (obj uncurry F).obj (j, k) ⟶ obj (obj (const (J × K)) c.pt) (j', k))
    ((obj uncurry F).map (f, 𝟙 k) ≫ c.ι.app (j', k)) (c.ι.app (j, k) ≫ Functor.map (obj (const (J × K)) c.pt) (f, 𝟙 k))

Tactic:
have := @NatTrans.naturality _ _ _ _ _ _ c.ι (j, k) (j', k) (f, 𝟙 k)
-- 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)
j j' : J
f : j ⟶ j'
k : K
this :
  Eq (α := (F.obj j).obj k ⟶ c.pt) (((F.map f).app k ≫ (F.obj j').map (𝟙 k)) ≫ c.ι.app (j', k))
    (c.ι.app (j, k) ≫ 𝟙 c.pt)
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.map f).app k ≫ c.ι.app (j', k)) (c.ι.app (j, k))

Tactic:
simp only [Category.comp_id, CategoryTheory.Functor.map_id] at this

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- 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)
j j' : J
f : j ⟶ j'
k : K
this : Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.map f).app k ≫ c.ι.app (j', k)) (c.ι.app (j, k))
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.map f).app k ≫ c.ι.app (j', k)) (c.ι.app (j, k))

Tactic:
this
-- 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)
j j' : J
f : j ⟶ j'
k : K
this : Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.map f).app k ≫ c.ι.app (j', k)) (c.ι.app (j, k))
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.map f).app k ≫ c.ι.app (j', k)) (c.ι.app (j, k))

Tactic:
exact this
-- 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 (obj curry G)
Q : (j : J) → IsColimit (D.obj j)
c : Cocone G
j x : J
x_1 : j ⟶ x
⊢ ∀ (j_1 : K),
    Eq (α := ((obj curry G).obj j).obj j_1 ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) x)
      ((D.obj j).ι.app j_1 ≫
          D.coconePoints.map x_1 ≫
            (Q x).desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (x, k), naturality := ⋯ } } :
        ((obj curry G).obj j).obj j_1 ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) x)
      ((D.obj j).ι.app j_1 ≫
          CategoryStruct.comp (Y := obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j)
            ((Q j).desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } } :
              (D.obj j).pt ⟶
                Cocone.pt.{v_2, v_3, u_2, u_3} (J := K) (F := (obj curry G).obj j)
                  { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } })
            (Functor.map (obj (const J) c.pt) x_1) :
        ((obj curry G).obj j).obj j_1 ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) x)

Tactic:
simp
-- 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 c
s : Cone D.conePoints
p p' : J × K
f : p ⟶ p'
dsimp :
  𝟙 s.pt ≫ s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
    (s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2) ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2
⊢ Functor.map (obj (const (J × K)) s.pt) f ≫ s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
    (s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2) ≫ (obj uncurry F).map f

Tactic:
dsimp
-- 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 c
s : Cone D.conePoints
p p' : J × K
f : p ⟶ p'
simp :
  s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
    s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2 ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2
⊢ 𝟙 s.pt ≫ s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
    (s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2) ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2

Tactic:
simp only [Category.id_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp