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
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 (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)
have 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)
Tactic: rw [← cancel_mono (colimitIsoColimitCurryCompColim G).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
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
⊢ 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
have 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)
Tactic: dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim, Equivalence.counit]
-- 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 : 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))
    (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)
have 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)
Tactic: rw [Category.assoc, Category.assoc, limitIsoLimitCurryCompLim_hom_π_π,
    HasLimit.isoOfEquivalence_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
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 := (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)
have 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)
Tactic: dsimp [Equivalence.counit]
-- 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 : 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)) ≫
      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)
have 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)
Tactic: rw [← prod_id, G.map_id]
-- 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 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := ((obj curry (Prod.swap K J ⋙ G)).obj k).obj j ⟶ colimit (obj curry G ⋙ colim))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫
      colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k ≫
        Iso.hom (colimitCurrySwapCompColimIsoColimitCurryCompColim G))
    (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)
have dsimp : Eq (α := G.obj (j, k) ⟶ colimit (obj curry G ⋙ colim))
  (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫
    CategoryStruct.comp (Y := colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
      (colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
      ((Iso.inv (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)) ≫
          Iso.hom (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G)))) ≫
        Iso.hom (colimitIsoColimitCurryCompColim G)))
  (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)
Tactic: dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
-- 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 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry G ⋙ colim))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫
      CategoryStruct.comp (Y := colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
        (colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
        ((Iso.inv (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)) ≫
            Iso.hom (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G)))) ≫
          Iso.hom (colimitIsoColimitCurryCompColim G)))
    (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ colim) j)
have slice_lhs : Eq (α := G.obj (j, k) ⟶ colimit (obj curry G ⋙ colim))
  (CategoryStruct.comp (Y := colimit (Prod.swap K J ⋙ G))
      (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫
          CategoryStruct.comp (Y := colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
            (colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
            (Iso.inv (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G))) :
        G.obj (j, k) ⟶ colimit (Prod.swap K J ⋙ G))
      (Iso.hom (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) :
        colimit (Prod.swap K J ⋙ G) ⟶ colimit G) ≫
    Iso.hom (colimitIsoColimitCurryCompColim G))
  (colimit.ι ((obj curry G).obj j) k ≫ colimit.ι (obj curry G ⋙ 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
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((obj curry G).obj j) k ≫
      CategoryStruct.comp (Y := colimit (obj curry G ⋙ colim)) (colimit.ι (obj curry G ⋙ colim) j)
        (Iso.inv (colimitCurrySwapCompColimIsoColimitCurryCompColim G)) =
    colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k
have dsimp : Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
  (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) ≫
        Iso.inv (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) ≫
          Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G))))
  (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
Tactic: dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
-- 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 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    (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) ≫
          Iso.inv (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) ≫
            Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G))))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
have slice_lhs : Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
  (CategoryStruct.comp (Y := 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)) :
        G.obj (j, k) ⟶ colimit G)
      (Iso.inv (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) :
        colimit G ⟶ colimit (Prod.swap K J ⋙ G)) ≫
    Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
  (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ 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
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    (CategoryStruct.comp (Y := 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)) :
          G.obj (j, k) ⟶ colimit G)
        (Iso.inv (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))) :
          colimit G ⟶ colimit (Prod.swap K J ⋙ G)) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
have rw : Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
  (CategoryStruct.comp (Y :=
      G.obj (obj (Equivalence.inverse (Prod.braiding K J) ⋙ Equivalence.functor (Prod.braiding K J)) (j, k)))
      (G.map (NatTrans.app (Equivalence.counitInv (Prod.braiding K J)) (j, k)))
      (NatTrans.app (Iso.hom (Iso.refl (Prod.swap K J ⋙ G))) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)) ≫
        colimit.ι (Prod.swap K J ⋙ G) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k))) ≫
    Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
  (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
Tactic: rw [colimitIsoColimitCurryCompColim_ι_ι_inv, HasColimit.ι_isoOfEquivalence_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
G : J × K ⥤ C
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    (CategoryStruct.comp (Y :=
        G.obj (obj (Equivalence.inverse (Prod.braiding K J) ⋙ Equivalence.functor (Prod.braiding K J)) (j, k)))
        (G.map (NatTrans.app (Equivalence.counitInv (Prod.braiding K J)) (j, k)))
        (NatTrans.app (Iso.hom (Iso.refl (Prod.swap K J ⋙ G))) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k)) ≫
          colimit.ι (Prod.swap K J ⋙ G) (obj (Equivalence.inverse (Prod.braiding K J)) (j, k))) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
have dsimp : Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
  ((G.map (Prod.mkHom (𝟙 j) (𝟙 k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
    Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
  (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
Tactic: dsimp [Equivalence.counitInv]
-- 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 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimitsOfShape.{v_1, u_1, v_3, u_3} J C
inst_5 : HasColimit (obj curry G ⋙ colim)
j : J
k : K
⊢ Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
    ((G.map (Prod.mkHom (𝟙 j) (𝟙 k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
    (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
have rw : Eq (α := G.obj (j, k) ⟶ colimit (obj curry (Prod.swap K J ⋙ G) ⋙ colim))
  ((𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
    Iso.hom (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)))
  (colimit.ι ((obj curry (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (obj curry (Prod.swap K J ⋙ G) ⋙ colim) k)
Tactic: rw [CategoryTheory.Bifunctor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
c : Cone F
t : (k : K) → IsLimit (F := F ⋙ obj (evaluation K C) k) (mapCone (obj (evaluation K C) k) c)
s : Cone F
X Y : K
f : X ⟶ Y
j : J
⊢ Eq (α := s.pt.obj X ⟶ (F ⋙ obj (evaluation K C) Y).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ obj (evaluation K C) Y) (mapCone (obj (evaluation K C) Y) c))
      (s.pt.map f ≫ (t Y).lift { pt := s.pt.obj Y, π := whiskerRight s.π (obj (evaluation K C) Y) } :
        s.pt.obj X ⟶ c.pt.obj Y)
      (NatTrans.app (Cone.π (mapCone (obj (evaluation K C) Y) c)) j :
        obj.{v₁, v, u₁, u}
            (obj (const J) (Cone.pt (F := F ⋙ obj (evaluation K C) Y) (mapCone (obj (evaluation K C) Y) c))) j ⟶
          (F ⋙ obj (evaluation K C) Y).obj j))
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ obj (evaluation K C) Y) (mapCone (obj (evaluation K C) Y) c))
      ((t X).lift { pt := s.pt.obj X, π := whiskerRight s.π (obj (evaluation K C) X) } ≫ c.pt.map f :
        s.pt.obj X ⟶ c.pt.obj Y)
      (NatTrans.app (Cone.π (mapCone (obj (evaluation K C) Y) c)) j :
        obj.{v₁, v, u₁, u}
            (obj (const J) (Cone.pt (F := F ⋙ obj (evaluation K C) Y) (mapCone (obj (evaluation K C) Y) c))) j ⟶
          (F ⋙ obj (evaluation K C) Y).obj j))
have rw : s.pt.map f ≫
    { pt := s.pt.obj Y, π := whiskerRight s.π (obj (evaluation K C) Y) : Cone (F ⋙ obj (evaluation K C) Y) }.π.app j =
  CategoryStruct.comp (Y := Cone.pt (F := F ⋙ obj (evaluation K C) Y) (mapCone (obj (evaluation K C) Y) c))
    ((t X).lift { pt := s.pt.obj X, π := whiskerRight s.π (obj (evaluation K C) X) } ≫ c.pt.map f :
      s.pt.obj X ⟶ c.pt.obj Y)
    (NatTrans.app (Cone.π (mapCone (obj (evaluation K C) Y) c)) j :
      obj.{v₁, v, u₁, u}
          (obj (const J) (Cone.pt (F := F ⋙ obj (evaluation K C) Y) (mapCone (obj (evaluation K C) Y) c))) j ⟶
        (F ⋙ obj (evaluation K C) Y).obj j)
Tactic: rw [assoc, (t Y).fac _ j]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
c : Cone F
t : (k : K) → IsLimit (F := F ⋙ obj (evaluation K C) k) (mapCone (obj (evaluation K C) k) c)
s : Cone F
j : J
⊢ { app := fun (k : K) ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π (obj (evaluation K C) k) },
        naturality := ⋯ } ≫
      c.π.app j =
    s.π.app j
have w : ∀ (k : K),
  NatTrans.app
      ({ app := fun (k : K) ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π (obj (evaluation K C) k) },
          naturality := sorry } ≫
        c.π.app j)
      k =
    (s.π.app j).app k
Tactic: ext k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
c : Cone F
t : (k : K) → IsLimit (F := F ⋙ obj (evaluation K C) k) (mapCone (obj (evaluation K C) k) c)
s : Cone F
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m =
    { app := fun (k : K) ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π (obj (evaluation K C) k) },
      naturality := ⋯ }
have w₁ : ∀ (x : K),
  m.app x =
    NatTrans.app
      { app := fun (k : K) ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π (obj (evaluation K C) k) },
        naturality := sorry }
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
c : Cocone F
t : (k : K) → IsColimit (F := F ⋙ obj (evaluation K C) k) (mapCocone (obj (evaluation K C) k) c)
s : Cocone F
X Y : K
f : X ⟶ Y
j : J
⊢ Eq (α := (F ⋙ obj (evaluation K C) X).obj j ⟶ s.pt.obj Y)
    (CategoryStruct.comp (Y :=
      obj.{v₁, v, u₁, u}
        (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation K C) X) (mapCocone (obj (evaluation K C) X) c))) j)
      (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation K C) X) c)) j)
      (c.pt.map f ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι (obj (evaluation K C) Y) }))
    (CategoryStruct.comp (Y :=
      obj.{v₁, v, u₁, u}
        (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation K C) X) (mapCocone (obj (evaluation K C) X) c))) j)
      (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation K C) X) c)) j)
      ((t X).desc { pt := s.pt.obj X, ι := whiskerRight s.ι (obj (evaluation K C) X) } ≫ s.pt.map f))
have rw : CategoryStruct.comp (Y :=
    obj.{v₁, v, u₁, u}
      (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation K C) X) (mapCocone (obj (evaluation K C) X) c))) j)
    (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation K C) X) c)) j)
    (c.pt.map f ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι (obj (evaluation K C) Y) }) =
  { pt := s.pt.obj X, ι := whiskerRight s.ι (obj (evaluation K C) X) : Cocone (F ⋙ obj (evaluation K C) X) }.ι.app j ≫
    s.pt.map f
Tactic: rw [(t X).fac_assoc _ j]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
c : Cocone F
t : (k : K) → IsColimit (F := F ⋙ obj (evaluation K C) k) (mapCocone (obj (evaluation K C) k) c)
s : Cocone F
X Y : K
f : X ⟶ Y
j : J
⊢ CategoryStruct.comp (Y :=
      obj.{v₁, v, u₁, u}
        (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation K C) X) (mapCocone (obj (evaluation K C) X) c))) j)
      (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation K C) X) c)) j)
      (c.pt.map f ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι (obj (evaluation K C) Y) }) =
    { pt := s.pt.obj X, ι := whiskerRight s.ι (obj (evaluation K C) X) : Cocone (F ⋙ obj (evaluation K C) X) }.ι.app j ≫
      s.pt.map f
have erw : (F.obj j).map f ≫ (c.ι.app j).app Y ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι (obj (evaluation K C) Y) } =
  { pt := s.pt.obj X, ι := whiskerRight s.ι (obj (evaluation K C) X) : Cocone (F ⋙ obj (evaluation K C) X) }.ι.app j ≫
    s.pt.map f
Tactic: erw [← (c.ι.app j).naturality_assoc f]