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
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))
    (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)

Tactic:
simp [Equivalence.unit]

Premises used: CategoryTheory.Equivalence.unit
-- 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
k : K
j : J
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)) ⋯))))
            (Iso.inv (HasColimit.isoOfNatIso F.uncurryObjFlip)))
          (Iso.hom (colimitUncurryIsoColimitCompColim F.flip))))
    (colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k)
⊢ colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ Iso.inv (colimitFlipCompColimIsoColimitCompColim F) =
    colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k

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
k : K
j : J
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)) ⋯))))
        (Iso.inv (HasColimit.isoOfNatIso F.uncurryObjFlip)))
      (Iso.hom (colimitUncurryIsoColimitCompColim F.flip)))
    (colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k)
⊢ 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)

Tactic:
slice_lhs 1 3 => simp only []
-- 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
k : K
j : J
⊢ 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)) ⋯))))
        (Iso.inv (HasColimit.isoOfNatIso F.uncurryObjFlip)))
      (Iso.hom (colimitUncurryIsoColimitCompColim F.flip)))
    (colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k)

Tactic:
simp [Equivalence.counitInv]

Premises used: CategoryTheory.Equivalence.counitInv
-- 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)
have : (i : G ≅ obj uncurry (obj curry G)) → limit G ≅ limit (obj curry G ⋙ lim)
⊢ limit G ≅ limit (obj curry G ⋙ lim)

Tactic:
have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G
-- 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)
i : G ≅ obj uncurry (obj curry G)
⊢ HasLimit (obj uncurry (obj curry G))

Tactic:
haveI : Limits.HasLimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasLimit_of_iso i
-- 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)
i : G ≅ obj uncurry (obj curry G)
this : HasLimit (obj uncurry (obj curry G))
trans : limit G ≅ limit (obj uncurry (obj curry G))
trans₁ : limit (obj uncurry (obj curry G)) ≅ limit (obj curry G ⋙ lim)
⊢ limit G ≅ limit (obj curry G ⋙ lim)

Tactic:
trans limit (uncurry.obj ((@curry J _ K _ C _).obj G))

Premises used: CategoryTheory.Functor.uncurry, CategoryTheory.Functor.curry, CategoryTheory.Limits.limit, 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 : 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 uncurry (obj curry G))

Tactic:
apply HasLimit.isoOfNatIso i

Premises used: CategoryTheory.Limits.HasLimit.isoOfNatIso
-- 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)
i : G ≅ obj uncurry (obj curry G)
this : HasLimit (obj uncurry (obj curry G))
⊢ limit (obj uncurry (obj curry G)) ≅ limit (obj curry G ⋙ lim)

Tactic:
exact limitUncurryIsoLimitCompLim ((@curry J _ K _ C _).obj G)

Premises used: CategoryTheory.Functor.curry, CategoryTheory.Limits.limitUncurryIsoLimitCompLim, 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
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 G ⟶ ((obj curry G).obj j).obj 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 ⟶ ((obj curry G).obj j).obj k)
    (limit.π G (j, k) : limit G ⟶ G.obj (j, k))

Tactic:
simp [limitIsoLimitCurryCompLim, Trans.simple]

Premises used: CategoryTheory.Limits.limitIsoLimitCurryCompLim, Trans.simple
-- 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
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
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))
⊢ 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)

Tactic:
rw [← cancel_epi (limitIsoLimitCurryCompLim G).hom]

Premises used: CategoryTheory.Limits.limitIsoLimitCurryCompLim, 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
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 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:
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 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
have : (i : G ≅ obj uncurry (obj curry G)) → colimit G ≅ colimit (obj curry G ⋙ colim)
⊢ colimit G ≅ colimit (obj curry G ⋙ colim)

Tactic:
have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G
-- 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)
i : G ≅ obj uncurry (obj curry G)
⊢ HasColimit (obj uncurry (obj curry G))

Tactic:
haveI : Limits.HasColimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasColimit_of_iso i.symm
-- 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)
i : G ≅ obj uncurry (obj curry G)
this : HasColimit (obj uncurry (obj curry G))
trans : colimit G ≅ colimit (obj uncurry (obj curry G))
trans₁ : colimit (obj uncurry (obj curry G)) ≅ colimit (obj curry G ⋙ colim)
⊢ colimit G ≅ colimit (obj curry G ⋙ colim)

Tactic:
trans colimit (uncurry.obj ((@curry J _ K _ C _).obj G))

Premises used: CategoryTheory.Functor.uncurry, CategoryTheory.Functor.curry, CategoryTheory.Limits.colimit, 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)
i : G ≅ obj uncurry (obj curry G)
this : HasColimit (obj uncurry (obj curry G))
⊢ colimit G ≅ colimit (obj uncurry (obj curry G))

Tactic:
apply HasColimit.isoOfNatIso i

Premises used: CategoryTheory.Limits.HasColimit.isoOfNatIso
-- 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)
i : G ≅ obj uncurry (obj curry G)
this : HasColimit (obj uncurry (obj curry G))
⊢ colimit (obj uncurry (obj curry G)) ≅ colimit (obj curry G ⋙ colim)

Tactic:
exact colimitUncurryIsoColimitCompColim ((@curry J _ K _ C _).obj G)

Premises used: CategoryTheory.Functor.curry, CategoryTheory.Limits.colimitUncurryIsoColimitCompColim, 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
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := ((obj curry G).obj j).obj k ⟶ colimit G)
    (colimit.ι ((obj curry G).obj j) k ≫
        CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim)) (colimit.ι (obj curry G ⋙ colim) j)
          (Iso.inv (colimitIsoColimitCurryCompColim G)) :
      ((obj curry G).obj j).obj k ⟶ colimit G)
    (colimit.ι G (j, k) : G.obj (j, k) ⟶ colimit G)

Tactic:
simp [colimitIsoColimitCurryCompColim, Trans.simple, colimitUncurryIsoColimitCompColim]

Premises used: CategoryTheory.Limits.colimitIsoColimitCurryCompColim, CategoryTheory.Limits.colimitUncurryIsoColimitCompColim, Trans.simple
-- 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
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
rw :
  Eq (α := G.obj (j, k) ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim))
        (colimit.ι G (j, k) ≫ Iso.hom (colimitIsoColimitCurryCompColim G))
        (Iso.inv (colimitIsoColimitCurryCompColim G)) :
      G.obj (j, k) ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim))
        (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)
        (Iso.inv (colimitIsoColimitCurryCompColim G)) :
      G.obj (j, k) ⟶ colimit G)
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry G ⋙ colim))
    (colimit.ι G (j, k) ≫ Iso.hom (colimitIsoColimitCurryCompColim G))
    (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)

Tactic:
rw [← cancel_mono (colimitIsoColimitCurryCompColim G).inv]

Premises used: CategoryTheory.Limits.colimitIsoColimitCurryCompColim, CategoryTheory.cancel_mono, 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
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := G.obj (j, k) ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim))
        (colimit.ι G (j, k) ≫ Iso.hom (colimitIsoColimitCurryCompColim G))
        (Iso.inv (colimitIsoColimitCurryCompColim G)) :
      G.obj (j, k) ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim))
        (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)
        (Iso.inv (colimitIsoColimitCurryCompColim G)) :
      G.obj (j, k) ⟶ colimit G)

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
G : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasLimit (obj curry G ⋙ lim)
j : J
k : K
dsimp :
  Eq (α := limit (obj curry (Prod.swap K J ⋙ G) ⋙ lim) ⟶ G.obj (j, k))
    (CategoryStruct.comp (Y := limit (obj curry G ⋙ lim))
      ((Iso.inv (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)) ≫
          Iso.hom (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G)))) ≫
        Iso.hom (limitIsoLimitCurryCompLim G))
      (limit.π (obj curry G ⋙ lim) j ≫ limit.π ((obj curry G).obj j) k))
    (limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j)
⊢ CategoryStruct.comp (Y := limit (obj curry G ⋙ lim)) (Iso.hom (limitCurrySwapCompLimIsoLimitCurryCompLim G))
      (limit.π (obj curry G ⋙ lim) j ≫ limit.π ((obj curry G).obj j) k) =
    limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j

Tactic:
dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim, Equivalence.counit]

Premises used: CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim, 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
G : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasLimit (obj curry G ⋙ lim)
j : J
k : K
rw :
  Eq (α := limit (obj curry (Prod.swap K J ⋙ G) ⋙ lim) ⟶ G.obj (j, k))
    (Iso.inv (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)) ≫
      CategoryStruct.comp (Y := (Prod.swap K J ⋙ G).obj (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)))
        (limit.π (Prod.swap K J ⋙ G) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)))
        (NatTrans.app (Iso.inv (Iso.refl (Prod.swap K J ⋙ G))) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)) ≫
          G.map (NatTrans.app (Equivalence.counit (Prod.braiding K J)) (j, k))))
    (limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j)
⊢ Eq (α := limit (obj curry (Prod.swap K J ⋙ G) ⋙ lim) ⟶ G.obj (j, k))
    (CategoryStruct.comp (Y := limit (obj curry G ⋙ lim))
      ((Iso.inv (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)) ≫
          Iso.hom (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G)))) ≫
        Iso.hom (limitIsoLimitCurryCompLim G))
      (limit.π (obj curry G ⋙ lim) j ≫ limit.π ((obj curry G).obj j) k))
    (limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j)

Tactic:
rw [Category.assoc, Category.assoc, limitIsoLimitCurryCompLim_hom_π_π,
    HasLimit.isoOfEquivalence_hom_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π, CategoryTheory.Limits.limitIsoLimitCurryCompLim_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
G : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasLimit (obj curry G ⋙ lim)
j : J
k : K
dsimp :
  Eq (α := limit (obj curry (Prod.swap K J ⋙ G) ⋙ lim) ⟶ G.obj (j, k))
    (Iso.inv (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)) ≫
      limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ G.map (Prod.mkHom (𝟙 j) (𝟙 k)))
    (limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j)
⊢ Eq (α := limit (obj curry (Prod.swap K J ⋙ G) ⋙ lim) ⟶ G.obj (j, k))
    (Iso.inv (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)) ≫
      CategoryStruct.comp (Y := (Prod.swap K J ⋙ G).obj (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)))
        (limit.π (Prod.swap K J ⋙ G) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)))
        (NatTrans.app (Iso.inv (Iso.refl (Prod.swap K J ⋙ G))) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)) ≫
          G.map (NatTrans.app (Equivalence.counit (Prod.braiding K J)) (j, k))))
    (limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j)

Tactic:
dsimp [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
G : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasLimit (obj curry G ⋙ lim)
j : J
k : K
rw :
  Eq (α := limit (obj curry (Prod.swap K J ⋙ G) ⋙ lim) ⟶ G.obj (j, k))
    (Iso.inv (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)) ≫
      CategoryStruct.comp (Y := G.obj (j, k))
        (limit.π (Prod.swap K J ⋙ G) (k, j) : limit (Prod.swap K J ⋙ G) ⟶ (Prod.swap K J ⋙ G).obj (k, j))
        (𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k))))
    (limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j)
⊢ Eq (α := limit (obj curry (Prod.swap K J ⋙ G) ⋙ lim) ⟶ G.obj (j, k))
    (Iso.inv (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)) ≫
      limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ G.map (Prod.mkHom (𝟙 j) (𝟙 k)))
    (limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j)

Tactic:
rw [← prod_id, G.map_id]

Premises used: CategoryTheory.prod_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
G : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasLimit (obj curry G ⋙ lim)
j : J
k : K
⊢ Eq (α := limit (obj curry (Prod.swap K J ⋙ G) ⋙ lim) ⟶ G.obj (j, k))
    (Iso.inv (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)) ≫
      CategoryStruct.comp (Y := G.obj (j, k))
        (limit.π (Prod.swap K J ⋙ G) (k, j) : limit (Prod.swap K J ⋙ G) ⟶ (Prod.swap K J ⋙ G).obj (k, j))
        (𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k))))
    (limit.π (obj curry (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((obj curry (Prod.swap K J ⋙ G)).obj k) j)

Tactic:
simp