awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
G : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_5 : HasLimit G
j : J
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))
⊢ 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)

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
G : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_5 : HasLimit G
j : J
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))
⊢ 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:
ext1 k
-- 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
G : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_5 : HasLimit G
j : J
k : K
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))
⊢ 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:
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]

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.curry_obj_obj_obj, CategoryTheory.Limits.limitIsoSwapCompLim_hom_app, CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Limits.limMap_π_assoc, CategoryTheory.Limits.colim_map, CategoryTheory.Functor.uncurry_obj_obj, CategoryTheory.Limits.lim_obj, CategoryTheory.Limits.colim_obj, CategoryTheory.Functor.flipIsoCurrySwapUncurry_hom_app_app, CategoryTheory.Functor.currying_unitIso_inv_app_app_app, CategoryTheory.Functor.flip_obj_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Prod.swap_obj, CategoryTheory.Limits.ι_colimitLimitToLimitColimit_π_assoc, CategoryTheory.Category.id_comp
-- 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
G : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_5 : HasLimit G
j : J
k : K
⊢ 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 [← comp_evaluation G k, limitObjIsoLimitCompEvaluation_hom_π_assoc]

Premises used: CategoryTheory.comp_evaluation, CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_hom_π_assoc
-- Module: Mathlib.CategoryTheory.Limits.Comma
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
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)
⊢ (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

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comma.limitAuxiliaryCone_π_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.mapCone_π_app, CategoryTheory.Comma.coneOfPreserves_pt_hom, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 (((fst L R).mapCone s).π.app j) ≫ (F.obj j).hom = s.pt.hom ≫ R.map (((snd L R).mapCone s).π.app j)

Tactic:
(s.π.app j).w

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.CommaMorphism.w, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 (((fst L R).mapCone s).π.app j) ≫ (F.obj j).hom = s.pt.hom ≫ R.map (((snd L R).mapCone s).π.app j)

Tactic:
exact (s.π.app j).w

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.CommaMorphism.w, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 := ⋯ }
right :
  m.right =
    CommaMorphism.right { 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 := ⋯ }

Tactic:
apply CommaMorphism.ext

Premises used: CategoryTheory.CommaMorphism.ext
-- Module: Mathlib.CategoryTheory.Limits.Comma
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
j : J
⊢ m.left ≫ c₁.π.app j = ((fst L R).mapCone s).π.app j

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 = CommaMorphism.left { left := t₁.lift ((fst L R).mapCone s), right := t₂.lift ((snd L R).mapCone s), w := ⋯ }

Tactic:
exact t₁.uniq ((fst L R).mapCone s) _ (fun j => by simp [← w])

Premises used: CategoryTheory.Comma.fst, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.mapCone
-- Module: Mathlib.CategoryTheory.Limits.Comma
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
j : J
⊢ m.right ≫ c₂.π.app j = ((snd L R).mapCone s).π.app j

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.Limits.Comma
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.right =
    CommaMorphism.right { left := t₁.lift ((fst L R).mapCone s), right := t₂.lift ((snd L R).mapCone s), w := ⋯ }

Tactic:
exact t₂.uniq ((snd L R).mapCone s) _ (fun j => by simp [← w])

Premises used: CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.mapCone, CategoryTheory.Comma.snd
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
h₁ :
  Eq (α :=
    (F.obj j₁).left ⟶
      left.{v₁, v₂, v₃, u₁, u₂, u₃} (T := T) (L := L) (R := R)
        (obj
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
          j₂))
    (CommaMorphism.left (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }))
    (CommaMorphism.left
      ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        Functor.map
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
              Comma L R })
          t))
h₂ :
  Eq (α :=
    (F.obj j₁).right ⟶
      right.{v₁, v₂, v₃, u₁, u₂, u₃} (T := T) (L := L) (R := R)
        (obj
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
          j₂))
    (CommaMorphism.right (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }))
    (CommaMorphism.right
      ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        Functor.map
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
              Comma L R })
          t))
⊢ Eq (α :=
    F.obj j₁ ⟶
      obj
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
        j₂)
    (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ })
    ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
      Functor.map
        (obj (const J)
          { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
            Comma L R })
        t)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ Eq (α :=
    (F.obj j₁).left ⟶
      left.{v₁, v₂, v₃, u₁, u₂, u₃} (T := T) (L := L) (R := R)
        (obj
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
          j₂))
    (CommaMorphism.left (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }))
    (CommaMorphism.left
      ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        Functor.map
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
              Comma L R })
          t))

Tactic:
simp [← c₁.w t]

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ Eq (α :=
    (F.obj j₁).right ⟶
      right.{v₁, v₂, v₃, u₁, u₂, u₃} (T := T) (L := L) (R := R)
        (obj
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) })
          j₂))
    (CommaMorphism.right (F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ }))
    (CommaMorphism.right
      ({ left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
        Functor.map
          (obj (const J)
            { left := c₁.pt, right := c₂.pt, hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) :
              Comma L R })
          t))

Tactic:
simp [← c₂.w t]

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
j : J
rw : L.map (((fst L R).mapCocone s).ι.app j) ≫ s.pt.hom = (F.obj j).hom ≫ R.map (((snd L R).mapCocone s).ι.app j)
⊢ Eq (α := ((F ⋙ fst L R) ⋙ L).obj j ⟶ R.obj s.pt.right)
    ((L.mapCocone c₁).ι.app j ≫ L.map (t₁.desc ((fst L R).mapCocone s)) ≫ s.pt.hom :
      ((F ⋙ fst L R) ⋙ L).obj j ⟶ R.obj s.pt.right)
    ((L.mapCocone c₁).ι.app j ≫ (coconeOfPreserves F t₁ c₂).pt.hom ≫ R.map (t₂.desc ((snd L R).mapCocone s)) :
      ((F ⋙ fst L R) ⋙ L).obj j ⟶ R.obj s.pt.right)

Tactic:
rw [coconeOfPreserves_pt_hom, (isColimitOfPreserves L t₁).fac_assoc,
            colimitAuxiliaryCocone_ι_app, assoc, ← R.map_comp, t₂.fac, L.mapCocone_ι_app, ←
            L.map_comp_assoc, t₁.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Functor.mapCocone_ι_app, CategoryTheory.Comma.coconeOfPreserves_pt_hom, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.IsColimit.fac_assoc, CategoryTheory.Comma.colimitAuxiliaryCocone_ι_app, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
j : J
⊢ L.map (((fst L R).mapCocone s).ι.app j) ≫ s.pt.hom = (F.obj j).hom ≫ R.map (((snd L R).mapCocone s).ι.app j)

Tactic:
(s.ι.app j).w

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
j : J
⊢ L.map (((fst L R).mapCocone s).ι.app j) ≫ s.pt.hom = (F.obj j).hom ≫ R.map (((snd L R).mapCocone s).ι.app j)

Tactic:
exact (s.ι.app j).w

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfPreserves F t₁ c₂).ι.app j ≫ m = s.ι.app j
left :
  m.left =
    CommaMorphism.left { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := ⋯ }
right :
  m.right =
    CommaMorphism.right { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := ⋯ }
⊢ m = { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := ⋯ }

Tactic:
apply CommaMorphism.ext

Premises used: CategoryTheory.CommaMorphism.ext
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfPreserves F t₁ c₂).ι.app j ≫ m = s.ι.app j
j : J
⊢ c₁.ι.app j ≫ m.left = ((fst L R).mapCocone s).ι.app j

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.Limits.Comma
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 : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
t₂ : IsColimit c₂
s : Cocone F
m : (coconeOfPreserves F t₁ c₂).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfPreserves F t₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ m.left =
    CommaMorphism.left { left := t₁.desc ((fst L R).mapCocone s), right := t₂.desc ((snd L R).mapCocone s), w := ⋯ }

Tactic:
exact t₁.uniq ((fst L R).mapCocone s) _ (fun j => by simp [← w])

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Comma.fst, CategoryTheory.Limits.IsColimit.uniq