awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
Q : DiagramOfCocones (obj curry G) := DiagramOfCocones.mkOfHasColimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := G.obj (y.1, x.2) ⟶ colimit ((obj curry G).obj y.1))
    (G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((obj curry G).obj y.1) y.2) (colimit.ι ((obj curry G).obj y.1) x.2)
rw :
  Eq (α := G.obj x ⟶ colimit (obj curry G ⋙ colim))
    (((obj curry G).map (f₁, f₂).1).app x.2 ≫
      ((obj curry G).obj y.1).map (f₁, f₂).2 ≫
        colimit.ι ((obj curry G).obj y.1) y.2 ≫ colimit.ι (obj curry G ⋙ colim) y.1)
    (colimit.ι ((obj curry G).obj x.1) x.2 ≫ (obj curry G ⋙ colim).map f₁ ≫ colimit.ι (obj curry G ⋙ colim) y.1)
⊢ G.map (f₁, f₂) ≫ colimit.ι ((obj curry G).obj y.1) y.2 ≫ colimit.ι (obj curry G ⋙ colim) y.1 =
    (colimit.ι ((obj curry G).obj x.1) x.2 ≫ colimit.ι (obj curry G ⋙ colim) x.1) ≫ 𝟙 (colimit (obj curry G ⋙ colim))

Tactic:
rw [← colimit.w (F := curry.obj G ⋙ colim) (f := f₁),
          Category.assoc, Category.comp_id, Prod.fac' (f₁, f₂),
          G.map_comp_assoc, ← curry_obj_map_app, ← curry_obj_obj_map]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colim, CategoryTheory.Functor.comp, Prod.mk, CategoryTheory.Functor.curry, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.curry_obj_obj_map, CategoryTheory.Prod.fac', CategoryTheory.Functor.curry_obj_map_app, CategoryTheory.Limits.colimit.w, CategoryTheory.Functor.obj
-- 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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
Q : DiagramOfCocones (obj curry G) := DiagramOfCocones.mkOfHasColimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := G.obj (y.1, x.2) ⟶ colimit ((obj curry G).obj y.1))
    (G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((obj curry G).obj y.1) y.2) (colimit.ι ((obj curry G).obj y.1) x.2)
dsimp :
  Eq (α := G.obj x ⟶ colimit (obj curry G ⋙ colim))
    (G.map (Prod.mkHom f₁ (𝟙 x.2)) ≫
      G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((obj curry G).obj y.1) y.2 ≫ colimit.ι (obj curry G ⋙ colim) y.1)
    (CategoryStruct.comp (Y := colimit ((obj curry G).obj x.1)) (colimit.ι ((obj curry G).obj x.1) x.2)
      (colimMap ((obj curry G).map f₁) ≫ colimit.ι (obj curry G ⋙ colim) y.1))
⊢ Eq (α := G.obj x ⟶ colimit (obj curry G ⋙ colim))
    (((obj curry G).map (f₁, f₂).1).app x.2 ≫
      ((obj curry G).obj y.1).map (f₁, f₂).2 ≫
        colimit.ι ((obj curry G).obj y.1) y.2 ≫ colimit.ι (obj curry G ⋙ colim) y.1)
    (colimit.ι ((obj curry G).obj x.1) x.2 ≫ (obj curry G ⋙ colim).map f₁ ≫ colimit.ι (obj curry G ⋙ colim) y.1)

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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
Q : DiagramOfCocones (obj curry G) := DiagramOfCocones.mkOfHasColimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := G.obj (y.1, x.2) ⟶ colimit ((obj curry G).obj y.1))
    (G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((obj curry G).obj y.1) y.2) (colimit.ι ((obj curry G).obj y.1) x.2)
⊢ Eq (α := G.obj x ⟶ colimit (obj curry G ⋙ colim))
    (G.map (Prod.mkHom f₁ (𝟙 x.2)) ≫
      G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((obj curry G).obj y.1) y.2 ≫ colimit.ι (obj curry G ⋙ colim) y.1)
    (CategoryStruct.comp (Y := colimit ((obj curry G).obj x.1)) (colimit.ι ((obj curry G).obj x.1) x.2)
      (colimMap ((obj curry G).map f₁) ≫ colimit.ι (obj curry G ⋙ colim) y.1))

Tactic:
simp [ι_colimMap_assoc, curry_obj_map_app, reassoc_of% this]

Premises used: CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Functor.curry_obj_map_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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
Q : DiagramOfCocones (obj curry G) := DiagramOfCocones.mkOfHasColimits (obj curry G)
Q' : (j : J) → IsColimit (Q.obj j) := fun (j : J) ↦ colimit.isColimit ((obj curry G).obj j)
c' : Cocone G
f : J × K
⊢ (coconeOfHasColimitCurryCompColim G).ι.app f ≫ colimit.desc (obj curry G ⋙ colim) (coconeOfCoconeCurry G Q' c') =
    c'.ι.app f

Tactic:
simp [coconeOfHasColimitCurryCompColim, Q, Q']

Premises used: CategoryTheory.Limits.coconeOfHasColimitCurryCompColim
-- 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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
Q : DiagramOfCocones (obj curry G) := DiagramOfCocones.mkOfHasColimits (obj curry G)
Q' : (j : J) → IsColimit (Q.obj j) := fun (j : J) ↦ colimit.isColimit ((obj curry G).obj j)
c' : Cocone G
f : (coconeOfHasColimitCurryCompColim G).pt ⟶ c'.pt
h : ∀ (j : J × K), (coconeOfHasColimitCurryCompColim G).ι.app j ≫ f = c'.ι.app j
dsimp : f = colimit.desc (obj curry G ⋙ colim) (coconeOfCoconeCurry G Q' c')
⊢ f = colimit.desc (obj curry G ⋙ colim) (coconeOfCoconeCurry G Q' c')

Tactic:
dsimp [coconeOfHasColimitCurryCompColim] at f h ⊢

Premises used: CategoryTheory.Limits.coconeOfHasColimitCurryCompColim
-- 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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
Q : DiagramOfCocones (obj curry G) := DiagramOfCocones.mkOfHasColimits (obj curry G)
Q' : (j : J) → IsColimit (Q.obj j) := fun (j : J) ↦ colimit.isColimit ((obj curry G).obj j)
c' : Cocone G
f : colimit (obj curry G ⋙ colim) ⟶ c'.pt
h : ∀ (j : J × K), (colimit.ι ((obj curry G).obj j.1) j.2 ≫ colimit.ι (obj curry G ⋙ colim) j.1) ≫ f = c'.ι.app j
⊢ f = colimit.desc (obj curry G ⋙ colim) (coconeOfCoconeCurry G Q' c')

Tactic:
colimit.hom_ext (F := curry.obj G ⋙ colim) (fun j ↦ colimit.hom_ext (fun k ↦ ?_))

Premises used: CategoryTheory.Limits.colimit.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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
Q : DiagramOfCocones (obj curry G) := DiagramOfCocones.mkOfHasColimits (obj curry G)
Q' : (j : J) → IsColimit (Q.obj j) := fun (j : J) ↦ colimit.isColimit ((obj curry G).obj j)
c' : Cocone G
f : colimit (obj curry G ⋙ colim) ⟶ c'.pt
h : ∀ (j : J × K), (colimit.ι ((obj curry G).obj j.1) j.2 ≫ colimit.ι (obj curry G ⋙ colim) j.1) ≫ f = c'.ι.app j
refine :
  ∀ (j : J) (k : K),
    colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j ≫ f =
      CategoryStruct.comp (Y := colimit ((obj curry G).obj j)) (colimit.ι ((obj curry G).obj j) k)
        (CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim)) (colimit.ι (obj curry G ⋙ colim) j)
          (colimit.desc (obj curry G ⋙ colim) (coconeOfCoconeCurry G Q' c')))
⊢ f = colimit.desc (obj curry G ⋙ colim) (coconeOfCoconeCurry G Q' c')

Tactic:
refine colimit.hom_ext (F := curry.obj G ⋙ colim) (fun j ↦ colimit.hom_ext (fun k ↦ ?_))

Premises used: CategoryTheory.Limits.colimit.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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
Q : DiagramOfCocones (obj curry G) := DiagramOfCocones.mkOfHasColimits (obj curry G)
Q' : (j : J) → IsColimit (Q.obj j) := fun (j : J) ↦ colimit.isColimit ((obj curry G).obj j)
c' : Cocone G
f : colimit (obj curry G ⋙ colim) ⟶ c'.pt
h : ∀ (j : J × K), (colimit.ι ((obj curry G).obj j.1) j.2 ≫ colimit.ι (obj curry G ⋙ colim) j.1) ≫ f = c'.ι.app j
j : J
k : K
⊢ colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j ≫ f =
    CategoryStruct.comp (Y := colimit ((obj curry G).obj j)) (colimit.ι ((obj curry G).obj j) k)
      (CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim)) (colimit.ι (obj curry G ⋙ colim) j)
        (colimit.desc (obj curry G ⋙ colim) (coconeOfCoconeCurry G Q' c')))

Tactic:
simp [← h ⟨j, k⟩, Q']

Premises used: Prod.mk
-- 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_1 : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj uncurry F)
inst_5 : HasColimit (F ⋙ colim)
c : Cocone (obj uncurry F) := colimit.cocone (obj uncurry F)
P : IsColimit c := colimit.isColimit (obj uncurry F)
G : DiagramOfCocones F := DiagramOfCocones.mkOfHasColimits F
Q : (j : J) → IsColimit (G.obj j) := fun (j : J) ↦ colimit.isColimit (F.obj j)
have : (Q' : IsColimit (coconeOfCoconeUncurry Q c)) → colimit (obj uncurry F) ≅ colimit (F ⋙ colim)
⊢ colimit (obj uncurry F) ≅ colimit (F ⋙ colim)

Tactic:
have Q' := coconeOfCoconeUncurryIsColimit Q P
-- 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_1 : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj uncurry F)
inst_5 : HasColimit (F ⋙ colim)
c : Cocone (obj uncurry F) := colimit.cocone (obj uncurry F)
P : IsColimit c := colimit.isColimit (obj uncurry F)
G : DiagramOfCocones F := DiagramOfCocones.mkOfHasColimits F
Q : (j : J) → IsColimit (G.obj j) := fun (j : J) ↦ colimit.isColimit (F.obj j)
Q' : IsColimit (coconeOfCoconeUncurry Q c)
have : (Q'' : IsColimit (colimit.cocone (F ⋙ colim))) → colimit (obj uncurry F) ≅ colimit (F ⋙ colim)
⊢ colimit (obj uncurry F) ≅ colimit (F ⋙ colim)

Tactic:
have Q'' := colimit.isColimit (F ⋙ colim)
-- 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_1 : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj uncurry F)
inst_5 : HasColimit (F ⋙ colim)
c : Cocone (obj uncurry F) := colimit.cocone (obj uncurry F)
P : IsColimit c := colimit.isColimit (obj uncurry F)
G : DiagramOfCocones F := DiagramOfCocones.mkOfHasColimits F
Q : (j : J) → IsColimit (G.obj j) := fun (j : J) ↦ colimit.isColimit (F.obj j)
Q' : IsColimit (coconeOfCoconeUncurry Q c)
Q'' : IsColimit (colimit.cocone (F ⋙ colim))
⊢ colimit (obj uncurry F) ≅ colimit (F ⋙ colim)

Tactic:
exact IsColimit.coconePointUniqueUpToIso Q' Q''

Premises used: CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- 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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj uncurry F)
inst_5 : HasColimit (F ⋙ colim)
j : J
k : K
dsimp :
  Eq (α := (F.obj j).obj k ⟶ colimit (obj uncurry F))
    (CategoryStruct.comp (Y := colimit (F.obj j)) (colimit.ι (F.obj j) k)
        (CategoryStruct.comp (Y := colimit (F ⋙ colim)) (colimit.ι (F ⋙ colim) j)
          (colimit.desc (F ⋙ colim)
            (coconeOfCoconeUncurry (fun (j : J) ↦ colimit.isColimit (F.obj j)) (colimit.cocone (obj uncurry F))))) :
      (F.obj j).obj k ⟶ colimit (obj uncurry F))
    (colimit.ι (obj uncurry F) (j, k) : (obj uncurry F).obj (j, k) ⟶ colimit (obj uncurry F))
⊢ Eq (α := (F.obj j).obj k ⟶ colimit (obj uncurry F))
    (colimit.ι (F.obj j) k ≫
      CategoryStruct.comp (Y := colimit (F ⋙ colim)) (colimit.ι (F ⋙ colim) j)
        (Iso.inv (colimitUncurryIsoColimitCompColim F)))
    (colimit.ι (obj uncurry F) (j, k))

Tactic:
dsimp [colimitUncurryIsoColimitCompColim, IsColimit.coconePointUniqueUpToIso,
    IsColimit.uniqueUpToIso]

Premises used: CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Limits.colimitUncurryIsoColimitCompColim, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- 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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj uncurry F)
inst_5 : HasColimit (F ⋙ colim)
j : J
k : K
⊢ Eq (α := (F.obj j).obj k ⟶ colimit (obj uncurry F))
    (CategoryStruct.comp (Y := colimit (F.obj j)) (colimit.ι (F.obj j) k)
        (CategoryStruct.comp (Y := colimit (F ⋙ colim)) (colimit.ι (F ⋙ colim) j)
          (colimit.desc (F ⋙ colim)
            (coconeOfCoconeUncurry (fun (j : J) ↦ colimit.isColimit (F.obj j)) (colimit.cocone (obj uncurry F))))) :
      (F.obj j).obj k ⟶ colimit (obj uncurry F))
    (colimit.ι (obj uncurry F) (j, k) : (obj uncurry F).obj (j, k) ⟶ colimit (obj uncurry 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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj uncurry F)
inst_5 : HasColimit (F ⋙ colim)
j : J
k : K
rw :
  Eq (α := (obj uncurry F).obj (j, k) ⟶ colimit (obj uncurry F))
    (CategoryStruct.comp (Y := colimit (F ⋙ colim))
      (CategoryStruct.comp (Y := colimit (obj uncurry F)) (colimit.ι (obj uncurry F) (j, k))
        (Iso.hom (colimitUncurryIsoColimitCompColim F)))
      (Iso.inv (colimitUncurryIsoColimitCompColim F)))
    (CategoryStruct.comp (Y := colimit (F ⋙ colim)) (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j)
      (Iso.inv (colimitUncurryIsoColimitCompColim F)))
⊢ Eq (α := (obj uncurry F).obj (j, k) ⟶ colimit (F ⋙ colim))
    (CategoryStruct.comp (Y := colimit (obj uncurry F)) (colimit.ι (obj uncurry F) (j, k))
      (Iso.hom (colimitUncurryIsoColimitCompColim F)))
    (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j)

Tactic:
rw [← cancel_mono (colimitUncurryIsoColimitCompColim F).inv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.colimitUncurryIsoColimitCompColim, CategoryTheory.Iso.inv
-- 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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj uncurry F)
inst_5 : HasColimit (F ⋙ colim)
j : J
k : K
⊢ Eq (α := (obj uncurry F).obj (j, k) ⟶ colimit (obj uncurry F))
    (CategoryStruct.comp (Y := colimit (F ⋙ colim))
      (CategoryStruct.comp (Y := colimit (obj uncurry F)) (colimit.ι (obj uncurry F) (j, k))
        (Iso.hom (colimitUncurryIsoColimitCompColim F)))
      (Iso.inv (colimitUncurryIsoColimitCompColim F)))
    (CategoryStruct.comp (Y := colimit (F ⋙ colim)) (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j)
      (Iso.inv (colimitUncurryIsoColimitCompColim 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
inst_3 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
x : K × J
⊢ (Equivalence.functor (Prod.braiding K J) ⋙ obj uncurry F).obj x ≅
    (Equivalence.functor (Prod.braiding K J) ⋙ obj uncurry F).obj x

Tactic:
rfl
-- 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
inst_3 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
j : J
k : K
dsimp :
  Eq (α := limit (F.flip ⋙ lim) ⟶ (F.obj j).obj k)
    (CategoryStruct.comp (Y := limit (F ⋙ lim))
      (CategoryStruct.comp (Y := limit (obj uncurry F.flip)) (Iso.inv (limitUncurryIsoLimitCompLim F.flip))
        (CategoryStruct.comp (Y := limit (Prod.swap K J ⋙ obj uncurry F))
          (Iso.hom (HasLimit.isoOfNatIso F.uncurryObjFlip))
          (CategoryStruct.comp (Y := limit (obj uncurry F))
            (Iso.hom
              (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents (fun (x : K × J) ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)))
            (Iso.hom (limitUncurryIsoLimitCompLim F)))))
      (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k))
    (limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j)
⊢ Iso.hom (limitFlipCompLimIsoLimitCompLim F) ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j

Tactic:
dsimp [limitFlipCompLimIsoLimitCompLim]

Premises used: CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim
-- 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
inst_3 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
j : J
k : K
⊢ Eq (α := limit (F.flip ⋙ lim) ⟶ (F.obj j).obj k)
    (CategoryStruct.comp (Y := limit (F ⋙ lim))
      (CategoryStruct.comp (Y := limit (obj uncurry F.flip)) (Iso.inv (limitUncurryIsoLimitCompLim F.flip))
        (CategoryStruct.comp (Y := limit (Prod.swap K J ⋙ obj uncurry F))
          (Iso.hom (HasLimit.isoOfNatIso F.uncurryObjFlip))
          (CategoryStruct.comp (Y := limit (obj uncurry F))
            (Iso.hom
              (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents (fun (x : K × J) ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)))
            (Iso.hom (limitUncurryIsoLimitCompLim F)))))
      (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k))
    (limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j)

Tactic:
simp [Equivalence.counit]

Premises used: CategoryTheory.Equivalence.counit
-- 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
inst_3 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_4 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
k : K
j : J
⊢ Iso.inv (limitFlipCompLimIsoLimitCompLim F) ≫ limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j =
    limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Tactic:
simp [limitFlipCompLimIsoLimitCompLim]

Premises used: CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim
-- 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
inst_3 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_4 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
x : K × J
⊢ (Equivalence.functor (Prod.braiding K J) ⋙ obj uncurry F).obj x ≅
    (Equivalence.functor (Prod.braiding K J) ⋙ obj uncurry F).obj x

Tactic:
rfl
-- 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
inst_3 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_4 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
j : J
k : K
dsimp :
  Eq (α := (F.obj j).obj k ⟶ colimit (F ⋙ colim))
    (colimit.ι (F.flip.obj k) j ≫
      CategoryStruct.comp (Y := colimit (F.flip ⋙ colim)) (colimit.ι (F.flip ⋙ colim) k)
        (CategoryStruct.comp (Y := colimit (obj uncurry F.flip)) (Iso.inv (colimitUncurryIsoColimitCompColim F.flip))
          (CategoryStruct.comp (Y := colimit (Prod.swap K J ⋙ obj uncurry F))
            (Iso.hom (HasColimit.isoOfNatIso F.uncurryObjFlip))
            (CategoryStruct.comp (Y := colimit (obj uncurry F))
              (Iso.hom
                (HasColimit.isoOfEquivalence (Prod.braiding K J)
                  (NatIso.ofComponents (fun (x : K × J) ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)))
              (Iso.hom (colimitUncurryIsoColimitCompColim F))))))
    (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j)
⊢ colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ Iso.hom (colimitFlipCompColimIsoColimitCompColim F) =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j

Tactic:
dsimp [colimitFlipCompColimIsoColimitCompColim]

Premises used: CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim
-- 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
inst_3 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_4 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
j : J
k : K
slice_lhs :
  Eq (α := (F.obj j).obj k ⟶ colimit (F ⋙ colim))
    (CategoryStruct.comp (Y := colimit (obj uncurry F))
      (CategoryStruct.comp (Y := colimit (Prod.swap K J ⋙ obj uncurry F))
        (CategoryStruct.comp (Y := colimit (obj uncurry F.flip))
          (colimit.ι (F.flip.obj k) j ≫
            CategoryStruct.comp (Y := colimit (F.flip ⋙ colim)) (colimit.ι (F.flip ⋙ colim) k)
              (Iso.inv (colimitUncurryIsoColimitCompColim F.flip)))
          (Iso.hom (HasColimit.isoOfNatIso F.uncurryObjFlip)))
        (Iso.hom
          (HasColimit.isoOfEquivalence (Prod.braiding K J)
            (NatIso.ofComponents (fun (x : K × J) ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯))))
      (Iso.hom (colimitUncurryIsoColimitCompColim F)))
    (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j)
⊢ Eq (α := (F.obj j).obj k ⟶ colimit (F ⋙ colim))
    (colimit.ι (F.flip.obj k) j ≫
      CategoryStruct.comp (Y := colimit (F.flip ⋙ colim)) (colimit.ι (F.flip ⋙ colim) k)
        (CategoryStruct.comp (Y := colimit (obj uncurry F.flip)) (Iso.inv (colimitUncurryIsoColimitCompColim F.flip))
          (CategoryStruct.comp (Y := colimit (Prod.swap K J ⋙ obj uncurry F))
            (Iso.hom (HasColimit.isoOfNatIso F.uncurryObjFlip))
            (CategoryStruct.comp (Y := colimit (obj uncurry F))
              (Iso.hom
                (HasColimit.isoOfEquivalence (Prod.braiding K J)
                  (NatIso.ofComponents (fun (x : K × J) ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)))
              (Iso.hom (colimitUncurryIsoColimitCompColim F))))))
    (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j)

Tactic:
slice_lhs 1 3 => simp only []