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

Tactic:
simp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj,
        Cocone.precompose_obj_pt, Cocone.whisker_pt, Functor.const_obj_obj,
        Cocone.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app, NatIso.ofComponents_inv_app,
        Iso.refl_inv, whiskerLeft_app, Category.id_comp, E] at h1

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.Cocone.whisker_pt, CategoryTheory.Limits.Cocone.whisker_ι, CategoryTheory.NatIso.ofComponents_inv_app, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.uncurry_obj_obj, CategoryTheory.Limits.Cocone.precompose_obj_ι, CategoryTheory.Iso.refl_inv, CategoryTheory.Prod.sectR_obj, CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.comp_app, CategoryTheory.Limits.Cocone.precompose_obj_pt, CategoryTheory.Category.id_comp
-- 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)
P : IsColimit (coconeOfCoconeUncurry 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 : Cocone (obj uncurry F)) → Cocone D.coconePoints :=
  fun (s : Cocone (obj uncurry F)) ↦
    { pt := s.pt,
      ι :=
        { app := fun (j : J) ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (obj uncurry F)
p : J × K
h1 :
  Eq (α := (F.obj p.1).obj p.2 ⟶ s.pt)
    (CategoryStruct.comp (Y := Cocone.pt (F := F.obj p.1) (D.obj p.1)) (NatTrans.app (Cocone.ι (D.obj p.1)) p.2)
        (desc (Q p.1)
          (obj (C := Cocone (Prod.sectR p.1 K ⋙ obj uncurry F))
            (Cocone.precompose (Iso.inv (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) ⋯)))
            (Cocone.whisker (Prod.sectR p.1 K) s))) :
      (F.obj p.1).obj p.2 ⟶ s.pt)
    (s.ι.app (p.1, p.2) : (obj uncurry F).obj (p.1, p.2) ⟶ obj (obj (const (J × K)) s.pt) (p.1, p.2))
⊢ Eq (α := D.coconePoints.obj p.1 ⟶ (S s).pt) ((coconeOfCoconeUncurry Q c).ι.app p.1 ≫ P.desc (S s)) ((S s).ι.app p.1)

Tactic:
have h2 := (P.fac (S s) p.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)
P : IsColimit (coconeOfCoconeUncurry 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 : Cocone (obj uncurry F)) → Cocone D.coconePoints :=
  fun (s : Cocone (obj uncurry F)) ↦
    { pt := s.pt,
      ι :=
        { app := fun (j : J) ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (obj uncurry F)
f : c.pt ⟶ s.pt
hf : ∀ (j : J × K), c.ι.app j ≫ f = s.ι.app j
j : J
k : K
⊢ (D.obj j).ι.app k ≫ (coconeOfCoconeUncurry Q c).ι.app j ≫ f = (D.obj j).ι.app k ≫ (S s).ι.app j

Tactic:
simpa [S, E] using hf (j, k)

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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
⊢ (mkOfHasLimits F).conePoints = F ⋙ lim

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.DiagramOfCones.conePoints, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap, 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
G : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
⊢ Eq (α := Cone.pt (F := (obj curry G).obj x.1) (Q.obj x.1) ⟶ ((obj curry G).obj x.1).obj y.2)
    (NatTrans.app (Cone.π (Q.obj x.1)) x.2 ≫ ((obj curry G).obj x.1).map f₂) (NatTrans.app (Cone.π (Q.obj x.1)) y.2)

Tactic:
have := (Q.obj x.1).w f₂
-- 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_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := Cone.pt (F := (obj curry G).obj x.1) (Q.obj x.1) ⟶ ((obj curry G).obj x.1).obj y.2)
    (NatTrans.app (Cone.π (Q.obj x.1)) x.2 ≫ ((obj curry G).obj x.1).map f₂) (NatTrans.app (Cone.π (Q.obj x.1)) y.2)
dsimp :
  𝟙 (limit (obj curry G ⋙ lim)) ≫ limit.π (obj curry G ⋙ lim) y.1 ≫ limit.π ((obj curry G).obj y.1) y.2 =
    (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)
⊢ Eq.{v_3 + 1} (α := obj (obj (const (J × K)) (limit (obj curry G ⋙ lim))) x ⟶ G.obj y)
    (Functor.map (obj (const (J × K)) (limit (obj curry G ⋙ lim))) (f₁, f₂) ≫
      limit.π (obj curry G ⋙ lim) y.1 ≫ NatTrans.app (Cone.π (Q.obj y.1)) y.2)
    ((limit.π (obj curry G ⋙ lim) x.1 ≫ NatTrans.app (Cone.π (Q.obj x.1)) x.2) ≫ G.map (f₁, f₂))

Tactic:
dsimp [Q] at 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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := limit ((obj curry G).obj x.1) ⟶ G.obj (x.1, y.2))
    (limit.π ((obj curry G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂)) (limit.π ((obj curry G).obj x.1) y.2)
rw :
  𝟙 (limit (obj curry G ⋙ lim)) ≫
      (limit.π (obj curry G ⋙ lim) x.1 ≫ (obj curry G ⋙ lim).map f₁) ≫ limit.π ((obj curry G).obj y.1) y.2 =
    (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)
⊢ 𝟙 (limit (obj curry G ⋙ lim)) ≫ limit.π (obj curry G ⋙ lim) y.1 ≫ limit.π ((obj curry G).obj y.1) y.2 =
    (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)

Tactic:
rw [← limit.w (F := curry.obj G ⋙ lim) (f := f₁)]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.lim, CategoryTheory.Functor.curry, CategoryTheory.Functor.obj, CategoryTheory.Limits.limit.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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := limit ((obj curry G).obj x.1) ⟶ G.obj (x.1, y.2))
    (limit.π ((obj curry G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂)) (limit.π ((obj curry G).obj x.1) y.2)
dsimp :
  𝟙 (limit (obj curry G ⋙ lim)) ≫
      CategoryStruct.comp (Y := limit ((obj curry G).obj y.1))
        (limit.π (obj curry G ⋙ lim) x.1 ≫ limMap ((obj curry G).map f₁)) (limit.π ((obj curry G).obj y.1) y.2) =
    (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)
⊢ 𝟙 (limit (obj curry G ⋙ lim)) ≫
      (limit.π (obj curry G ⋙ lim) x.1 ≫ (obj curry G ⋙ lim).map f₁) ≫ limit.π ((obj curry G).obj y.1) y.2 =
    (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, 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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := limit ((obj curry G).obj x.1) ⟶ G.obj (x.1, y.2))
    (limit.π ((obj curry G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂)) (limit.π ((obj curry G).obj x.1) y.2)
⊢ 𝟙 (limit (obj curry G ⋙ lim)) ≫
      CategoryStruct.comp (Y := limit ((obj curry G).obj y.1))
        (limit.π (obj curry G ⋙ lim) x.1 ≫ limMap ((obj curry G).map f₁)) (limit.π ((obj curry G).obj y.1) y.2) =
    (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)

Tactic:
simp only [Category.assoc, Category.id_comp, Prod.fac (f₁, f₂),
          G.map_comp, limMap_π, curry_obj_map_app, reassoc_of% this]

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Category.assoc, Prod.mk, CategoryTheory.Prod.fac, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.curry_obj_map_app, CategoryTheory.Category.id_comp
-- 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_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
Q' : (j : J) → IsLimit (Q.obj j) := fun (j : J) ↦ limit.isLimit ((obj curry G).obj j)
c' : Cone G
f : J × K
⊢ limit.lift (obj curry G ⋙ lim) (coneOfConeCurry G Q' c') ≫ (coneOfHasLimitCurryCompLim G).π.app f = c'.π.app f

Tactic:
simp [coneOfHasLimitCurryCompLim, Q, Q']

Premises used: CategoryTheory.Limits.coneOfHasLimitCurryCompLim
-- 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_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
Q' : (j : J) → IsLimit (Q.obj j) := fun (j : J) ↦ limit.isLimit ((obj curry G).obj j)
c' : Cone G
f : c'.pt ⟶ (coneOfHasLimitCurryCompLim G).pt
h : ∀ (j : J × K), f ≫ (coneOfHasLimitCurryCompLim G).π.app j = c'.π.app j
dsimp : f = limit.lift (obj curry G ⋙ lim) (coneOfConeCurry G Q' c')
⊢ f = limit.lift (obj curry G ⋙ lim) (coneOfConeCurry G Q' c')

Tactic:
dsimp [coneOfHasLimitCurryCompLim] at f h ⊢

Premises used: CategoryTheory.Limits.coneOfHasLimitCurryCompLim
-- 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_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
Q' : (j : J) → IsLimit (Q.obj j) := fun (j : J) ↦ limit.isLimit ((obj curry G).obj j)
c' : Cone G
f : c'.pt ⟶ limit (obj curry G ⋙ lim)
h : ∀ (j : J × K), f ≫ limit.π (obj curry G ⋙ lim) j.1 ≫ limit.π ((obj curry G).obj j.1) j.2 = c'.π.app j
⊢ f = limit.lift (obj curry G ⋙ lim) (coneOfConeCurry G Q' c')

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

Premises used: CategoryTheory.Limits.limit.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 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
Q' : (j : J) → IsLimit (Q.obj j) := fun (j : J) ↦ limit.isLimit ((obj curry G).obj j)
c' : Cone G
f : c'.pt ⟶ limit (obj curry G ⋙ lim)
h : ∀ (j : J × K), f ≫ limit.π (obj curry G ⋙ lim) j.1 ≫ limit.π ((obj curry G).obj j.1) j.2 = c'.π.app j
refine :
  ∀ (j : J) (k : K),
    (f ≫ limit.π (obj curry G ⋙ lim) j) ≫ limit.π ((obj curry G).obj j) k =
      CategoryStruct.comp (Y := limit ((obj curry G).obj j))
        (CategoryStruct.comp (Y := limit (obj curry G ⋙ lim)) (limit.lift (obj curry G ⋙ lim) (coneOfConeCurry G Q' c'))
          (limit.π (obj curry G ⋙ lim) j))
        (limit.π ((obj curry G).obj j) k)
⊢ f = limit.lift (obj curry G ⋙ lim) (coneOfConeCurry G Q' c')

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

Premises used: CategoryTheory.Limits.limit.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_1 : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
c : Cone (obj uncurry F) := limit.cone (obj uncurry F)
P : IsLimit c := limit.isLimit (obj uncurry F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (G.obj j) := fun (j : J) ↦ limit.isLimit (F.obj j)
have : (Q' : IsLimit (coneOfConeUncurry Q c)) → limit (obj uncurry F) ≅ limit (F ⋙ lim)
⊢ limit (obj uncurry F) ≅ limit (F ⋙ lim)

Tactic:
have Q' := coneOfConeUncurryIsLimit 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 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
c : Cone (obj uncurry F) := limit.cone (obj uncurry F)
P : IsLimit c := limit.isLimit (obj uncurry F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (G.obj j) := fun (j : J) ↦ limit.isLimit (F.obj j)
Q' : IsLimit (coneOfConeUncurry Q c)
have : (Q'' : IsLimit (limit.cone (F ⋙ lim))) → limit (obj uncurry F) ≅ limit (F ⋙ lim)
⊢ limit (obj uncurry F) ≅ limit (F ⋙ lim)

Tactic:
have Q'' := limit.isLimit (F ⋙ lim)
-- 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 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
c : Cone (obj uncurry F) := limit.cone (obj uncurry F)
P : IsLimit c := limit.isLimit (obj uncurry F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (G.obj j) := fun (j : J) ↦ limit.isLimit (F.obj j)
Q' : IsLimit (coneOfConeUncurry Q c)
Q'' : IsLimit (limit.cone (F ⋙ lim))
⊢ limit (obj uncurry F) ≅ limit (F ⋙ lim)

Tactic:
exact IsLimit.conePointUniqueUpToIso Q' Q''

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso
-- 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_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
j : J
k : K
dsimp :
  Eq (α := limit (obj uncurry F) ⟶ (F.obj j).obj k)
    (CategoryStruct.comp (Y := limit (F ⋙ lim))
        (limit.lift (F ⋙ lim) (coneOfConeUncurry (fun (j : J) ↦ limit.isLimit (F.obj j)) (limit.cone (obj uncurry F))))
        (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k) :
      limit (obj uncurry F) ⟶ (F.obj j).obj k)
    (limit.π (obj uncurry F) (j, k) : limit (obj uncurry F) ⟶ (obj uncurry F).obj (j, k))
⊢ Eq (α := limit (obj uncurry F) ⟶ (F.obj j).obj k)
    (CategoryStruct.comp (Y := limit (F ⋙ lim)) (Iso.hom (limitUncurryIsoLimitCompLim F))
      (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k))
    (limit.π (obj uncurry F) (j, k))

Tactic:
dsimp [limitUncurryIsoLimitCompLim, IsLimit.conePointUniqueUpToIso, IsLimit.uniqueUpToIso]

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.IsLimit.uniqueUpToIso, CategoryTheory.Limits.limitUncurryIsoLimitCompLim
-- 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_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
j : J
k : K
⊢ Eq (α := limit (obj uncurry F) ⟶ (F.obj j).obj k)
    (CategoryStruct.comp (Y := limit (F ⋙ lim))
        (limit.lift (F ⋙ lim) (coneOfConeUncurry (fun (j : J) ↦ limit.isLimit (F.obj j)) (limit.cone (obj uncurry F))))
        (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k) :
      limit (obj uncurry F) ⟶ (F.obj j).obj k)
    (limit.π (obj uncurry F) (j, k) : limit (obj uncurry F) ⟶ (obj uncurry F).obj (j, k))

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 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
j : J
k : K
rw :
  Eq (α := limit (obj uncurry F) ⟶ (obj uncurry F).obj (j, k))
    (CategoryStruct.comp (Y := limit (F ⋙ lim)) (Iso.hom (limitUncurryIsoLimitCompLim F))
      (CategoryStruct.comp (Y := limit (obj uncurry F)) (Iso.inv (limitUncurryIsoLimitCompLim F))
        (limit.π (obj uncurry F) (j, k))))
    (CategoryStruct.comp (Y := limit (F ⋙ lim)) (Iso.hom (limitUncurryIsoLimitCompLim F))
      (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k))
⊢ Eq (α := limit (F ⋙ lim) ⟶ (obj uncurry F).obj (j, k))
    (CategoryStruct.comp (Y := limit (obj uncurry F)) (Iso.inv (limitUncurryIsoLimitCompLim F))
      (limit.π (obj uncurry F) (j, k)))
    (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k)

Tactic:
rw [← cancel_epi (limitUncurryIsoLimitCompLim F).hom]

Premises used: CategoryTheory.Limits.limitUncurryIsoLimitCompLim, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- 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_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
j : J
k : K
⊢ Eq (α := limit (obj uncurry F) ⟶ (obj uncurry F).obj (j, k))
    (CategoryStruct.comp (Y := limit (F ⋙ lim)) (Iso.hom (limitUncurryIsoLimitCompLim F))
      (CategoryStruct.comp (Y := limit (obj uncurry F)) (Iso.inv (limitUncurryIsoLimitCompLim F))
        (limit.π (obj uncurry F) (j, k))))
    (CategoryStruct.comp (Y := limit (F ⋙ lim)) (Iso.hom (limitUncurryIsoLimitCompLim F))
      (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k))

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
⊢ (mkOfHasColimits F).coconePoints = F ⋙ colim

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map, CategoryTheory.Limits.DiagramOfCocones.coconePoints, 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
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
⊢ Eq (α := ((obj curry G).obj y.1).obj x.2 ⟶ Cocone.pt (F := (obj curry G).obj y.1) (Q.obj y.1))
    (((obj curry G).obj y.1).map f₂ ≫ NatTrans.app (Cocone.ι (Q.obj y.1)) y.2) (NatTrans.app (Cocone.ι (Q.obj y.1)) x.2)

Tactic:
have := (Q.obj y.1).w f₂
-- 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 (α := ((obj curry G).obj y.1).obj x.2 ⟶ Cocone.pt (F := (obj curry G).obj y.1) (Q.obj y.1))
    (((obj curry G).obj y.1).map f₂ ≫ NatTrans.app (Cocone.ι (Q.obj y.1)) y.2) (NatTrans.app (Cocone.ι (Q.obj y.1)) x.2)
dsimp :
  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))
⊢ Eq (α := G.obj x ⟶ obj (obj (const (J × K)) (colimit (obj curry G ⋙ colim))) y)
    (G.map (f₁, f₂) ≫ NatTrans.app (Cocone.ι (Q.obj y.1)) y.2 ≫ colimit.ι (obj curry G ⋙ colim) y.1)
    (CategoryStruct.comp (Y := obj (obj (const (J × K)) (colimit (obj curry G ⋙ colim))) x)
      (NatTrans.app (Cocone.ι (Q.obj x.1)) x.2 ≫ colimit.ι (obj curry G ⋙ colim) x.1)
      (Functor.map (obj (const (J × K)) (colimit (obj curry G ⋙ colim))) (f₁, f₂)))

Tactic:
dsimp [Q] at this ⊢