awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
apply :
  ∀ (j : WalkingMultispan (multispanShapeCoend.{v_2, u_1} J)),
    (ChosenCoendsOfShape.cowedge F).ι.app j ≫ f = (ChosenCoendsOfShape.cowedge F).ι.app j ≫ g
⊢ f = g

Tactic:
apply (ChosenCoendsOfShape.isCoend F).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.ChosenCoendsOfShape.isCoend
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend.{v_2, u_1} J).L
⊢ Eq (α := (multispanIndexCoend F).multispan.obj (WalkingMultispan.left a) ⟶ X)
    ((ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ f)
    ((ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.left a) ≫ g)

Tactic:
simpa using _ ≫= h _
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend.{v_2, u_1} J).R
⊢ Eq (α := (multispanIndexCoend F).multispan.obj (WalkingMultispan.right a) ⟶ X)
    ((ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ f)
    ((ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ g)

Tactic:
h _

Premises used: CategoryTheory.Limits.chosenCoend.ι, CategoryTheory.Limits.chosenCoend, CategoryTheory.Limits.Multicofork.π
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J C
X : C
f g : chosenCoend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
a : (multispanShapeCoend.{v_2, u_1} J).R
⊢ Eq (α := (multispanIndexCoend F).multispan.obj (WalkingMultispan.right a) ⟶ X)
    ((ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ f)
    ((ChosenCoendsOfShape.cowedge F).ι.app (WalkingMultispan.right a) ≫ g)

Tactic:
exact h _
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J C
X : C
f : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j
j : J
⊢ CategoryStruct.comp (Y := chosenCoend F) (ι F j) (desc f hf) = f j

Tactic:
apply IsColimit.fac

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J C
X : C
f_1 : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f_1 i = (F.obj (op j)).map g ≫ f_1 j
G : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
f : F ⟶ G
j j' : J
φ : j ⟶ j'
⊢ Eq (α := (F.obj (op j')).obj j ⟶ chosenCoend G)
    ((F.map φ.op).app j ≫
      (fun (x : J) ↦ (NatTrans.app (f.app (op x)) x ≫ ι G x : (F.obj (op x)).obj x ⟶ chosenCoend G)) j)
    ((F.obj (op j')).map φ ≫
      (fun (x : J) ↦ (NatTrans.app (f.app (op x)) x ≫ ι G x : (F.obj (op x)).obj x ⟶ chosenCoend G)) j')

Tactic:
simp [chosenCoend.condition]

Premises used: CategoryTheory.Limits.chosenCoend.condition
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
inst_2 : ChosenCoendsOfShape.{v_2, u_1, v_1, u_2} J C
G : Jᵒᵖ ⥤ Functor.{v_2, v_1, u_1, u_2} J C
f : F ⟶ G
j : J
⊢ Eq (α := (F.obj (op j)).obj j ⟶ chosenCoend G) (ι F j ≫ map f) (NatTrans.app (f.app (op j)) j ≫ ι G j)

Tactic:
simp [chosenCoend.map]

Premises used: CategoryTheory.Limits.chosenCoend.map
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_3
C : Type u_4
inst : Category.{v_3, u_4} C
inst_1 : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
inst_2 : ChosenEndsOfShape.{v_4, u_3, v_3, u_4} J C
i j : J
f : i ⟶ j
⊢ Eq (α := chosenEnd F ⟶ (F.obj (op i)).obj j) (π F i ≫ (F.obj (op i)).map f) (π F j ≫ (F.map f.op).app j)

Tactic:
(ChosenEndsOfShape.wedge F).condition f

Premises used: CategoryTheory.Limits.chosenEnd.π, CategoryTheory.Limits.ChosenEndsOfShape.wedge, CategoryTheory.Limits.Wedge.condition, CategoryTheory.Limits.chosenEnd
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_3
C : Type u_4
inst : Category.{v_3, u_4} C
inst_1 : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
inst_2 : ChosenEndsOfShape.{v_4, u_3, v_3, u_4} J C
X : C
f g : X ⟶ chosenEnd F
h : ∀ (j : J), f ≫ π F j = g ≫ π F j
⊢ f = g

Tactic:
Wedge.IsLimit.hom_ext (ChosenEndsOfShape.isEnd F) h

Premises used: CategoryTheory.Limits.Wedge.IsLimit.hom_ext, CategoryTheory.Limits.ChosenEndsOfShape.isEnd, CategoryTheory.Limits.chosenEnd
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_3
C : Type u_4
inst : Category.{v_3, u_4} C
inst_1 : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
inst_2 : ChosenEndsOfShape.{v_4, u_3, v_3, u_4} J C
X : C
f : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
j : J
⊢ CategoryStruct.comp (Y := chosenEnd F) (lift f hf) (π F j) = f j

Tactic:
apply IsLimit.fac

Premises used: CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
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'
⊢ (F.obj (op j)).map φ ≫ NatTrans.app (f.app (op j)) j' = NatTrans.app (f.app (op j)) j ≫ (G.obj (op j)).map φ

Tactic:
have e := (f.app (op j)).naturality φ
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
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 φ
simp :
  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')
⊢ Eq (α := chosenEnd F ⟶ (G.obj (op j)).obj j')
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : chosenEnd F ⟶ (G.obj (op x)).obj x)) j ≫
      (G.obj (op j)).map φ)
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : chosenEnd F ⟶ (G.obj (op x)).obj x)) j' ≫
      (G.map φ.op).app j')

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
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 φ
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')
⊢ 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')

Tactic:
rw [← e, reassoc_of% chosenEnd.condition F φ]

Premises used: CategoryTheory.Limits.chosenEnd.condition
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
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' ≫ (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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Chosen.End
Goal:
J : Type u_3
C : Type u_4
inst : Category.{v_3, u_4} C
inst_1 : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
inst_2 : ChosenEndsOfShape.{v_4, u_3, v_3, u_4} J C
G : Jᵒᵖ ⥤ Functor.{v_4, v_3, u_3, u_4} J C
f : F ⟶ G
j : J
⊢ Eq (α := chosenEnd F ⟶ (G.obj (op j)).obj j) (map f ≫ π G j) (π F j ≫ NatTrans.app (f.app (op j)) j)

Tactic:
simp [chosenEnd.map]

Premises used: CategoryTheory.Limits.chosenEnd.map
-- Module: Mathlib.CategoryTheory.Limits.ColimitLimit
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
j : J
k k' : K
f : k ⟶ k'
⊢ F.map (𝟙 j ×ₘ f) = ((obj curry F).obj j).map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ColimitLimit
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
j j' : J
f : j ⟶ j'
k : K
⊢ F.map (f ×ₘ 𝟙 k) = ((obj curry (swap K J ⋙ F)).obj k).map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.ColimitLimit
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'
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)
⊢ 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))

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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.curry_obj_obj_obj, CategoryTheory.Limits.lim_map, CategoryTheory.Limits.limMap_π_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.lim_obj, CategoryTheory.Limits.colimit.cocone_x, CategoryTheory.Prod.swap_obj, CategoryTheory.Functor.curry_obj_map_app, CategoryTheory.Prod.swap_map, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.ColimitLimit
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)
rw₁ 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)
⊢ 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:
rw [map_id_left_eq_curry_map, colimit.w]

Premises used: CategoryTheory.Limits.map_id_left_eq_curry_map, CategoryTheory.Limits.colimit.w
-- Module: Mathlib.CategoryTheory.Limits.ColimitLimit
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'
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 := ⋯ } :
                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 := ⋯ } :
                  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)) :
      colimit (obj curry (swap K J ⋙ F) ⋙ lim) ⟶ colimit ((obj curry F).obj 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)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.ColimitLimit
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)
w₁ 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)
⊢ 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:
rw [map_id_right_eq_curry_swap_map, limit.w_assoc]

Premises used: CategoryTheory.Limits.map_id_right_eq_curry_swap_map, CategoryTheory.Limits.limit.w_assoc
-- Module: Mathlib.CategoryTheory.Limits.ColimitLimit
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
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 := ⋯ } :
                          NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) },
                naturality := ⋯ } })
        (limit.π (obj curry F ⋙ colim) j)))
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) 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

Tactic:
dsimp [colimitLimitToLimitColimit]

Premises used: CategoryTheory.Limits.colimitLimitToLimitColimit
-- Module: Mathlib.CategoryTheory.Limits.ColimitLimit
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
⊢ 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 := ⋯ } :
                          NatTrans (obj curry (swap K J ⋙ F) ⋙ lim) (obj (const K) (colimit ((obj curry F).obj j)))) },
                naturality := ⋯ } })
        (limit.π (obj curry F ⋙ colim) j)))
    (limit.π ((obj curry (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((obj curry F).obj j) k)

Tactic:
simp