awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
⊢ 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₂)))
have 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))
Tactic: dsimp [Q] at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
⊢ 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))
have 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)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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))
    (((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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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')
have 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')))
Tactic: refine colimit.hom_ext (F := curry.obj G ⋙ colim) (fun j ↦ colimit.hom_ext (fun k ↦ ?_))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
⊢ colimit (obj uncurry F) ≅ colimit (F ⋙ colim)
have have : (Q' : IsColimit (coconeOfCoconeUncurry Q c)) → colimit (obj uncurry F) ≅ colimit (F ⋙ colim)
Tactic: have Q' := coconeOfCoconeUncurryIsColimit Q P
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
⊢ colimit (obj uncurry F) ≅ colimit (F ⋙ colim)
have have : (Q'' : IsColimit (colimit.cocone (F ⋙ colim))) → colimit (obj uncurry F) ≅ colimit (F ⋙ colim)
Tactic: have Q'' := colimit.isColimit (F ⋙ colim)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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))
    (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))
have 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))
Tactic: dsimp [colimitUncurryIsoColimitCompColim, IsColimit.coconePointUniqueUpToIso,
    IsColimit.uniqueUpToIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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 (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)
have 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)))
Tactic: rw [← cancel_mono (colimitUncurryIsoColimitCompColim F).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
⊢ Iso.hom (limitFlipCompLimIsoLimitCompLim F) ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j
have 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)) sorry)))
          (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: dsimp [limitFlipCompLimIsoLimitCompLim]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
⊢ colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ Iso.hom (colimitFlipCompColimIsoColimitCompColim F) =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j
have 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)) sorry)))
            (Iso.hom (colimitUncurryIsoColimitCompColim F))))))
  (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j)
Tactic: dsimp [colimitFlipCompColimIsoColimitCompColim]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
⊢ 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)
have 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)) sorry))))
    (Iso.hom (colimitUncurryIsoColimitCompColim F)))
  (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j)
Tactic: slice_lhs 1 3 => simp only []
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
k : K
j : J
⊢ colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ Iso.inv (colimitFlipCompColimIsoColimitCompColim F) =
    colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k
have dsimp : Eq (α := (F.obj j).obj k ⟶ colimit (F.flip ⋙ colim))
  (colimit.ι (F.obj j) k ≫
    CategoryStruct.comp (Y := colimit (F ⋙ colim)) (colimit.ι (F ⋙ colim) j)
      (CategoryStruct.comp (Y := colimit (obj uncurry F.flip))
        (CategoryStruct.comp (Y := colimit (Prod.swap K J ⋙ obj uncurry F))
          (CategoryStruct.comp (Y := colimit (obj uncurry F)) (Iso.inv (colimitUncurryIsoColimitCompColim F))
            (Iso.inv
              (HasColimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents (fun (x : K × J) ↦ Iso.refl ((F.obj x.2).obj x.1)) sorry))))
          (Iso.inv (HasColimit.isoOfNatIso F.uncurryObjFlip)))
        (Iso.hom (colimitUncurryIsoColimitCompColim F.flip))))
  (colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k)
Tactic: dsimp [colimitFlipCompColimIsoColimitCompColim]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
k : K
j : J
⊢ Eq (α := (F.obj j).obj k ⟶ colimit (F.flip ⋙ colim))
    (colimit.ι (F.obj j) k ≫
      CategoryStruct.comp (Y := colimit (F ⋙ colim)) (colimit.ι (F ⋙ colim) j)
        (CategoryStruct.comp (Y := colimit (obj uncurry F.flip))
          (CategoryStruct.comp (Y := colimit (Prod.swap K J ⋙ obj uncurry F))
            (CategoryStruct.comp (Y := colimit (obj uncurry F)) (Iso.inv (colimitUncurryIsoColimitCompColim F))
              (Iso.inv
                (HasColimit.isoOfEquivalence (Prod.braiding K J)
                  (NatIso.ofComponents (fun (x : K × J) ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯))))
            (Iso.inv (HasColimit.isoOfNatIso F.uncurryObjFlip)))
          (Iso.hom (colimitUncurryIsoColimitCompColim F.flip))))
    (colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k)
have slice_lhs : Eq (α := (F.obj j).obj k ⟶ colimit (F.flip ⋙ colim))
  (CategoryStruct.comp (Y := colimit (obj uncurry F.flip))
    (CategoryStruct.comp (Y := colimit (Prod.swap K J ⋙ obj uncurry F))
      (CategoryStruct.comp (Y := colimit (obj uncurry F))
        (colimit.ι (F.obj j) k ≫
          CategoryStruct.comp (Y := colimit (F ⋙ colim)) (colimit.ι (F ⋙ colim) j)
            (Iso.inv (colimitUncurryIsoColimitCompColim F)))
        (Iso.inv
          (HasColimit.isoOfEquivalence (Prod.braiding K J)
            (NatIso.ofComponents (fun (x : K × J) ↦ Iso.refl ((F.obj x.2).obj x.1)) sorry))))
      (Iso.inv (HasColimit.isoOfNatIso F.uncurryObjFlip)))
    (Iso.hom (colimitUncurryIsoColimitCompColim F.flip)))
  (colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k)
Tactic: slice_lhs 1 3 => simp only []
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
⊢ limit G ≅ limit (obj curry G ⋙ lim)
have have : (i : G ≅ obj uncurry (obj curry G)) → limit G ≅ limit (obj curry G ⋙ lim)
Tactic: have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (hypothesis)
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)
i : G ≅ obj uncurry (obj curry G)
⊢ limit G ≅ limit (obj curry G ⋙ lim)
have this : HasLimit (obj uncurry (obj curry G))
Tactic: haveI : Limits.HasLimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasLimit_of_iso i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
i : G ≅ obj uncurry (obj curry G)
this : HasLimit (obj uncurry (obj curry G))
⊢ limit G ≅ limit (obj curry G ⋙ lim)
have trans : limit G ≅ limit (obj uncurry (obj curry G))
Tactic: trans limit (uncurry.obj ((@curry J _ K _ C _).obj G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
i : G ≅ obj uncurry (obj curry G)
this : HasLimit (obj uncurry (obj curry G))
trans : limit G ≅ limit (obj uncurry (obj curry G))
⊢ limit G ≅ limit (obj curry G ⋙ lim)
have trans₁ : limit (obj uncurry (obj curry G)) ≅ limit (obj curry G ⋙ lim)
Tactic: trans limit (uncurry.obj ((@curry J _ K _ C _).obj G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
G : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
j : J
k : K
⊢ Eq (α := limit (obj curry G ⋙ lim) ⟶ G.obj (j, k)) (Iso.inv (limitIsoLimitCurryCompLim G) ≫ limit.π G (j, k))
    (limit.π (obj curry G ⋙ lim) j ≫ limit.π ((obj curry G).obj j) k)
have rw : Eq (α := limit G ⟶ G.obj (j, k))
  (CategoryStruct.comp (Y := limit (obj curry G ⋙ lim)) (Iso.hom (limitIsoLimitCurryCompLim G))
      (Iso.inv (limitIsoLimitCurryCompLim G) ≫ limit.π G (j, k)) :
    limit G ⟶ G.obj (j, k))
  (CategoryStruct.comp (Y := limit (obj curry G ⋙ lim)) (Iso.hom (limitIsoLimitCurryCompLim G))
      (limit.π (obj curry G ⋙ lim) j ≫ limit.π ((obj curry G).obj j) k) :
    limit G ⟶ G.obj (j, k))
Tactic: rw [← cancel_epi (limitIsoLimitCurryCompLim G).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
⊢ colimit G ≅ colimit (obj curry G ⋙ colim)
have have : (i : G ≅ obj uncurry (obj curry G)) → colimit G ≅ colimit (obj curry G ⋙ colim)
Tactic: have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (hypothesis)
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)
i : G ≅ obj uncurry (obj curry G)
⊢ colimit G ≅ colimit (obj curry G ⋙ colim)
have this : HasColimit (obj uncurry (obj curry G))
Tactic: haveI : Limits.HasColimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasColimit_of_iso i.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
i : G ≅ obj uncurry (obj curry G)
this : HasColimit (obj uncurry (obj curry G))
⊢ colimit G ≅ colimit (obj curry G ⋙ colim)
have trans : colimit G ≅ colimit (obj uncurry (obj curry G))
Tactic: trans colimit (uncurry.obj ((@curry J _ K _ C _).obj G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
i : G ≅ obj uncurry (obj curry G)
this : HasColimit (obj uncurry (obj curry G))
trans : colimit G ≅ colimit (obj uncurry (obj curry G))
⊢ colimit G ≅ colimit (obj curry G ⋙ colim)
have trans₁ : colimit (obj uncurry (obj curry G)) ≅ colimit (obj curry G ⋙ colim)
Tactic: trans colimit (uncurry.obj ((@curry J _ K _ C _).obj G))