awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Chosen.End (goal)
Goal:
J_1 : Type u_1
C_1 : Type u_2
inst : Category.{v_1, u_2} C_1
inst_1 : Category.{v_2, u_1} J_1
F_1 : J_1ᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J_1 C_1
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J_1 C_1
X_1 : C_1
f_1 : (j : J_1) → (F_1.obj (op j)).obj j ⟶ X_1
hf_1 : ∀ ⦃i j : J_1⦄ (g : i ⟶ j), (F_1.map g.op).app i ≫ f_1 i = (F_1.obj (op j)).map g ≫ f_1 j
J : Type u_3
C : Type u_4
inst_3 : Category.{v_3, u_4} C
inst_4 : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
inst_5 : ChosenEndsOfShape.{v_4, u_3, v_3, u_4} J C
X : C
f_2 : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f_2 i ≫ (F.obj (op i)).map g = f_2 j ≫ (F.map g.op).app j
G : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ NatTrans.app (f.app (op j)) j' = NatTrans.app (f.app (op j)) j ≫ (G.obj (op j)).map φ
⊢ Eq (α := chosenEnd F ⟶ (G.obj (op j)).obj j') (π F j ≫ NatTrans.app (f.app (op j)) j ≫ (G.obj (op j)).map φ)
    (π F j' ≫ NatTrans.app (f.app (op j')) j' ≫ (G.map φ.op).app j')
have rw : Eq (α := chosenEnd F ⟶ (G.obj (op j)).obj j') (π F j' ≫ (F.map φ.op).app j' ≫ NatTrans.app (f.app (op j)) j')
  (π F j' ≫ NatTrans.app (f.app (op j')) j' ≫ (G.map φ.op).app j')
Tactic: rw [← e, reassoc_of% chosenEnd.condition F φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
j : J
k k' : K
f : k ⟶ k'
⊢ Eq (α :=
    (obj curry (swap K J ⋙ F) ⋙ lim).obj k ⟶
      obj.{v₂, v, u₂, u} (obj (const K) (colimit.cocone ((obj curry F).obj j)).1) k')
    ((obj curry (swap K J ⋙ F) ⋙ lim).map f ≫
      limit.π ((obj curry (swap K J ⋙ F)).obj k') j ≫ colimit.ι ((obj curry F).obj j) k')
    (CategoryStruct.comp (Y := obj.{v₂, v, u₂, u} (obj (const K) (colimit.cocone ((obj curry F).obj j)).1) k)
      (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)
      (Functor.map (obj (const K) (colimit.cocone ((obj curry F).obj j)).1) f))
have simp : Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j))
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ F.map (𝟙 j ×ₘ f) ≫ colimit.ι ((obj curry F).obj j) k')
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)
Tactic: simp only [Functor.comp_obj, lim_obj, colimit.cocone_x,
                        Functor.const_obj_obj, Functor.comp_map, lim_map,
                        curry_obj_obj_obj, Prod.swap_obj, limMap_π_assoc, curry_obj_map_app,
                        Prod.swap_map, Functor.const_obj_map, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
j : J
k k' : K
f : k ⟶ k'
⊢ Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j))
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ F.map (𝟙 j ×ₘ f) ≫ colimit.ι ((obj curry F).obj j) k')
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)
have rw : Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j))
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ ((obj curry F).obj j).map f ≫ colimit.ι ((obj curry F).obj j) k')
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)
Tactic: rw [map_id_left_eq_curry_map, colimit.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
j : J
k k' : K
f : k ⟶ k'
rw :
  Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j))
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ ((obj curry F).obj j).map f ≫ colimit.ι ((obj curry F).obj j) k')
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)
⊢ Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j))
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ F.map (𝟙 j ×ₘ f) ≫ colimit.ι ((obj curry F).obj j) k')
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)
have rw₁ : Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j))
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)
Tactic: rw [map_id_left_eq_curry_map, colimit.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
j j' : J
f : j ⟶ j'
⊢ Eq.{v + 1} (α :=
    obj.{v₁, v, u₁, u} (obj (const J) (colimit.cocone (obj curry (swap K J ⋙ F) ⋙ lim)).1) j ⟶
      (obj curry F ⋙ colim).obj j')
    (Functor.map (obj (const J) (colimit.cocone (obj curry (swap K J ⋙ F) ⋙ lim)).1) f ≫
      colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
        { pt := (colimit.cocone ((obj curry F).obj j')).1,
          ι :=
            ({ app := fun (k : K) ↦ limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k,
                naturality := ⋯ } :
              NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit.cocone ((obj curry F).obj j')).1)) })
    (colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
        { pt := (colimit.cocone ((obj curry F).obj j)).1,
          ι :=
            ({ app := fun (k : K) ↦ limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                naturality := ⋯ } :
              NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit.cocone ((obj curry F).obj j)).1)) } ≫
      (obj curry F ⋙ colim).map f)
have dsimp : Eq (α := colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶ colimit ((obj curry F).obj j'))
  (𝟙 (colimit (obj curry (swap K J ⋙ F) ⋙ lim)) ≫
      colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
        { pt := colimit ((obj curry F).obj j'),
          ι :=
            ({ app := fun (k : K) ↦ limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k,
                naturality := sorry } :
              NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j')))) } :
    colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶ colimit ((obj curry F).obj j'))
  (CategoryStruct.comp (Y := colimit ((obj curry F).obj j))
      (colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
          { pt := colimit ((obj curry F).obj j),
            ι :=
              ({ app := fun (k : K) ↦ limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                  naturality := sorry } :
                NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) } :
        colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶
          Cocone.pt (F := obj curry (swap K J ⋙ F) ⋙ lim)
            { pt := colimit ((obj curry F).obj j),
              ι :=
                ({
                    app := fun (k : K) ↦
                      limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                    naturality := sorry } :
                  NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) })
      (colimMap ((obj curry F).map f)) :
    colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶ colimit ((obj curry F).obj j'))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
j j' : J
f : j ⟶ j'
k : K
⊢ Eq (α := (obj curry (swap K J ⋙ F) ⋙ lim).obj k ⟶ colimit ((obj curry F).obj j'))
    (CategoryStruct.comp (Y := colimit (obj curry (swap K J ⋙ F) ⋙ lim)) (colimit.ι (obj curry (swap K J ⋙ F) ⋙ lim) k)
        (𝟙 (colimit (obj curry (swap K J ⋙ F) ⋙ lim)) ≫
          colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
            { pt := colimit ((obj curry F).obj j'),
              ι :=
                ({
                    app := fun (k : K) ↦
                      limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k,
                    naturality := ⋯ } :
                  NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j')))) }) :
      (obj curry (swap K J ⋙ F) ⋙ lim).obj k ⟶ colimit ((obj curry F).obj j'))
    (CategoryStruct.comp (Y := colimit (obj curry (swap K J ⋙ F) ⋙ lim)) (colimit.ι (obj curry (swap K J ⋙ F) ⋙ lim) k)
        (CategoryStruct.comp (Y := colimit ((obj curry F).obj j))
          (colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
              { pt := colimit ((obj curry F).obj j),
                ι :=
                  ({
                      app := fun (k : K) ↦
                        limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                      naturality := ⋯ } :
                    NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) } :
            colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶
              Cocone.pt (F := obj curry (swap K J ⋙ F) ⋙ lim)
                { pt := colimit ((obj curry F).obj j),
                  ι :=
                    ({
                        app := fun (k : K) ↦
                          limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                        naturality := ⋯ } :
                      NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) })
          (colimMap ((obj curry F).map f))) :
      (obj curry (swap K J ⋙ F) ⋙ lim).obj k ⟶ colimit ((obj curry F).obj j'))
have w : Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j'))
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k)
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ F.map (f ×ₘ 𝟙 k) ≫ colimit.ι ((obj curry F).obj j') k)
Tactic: simp only [Functor.comp_obj, lim_obj, Category.id_comp, colimit.ι_desc,
              colimit.ι_desc_assoc, Category.assoc, ι_colimMap,
              curry_obj_obj_obj, curry_obj_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
j j' : J
f : j ⟶ j'
k : K
⊢ Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j'))
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k)
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ F.map (f ×ₘ 𝟙 k) ≫ colimit.ι ((obj curry F).obj j') k)
have w : Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j'))
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k)
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫
    ((obj curry (swap K J ⋙ F)).obj k).map f ≫ colimit.ι ((obj curry F).obj j') k)
Tactic: rw [map_id_right_eq_curry_swap_map, limit.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
j j' : J
f : j ⟶ j'
k : K
w :
  Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j'))
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k)
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫
      ((obj curry (swap K J ⋙ F)).obj k).map f ≫ colimit.ι ((obj curry F).obj j') k)
⊢ Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j'))
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k)
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ F.map (f ×ₘ 𝟙 k) ≫ colimit.ι ((obj curry F).obj j') k)
have w₁ : Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j'))
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k)
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j' ≫ colimit.ι ((obj curry F).obj j') k)
Tactic: rw [map_id_right_eq_curry_swap_map, limit.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
j : J
k : K
⊢ colimit.ι (obj curry (swap K J ⋙ F) ⋙ lim) k ≫ colimitLimitToLimitColimit F ≫ limit.π (obj curry F ⋙ colim) j =
    limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k
have dsimp : Eq (α := limit ((obj curry (swap K J ⋙ F)).obj k) ⟶ colimit ((obj curry F).obj j))
  (CategoryStruct.comp (Y := colimit (obj curry (swap K J ⋙ F) ⋙ lim)) (colimit.ι (obj curry (swap K J ⋙ F) ⋙ lim) k)
    (CategoryStruct.comp (Y := limit (obj curry F ⋙ colim))
      (limit.lift (obj curry F ⋙ colim)
        { pt := colimit (obj curry (swap K J ⋙ F) ⋙ lim),
          π :=
            {
              app := fun (j : J) ↦
                colimit.desc (obj curry (swap K J ⋙ F) ⋙ lim)
                  { pt := colimit ((obj curry F).obj j),
                    ι :=
                      ({
                          app := fun (k : K) ↦
                            limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k,
                          naturality := sorry } :
                        NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) },
              naturality := sorry } })
      (limit.π (obj curry F ⋙ colim) j)))
  (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)
Tactic: dsimp [colimitLimitToLimitColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
G : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_5 : HasLimit G
j : J
⊢ Eq (α := Cone.pt (F := G ⋙ colim) (mapCone colim (limit.cone G)) ⟶ (G ⋙ colim).obj j)
    (CategoryStruct.comp (Y := obj colim (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
          (Functor.map colim (Iso.hom (limitIsoSwapCompLim G)) :
            obj colim (limit.cone G).pt ⟶ obj colim (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
          (CategoryStruct.comp (Y := limit (obj curry (obj uncurry G) ⋙ colim))
              (colimitLimitToLimitColimit (obj uncurry G))
              (Functor.map lim (whiskerRight (Iso.inv (Iso.app (Equivalence.unitIso currying) G)) colim)) :
            obj colim (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim) ⟶ (limit.cone (G ⋙ colim)).pt) ≫
        (limit.cone (G ⋙ colim)).π.app j :
      Cone.pt (F := G ⋙ colim) (mapCone colim (limit.cone G)) ⟶ (G ⋙ colim).obj j)
    (NatTrans.app (Cone.π (mapCone colim (limit.cone G))) j :
      obj.{v₁, v, u₁, u} (obj (const J) (Cone.pt (F := G ⋙ colim) (mapCone colim (limit.cone G)))) j ⟶
        (G ⋙ colim).obj j)
have dsimp : Eq (α := colimit (limit G) ⟶ colimit (G.obj j))
  (CategoryStruct.comp (Y := limit (G ⋙ colim))
      (CategoryStruct.comp (Y := colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
        (colimMap (Iso.hom (limitIsoSwapCompLim G)) :
          colimit (limit G) ⟶ colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
        (CategoryStruct.comp (Y := limit (obj curry (obj uncurry G) ⋙ colim))
            (colimitLimitToLimitColimit (obj uncurry G))
            (limMap (whiskerRight (NatTrans.app (Iso.inv (Equivalence.unitIso currying)) G) colim)) :
          colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim) ⟶ limit (G ⋙ colim)))
      (limit.π (G ⋙ colim) j) :
    colimit (limit G) ⟶ colimit (G.obj j))
  (colimMap (limit.π G j) : colimit (limit G) ⟶ colimit (G.obj j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
G : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_5 : HasLimit G
j : J
⊢ Eq (α := colimit (limit G) ⟶ colimit (G.obj j))
    (CategoryStruct.comp (Y := limit (G ⋙ colim))
        (CategoryStruct.comp (Y := colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
          (colimMap (Iso.hom (limitIsoSwapCompLim G)) :
            colimit (limit G) ⟶ colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
          (CategoryStruct.comp (Y := limit (obj curry (obj uncurry G) ⋙ colim))
              (colimitLimitToLimitColimit (obj uncurry G))
              (limMap (whiskerRight (NatTrans.app (Iso.inv (Equivalence.unitIso currying)) G) colim)) :
            colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim) ⟶ limit (G ⋙ colim)))
        (limit.π (G ⋙ colim) j) :
      colimit (limit G) ⟶ colimit (G.obj j))
    (colimMap (limit.π G j) : colimit (limit G) ⟶ colimit (G.obj j))
have w : ∀ (k : K),
  CategoryStruct.comp (Y := colimit (limit G)) (colimit.ι (limit G) k)
      (CategoryStruct.comp (Y := limit (G ⋙ colim))
        (CategoryStruct.comp (Y := colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
          (colimMap (Iso.hom (limitIsoSwapCompLim G)) :
            colimit (limit G) ⟶ colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
          (CategoryStruct.comp (Y := limit (obj curry (obj uncurry G) ⋙ colim))
              (colimitLimitToLimitColimit (obj uncurry G))
              (limMap (whiskerRight (NatTrans.app (Iso.inv (Equivalence.unitIso currying)) G) colim)) :
            colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim) ⟶ limit (G ⋙ colim)))
        (limit.π (G ⋙ colim) j)) =
    CategoryStruct.comp (Y := colimit (limit G)) (colimit.ι (limit G) k) (colimMap (limit.π G j))
Tactic: ext1 k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ColimitLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : Category.{v₁, u₁} J
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
G : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_5 : HasLimit G
j : J
k : K
⊢ CategoryStruct.comp (Y := colimit (limit G)) (colimit.ι (limit G) k)
      (CategoryStruct.comp (Y := limit (G ⋙ colim))
        (CategoryStruct.comp (Y := colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
          (colimMap (Iso.hom (limitIsoSwapCompLim G)) :
            colimit (limit G) ⟶ colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim))
          (CategoryStruct.comp (Y := limit (obj curry (obj uncurry G) ⋙ colim))
              (colimitLimitToLimitColimit (obj uncurry G))
              (limMap (whiskerRight (NatTrans.app (Iso.inv (Equivalence.unitIso currying)) G) colim)) :
            colimit (obj curry (swap K J ⋙ obj uncurry G) ⋙ lim) ⟶ limit (G ⋙ colim)))
        (limit.π (G ⋙ colim) j)) =
    CategoryStruct.comp (Y := colimit (limit G)) (colimit.ι (limit G) k) (colimMap (limit.π G j))
have w : Eq (α := (limit G).obj k ⟶ colimit (G.obj j))
  (CategoryStruct.comp (Y := limit (G.flip.obj k))
      (Iso.hom (limitObjIsoLimitCompEvaluation G k) : (limit G).obj k ⟶ limit (G.flip.obj k))
      (limit.π (G.flip.obj k) j ≫ colimit.ι (G.obj j) k : limit (G.flip.obj k) ⟶ colimit (G.obj j)) :
    (limit G).obj k ⟶ colimit (G.obj j))
  (NatTrans.app (limit.π G j) k ≫ colimit.ι (G.obj j) k : (limit G).obj k ⟶ colimit (G.obj j))
Tactic: simp only [Category.assoc, limMap_π, Functor.comp_obj, colim_obj, whiskerRight_app,
      colim_map, ι_colimMap_assoc, lim_obj, limitIsoSwapCompLim_hom_app,
      ι_colimitLimitToLimitColimit_π_assoc, curry_obj_obj_obj, Prod.swap_obj,
      uncurry_obj_obj, ι_colimMap, currying_unitIso_inv_app_app_app, Category.id_comp,
      limMap_π_assoc, Functor.flip_obj_obj, flipIsoCurrySwapUncurry_hom_app_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (goal)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
j : J
⊢ (L.map (t₁.lift ((fst L R).mapCone s)) ≫ (coneOfPreserves F c₁ t₂).pt.hom) ≫ (R.mapCone c₂).π.app j =
    (s.pt.hom ≫ R.map (t₂.lift ((snd L R).mapCone s))) ≫ (R.mapCone c₂).π.app j
have rw : L.map (((fst L R).mapCone s).π.app j) ≫ (F.obj j).hom = s.pt.hom ≫ R.map (((snd L R).mapCone s).π.app j)
Tactic: rw [coneOfPreserves_pt_hom, assoc, assoc, (isLimitOfPreserves R t₂).fac,
            limitAuxiliaryCone_π_app, ← L.map_comp_assoc, t₁.fac, R.mapCone_π_app,
            ← R.map_comp, t₂.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (goal)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
m : s.pt ⟶ (coneOfPreserves F c₁ t₂).pt
w : ∀ (j : J), m ≫ (coneOfPreserves F c₁ t₂).π.app j = s.π.app j
⊢ m = { left := t₁.lift ((fst L R).mapCone s), right := t₂.lift ((snd L R).mapCone s), w := ⋯ }
have left : m.left = CommaMorphism.left { left := t₁.lift ((fst L R).mapCone s), right := t₂.lift ((snd L R).mapCone s), w := sorry }
Tactic: apply CommaMorphism.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Comma (goal)
Goal:
J : Type w
inst : Category.{w', w} J
A : Type u₁
inst_1 : Category.{v₁, u₁} A
B : Type u₂
inst_2 : Category.{v₂, u₂} B
T : Type u₃
inst_3 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
F : J ⥤ Comma L R
inst_4 : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
t₁ : IsLimit c₁
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
s : Cone F
m : s.pt ⟶ (coneOfPreserves F c₁ t₂).pt
w : ∀ (j : J), m ≫ (coneOfPreserves F c₁ t₂).π.app j = s.π.app j
left :
  m.left = CommaMorphism.left { left := t₁.lift ((fst L R).mapCone s), right := t₂.lift ((snd L R).mapCone s), w := ⋯ }
⊢ m = { left := t₁.lift ((fst L R).mapCone s), right := t₂.lift ((snd L R).mapCone s), w := ⋯ }
have right : m.right = CommaMorphism.right { left := t₁.lift ((fst L R).mapCone s), right := t₂.lift ((snd L R).mapCone s), w := sorry }
Tactic: apply CommaMorphism.ext