awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
H : J ⥤ Functor.{v₂, v, u₂, u} K C
inst_3 : HasColimit H
c : Cocone H
j : J
k : K
⊢ CategoryStruct.comp (Y := (colimit H).obj k) (NatTrans.app (ι H j) k) (NatTrans.app (desc H c) k) = (c.ι.app j).app k

Tactic:
congr_app (colimit.ι_desc c j) k

Premises used: CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
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)
⊢ 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))

Tactic:
rw [assoc, (t Y).fac _ j]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
⊢ 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:
simpa using
            ((t X).fac_assoc ⟨s.pt.obj X, whiskerRight s.π ((evaluation K C).obj X)⟩ j _).symm

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.Cone.pt, CategoryTheory.Functor.whiskerRight, CategoryTheory.Limits.IsLimit.fac_assoc, CategoryTheory.evaluation, Eq.symm, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
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 := ⋯ } ≫
          c.π.app j)
        k =
      (s.π.app j).app k
⊢ { 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

Tactic:
ext k
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
k : K
⊢ NatTrans.app
      ({ app := fun (k : K) ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π (obj (evaluation K C) k) },
          naturality := ⋯ } ≫
        c.π.app j)
      k =
    (s.π.app j).app k

Tactic:
(t k).fac _ j

Premises used: CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
k : K
⊢ NatTrans.app
      ({ app := fun (k : K) ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π (obj (evaluation K C) k) },
          naturality := ⋯ } ≫
        c.π.app j)
      k =
    (s.π.app j).app k

Tactic:
exact (t k).fac _ j

Premises used: CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
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 := ⋯ }
        x
⊢ m =
    { app := fun (k : K) ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π (obj (evaluation K C) k) },
      naturality := ⋯ }

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
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 := ⋯ }
      x

Tactic:
(t x).hom_ext fun j =>
      (congr_app (w j) x).trans
        ((t x).fac ⟨s.pt.obj _, whiskerRight s.π ((evaluation K C).obj _)⟩ j).symm

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.Cone.pt, CategoryTheory.Functor.whiskerRight, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.evaluation, Eq.symm, CategoryTheory.congr_app, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj, Eq.trans, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
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 := ⋯ }
      x

Tactic:
exact (t x).hom_ext fun j =>
      (congr_app (w j) x).trans
        ((t x).fac ⟨s.pt.obj _, whiskerRight s.π ((evaluation K C).obj _)⟩ j).symm

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.Cone.pt, CategoryTheory.Functor.whiskerRight, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.evaluation, Eq.symm, CategoryTheory.congr_app, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj, Eq.trans, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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 : (k : K) → LimitCone (F.flip.obj k)
k : K
j : J
⊢ (c k).isLimit.lift { pt := (c k).cone.pt, π := (c k).cone.π ≫ F.flip.map (𝟙 k) } ≫ (c k).cone.π.app j =
    𝟙 (c k).cone.pt ≫ (c k).cone.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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 : (k : K) → LimitCone (F.flip.obj k)
k₁ k₂ k₃ : K
f₁ : k₁ ⟶ k₂
f₂ : k₂ ⟶ k₃
j : J
⊢ Eq (α :=
    { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map (f₁ ≫ f₂) : Cone (F.flip.obj k₃) }.pt ⟶
      (F.flip.obj k₃).obj j)
    ((c k₃).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map (f₁ ≫ f₂) } ≫ (c k₃).cone.π.app j)
    (CategoryStruct.comp (Y := (c k₂).cone.pt)
        ((c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f₁ } :
          { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f₁ : Cone (F.flip.obj k₂) }.pt ⟶ (c k₂).cone.pt)
        ((c k₃).isLimit.lift { pt := (c k₂).cone.pt, π := (c k₂).cone.π ≫ F.flip.map f₂ } :
          { pt := (c k₂).cone.pt, π := (c k₂).cone.π ≫ F.flip.map f₂ : Cone (F.flip.obj k₃) }.pt ⟶ (c k₃).cone.pt) ≫
      (c k₃).cone.π.app j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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 : (k : K) → LimitCone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
k : K
⊢ (map
            (obj (const J)
              { obj := fun (k : K) ↦ (c k).cone.pt,
                map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                  (c k₂).isLimit.lift
                    { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
            g ≫
          { app := fun (k : K) ↦ (c k).cone.π.app j₂, naturality := ⋯ :
            NatTrans
              (obj
                (obj (const J)
                  { obj := fun (k : K) ↦ (c k).cone.pt,
                    map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                      (c k₂).isLimit.lift
                        { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                    map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
                j₂)
              (F.obj j₂) }).app
      k =
    NatTrans.app
      ({ app := fun (k : K) ↦ (c k).cone.π.app j₁, naturality := ⋯ :
          NatTrans
            (obj
              (obj (const J)
                { obj := fun (k : K) ↦ (c k).cone.pt,
                  map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                    (c k₂).isLimit.lift
                      { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                  map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
              j₁)
            (F.obj j₁) } ≫
        F.map g)
      k

Tactic:
(c k).cone.π.naturality g

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.LimitCone.cone
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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 : (k : K) → LimitCone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
k : K
⊢ (map
            (obj (const J)
              { obj := fun (k : K) ↦ (c k).cone.pt,
                map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                  (c k₂).isLimit.lift
                    { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
            g ≫
          { app := fun (k : K) ↦ (c k).cone.π.app j₂, naturality := ⋯ :
            NatTrans
              (obj
                (obj (const J)
                  { obj := fun (k : K) ↦ (c k).cone.pt,
                    map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                      (c k₂).isLimit.lift
                        { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                    map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
                j₂)
              (F.obj j₂) }).app
      k =
    NatTrans.app
      ({ app := fun (k : K) ↦ (c k).cone.π.app j₁, naturality := ⋯ :
          NatTrans
            (obj
              (obj (const J)
                { obj := fun (k : K) ↦ (c k).cone.pt,
                  map := fun {k₁ k₂ : K} (f : k₁ ⟶ k₂) ↦
                    (c k₂).isLimit.lift
                      { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f : Cone (F.flip.obj k₂) },
                  map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v, u₂, u} K C })
              j₁)
            (F.obj j₁) } ≫
        F.map g)
      k

Tactic:
exact (c k).cone.π.naturality g

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.LimitCone.cone
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
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
⊢ 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))

Tactic:
rw [(t X).fac_assoc _ j]

Premises used: CategoryTheory.Limits.IsColimit.fac_assoc
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
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
⊢ 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:
erw [← (c.ι.app j).naturality_assoc f]

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
erw :
  (F.obj j).map f ≫
      { pt := s.pt.obj Y, ι := whiskerRight s.ι (obj (evaluation K C) Y) : Cocone (F ⋙ obj (evaluation K C) Y) }.ι.app
        j =
    { 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
⊢ (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 [(t Y).fac ⟨s.pt.obj _, whiskerRight s.ι _⟩ j]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Functor.whiskerRight, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
⊢ (F.obj j).map f ≫
      { pt := s.pt.obj Y, ι := whiskerRight s.ι (obj (evaluation K C) Y) : Cocone (F ⋙ obj (evaluation K C) Y) }.ι.app
        j =
    { 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
j : J
w :
  ∀ (k : K),
    NatTrans.app
        (c.ι.app j ≫
          { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
            naturality := ⋯ })
        k =
      (s.ι.app j).app k
⊢ c.ι.app j ≫
      { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
        naturality := ⋯ } =
    s.ι.app j

Tactic:
ext k
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
j : J
k : K
⊢ NatTrans.app
      (c.ι.app j ≫
        { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
          naturality := ⋯ })
      k =
    (s.ι.app j).app k

Tactic:
(t k).fac _ j

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
j : J
k : K
⊢ NatTrans.app
      (c.ι.app j ≫
        { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
          naturality := ⋯ })
      k =
    (s.ι.app j).app k

Tactic:
exact (t k).fac _ j

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
m : c.pt ⟶ s.pt
w : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
w₁ :
  ∀ (x : K),
    m.app x =
      NatTrans.app
        { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
          naturality := ⋯ }
        x
⊢ m =
    { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
      naturality := ⋯ }

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
m : c.pt ⟶ s.pt
w : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : K
⊢ m.app x =
    NatTrans.app
      { app := fun (k : K) ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι (obj (evaluation K C) k) },
        naturality := ⋯ }
      x

Tactic:
(t x).hom_ext fun j =>
      (congr_app (w j) x).trans
        ((t x).fac ⟨s.pt.obj _, whiskerRight s.ι ((evaluation K C).obj _)⟩ j).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Functor.whiskerRight, CategoryTheory.Limits.Cocone.ι, CategoryTheory.evaluation, Eq.symm, CategoryTheory.congr_app, CategoryTheory.Functor.obj, Eq.trans, CategoryTheory.Limits.Cocone.pt