awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : D ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v₁, v', u₁, u'} J D
H : ∀ (k : K), PreservesLimit G (F ⋙ obj (evaluation K C) k)
c : Cone G
hc : IsLimit c
X : K
this : PreservesLimit G (F ⋙ obj (evaluation K C) X)
⊢ IsLimit ((F ⋙ obj (evaluation K C) X).mapCone c)

Tactic:
exact isLimitOfPreserves _ hc

Premises used: CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K : Type u₂
inst_2 : Category.{v₂, u₂} K
F : D ⥤ Functor.{v₂, v, u₂, u} K C
J : Type u_1
inst_3 : Category.{v_1, u_1} J
h : ∀ (k : K), PreservesLimitsOfShape.{v_1, u_1, v', v, u', u} J (F ⋙ obj (evaluation K C) k)
⊢ PreservesLimitsOfShape J F

Tactic:
⟨fun {G} => preservesLimit_of_evaluation F G fun _ => PreservesLimitsOfShape.preservesLimit⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit, CategoryTheory.Limits.preservesLimit_of_evaluation, CategoryTheory.Limits.PreservesLimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K : Type u₂
inst_2 : Category.{v₂, u₂} K
F : D ⥤ Functor.{v₂, v, u₂, u} K C
h : ∀ (k : K), PreservesLimitsOfSize.{w', w, v', v, u', u} (F ⋙ obj (evaluation K C) k)
⊢ PreservesLimitsOfSize.{w', w, v', max u₂ v, u', max (max (max u u₂) v) v₂} F

Tactic:
⟨fun {L} _ =>
    preservesLimitsOfShape_of_evaluation F L fun _ => PreservesLimitsOfSize.preservesLimitsOfShape⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.mk, CategoryTheory.Limits.preservesLimitsOfShape_of_evaluation, CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
-- 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
⊢ PreservesLimitsOfSize.{w', w, v, max u' v, u, max (max (max u u') v) v'} (C := C) (D := Functor.{v', v, u', u} D C)
    (const D)

Tactic:
preservesLimits_of_evaluation _ fun _ =>
    preservesLimits_of_natIso <| Iso.symm <| constCompEvaluationObj _ _

Premises used: CategoryTheory.Functor.constCompEvaluationObj, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesLimits_of_evaluation, CategoryTheory.Limits.preservesLimits_of_natIso
-- 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 : D ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v₁, v', u₁, u'} J D
H : ∀ (k : K), PreservesColimit G (F ⋙ obj (evaluation K C) k)
c : Cocone G
hc : IsColimit c
t : (k : K) → IsColimit (F := (G ⋙ F) ⋙ obj (evaluation K C) k) (mapCocone (obj (evaluation K C) k) (F.mapCocone c))
⊢ IsColimit (F.mapCocone c)

Tactic:
apply evaluationJointlyReflectsColimits

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsColimits
-- 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 : D ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v₁, v', u₁, u'} J D
H : ∀ (k : K), PreservesColimit G (F ⋙ obj (evaluation K C) k)
c : Cocone G
hc : IsColimit c
X : K
⊢ PreservesColimit G (F ⋙ obj (evaluation K C) X)

Tactic:
haveI := H 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 : D ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v₁, v', u₁, u'} J D
H : ∀ (k : K), PreservesColimit G (F ⋙ obj (evaluation K C) k)
c : Cocone G
hc : IsColimit c
X : K
this : PreservesColimit G (F ⋙ obj (evaluation K C) X)
t : IsColimit ((F ⋙ obj (evaluation K C) X).mapCocone c)
⊢ IsColimit (F := (G ⋙ F) ⋙ obj (evaluation K C) X) (mapCocone (obj (evaluation K C) X) (F.mapCocone c))

Tactic:
change IsColimit ((F ⋙ (evaluation K C).obj X).mapCocone c)

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.comp, CategoryTheory.Limits.IsColimit, CategoryTheory.evaluation, 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 : D ⥤ Functor.{v₂, v, u₂, u} K C
G : Functor.{v₁, v', u₁, u'} J D
H : ∀ (k : K), PreservesColimit G (F ⋙ obj (evaluation K C) k)
c : Cocone G
hc : IsColimit c
X : K
this : PreservesColimit G (F ⋙ obj (evaluation K C) X)
⊢ IsColimit ((F ⋙ obj (evaluation K C) X).mapCocone c)

Tactic:
exact isColimitOfPreserves _ hc

Premises used: CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K : Type u₂
inst_2 : Category.{v₂, u₂} K
F : D ⥤ Functor.{v₂, v, u₂, u} K C
J : Type u_1
inst_3 : Category.{v_1, u_1} J
h : ∀ (k : K), PreservesColimitsOfShape.{v_1, u_1, v', v, u', u} J (F ⋙ obj (evaluation K C) k)
⊢ PreservesColimitsOfShape J F

Tactic:
⟨fun {G} => preservesColimit_of_evaluation F G fun _ => PreservesColimitsOfShape.preservesColimit⟩

Premises used: CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit, CategoryTheory.Limits.preservesColimit_of_evaluation, CategoryTheory.Limits.PreservesColimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K : Type u₂
inst_2 : Category.{v₂, u₂} K
F : D ⥤ Functor.{v₂, v, u₂, u} K C
h : ∀ (k : K), PreservesColimitsOfSize.{w', w, v', v, u', u} (F ⋙ obj (evaluation K C) k)
⊢ PreservesColimitsOfSize.{w', w, v', max u₂ v, u', max (max (max u u₂) v) v₂} F

Tactic:
⟨fun {L} _ =>
    preservesColimitsOfShape_of_evaluation F L fun _ =>
      PreservesColimitsOfSize.preservesColimitsOfShape⟩

Premises used: CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape, CategoryTheory.Limits.PreservesColimitsOfSize.mk, CategoryTheory.Limits.preservesColimitsOfShape_of_evaluation
-- 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
⊢ PreservesColimitsOfSize.{w', w, v, max u' v, u, max (max (max u u') v) v'} (C := C) (D := Functor.{v', v, u', u} D C)
    (const D)

Tactic:
preservesColimits_of_evaluation _ fun _ =>
    preservesColimits_of_natIso <| Iso.symm <| constCompEvaluationObj _ _

Premises used: CategoryTheory.Functor.constCompEvaluationObj, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesColimits_of_natIso, CategoryTheory.Limits.preservesColimits_of_evaluation
-- 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
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
w :
  ∀ (k : K),
    Eq (α :=
      (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
        (obj lim G).obj k)
      (NatTrans.app
        (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
          Iso.hom
            ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x))
              G))
        k)
      (NatTrans.app
        (Iso.hom
            ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x))
              F) ≫
          map lim η)
        k)
⊢ Eq (α := obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F ⟶ obj lim G)
    (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
      Iso.hom
        ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) G))
    (Iso.hom
        ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) F) ≫
      map lim η)

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
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
k : K
w :
  ∀ (j : J),
    Eq (α :=
      (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶ (G.obj j).obj k)
      (CategoryStruct.comp (Y := (limit G).obj k)
        (NatTrans.app
          (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
            Iso.hom
              ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x))
                G))
          k)
        (NatTrans.app (limit.π G j) k))
      (CategoryStruct.comp (Y := (limit G).obj k)
        (NatTrans.app
            (Iso.hom
                ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦
                    (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x))
                  F) ≫
              map lim η)
            k :
          (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
            (obj lim G).obj k)
        (NatTrans.app (limit.π G j) k))
⊢ Eq (α :=
    (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶ (obj lim G).obj k)
    (NatTrans.app
      (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
        Iso.hom
          ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) G))
      k)
    (NatTrans.app
      (Iso.hom
          ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x)) F) ≫
        map lim η)
      k)

Tactic:
apply limit_obj_ext

Premises used: CategoryTheory.Limits.limit_obj_ext
-- 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
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
k : K
j : J
⊢ Eq (α :=
    (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶ (G.obj j).obj k)
    (CategoryStruct.comp (Y := (limit G).obj k)
      (NatTrans.app
        (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
          Iso.hom
            ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x))
              G))
        k)
      (NatTrans.app (limit.π G j) k))
    (CategoryStruct.comp (Y := (limit G).obj k)
      (NatTrans.app
          (Iso.hom
              ((fun (x : J ⥤ Functor.{v₂, v, u₂, u} K C) ↦ (Iso.symm (limitIsoFlipCompLim x) : x.flip ⋙ lim ≅ limit x))
                F) ≫
            map lim η)
          k :
        (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
          (obj lim G).obj k)
      (NatTrans.app (limit.π G j) k))

Tactic:
simp [comp_evaluation, ← NatTrans.comp_app (limMap η)]

Premises used: CategoryTheory.comp_evaluation, CategoryTheory.Limits.limMap, CategoryTheory.NatTrans.comp_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
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : K ⥤ Functor.{v₁, v, u₁, u} J C
η : F ⟶ G
w :
  ∀ (k : K),
    Eq (α :=
      (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
        (obj (flipFunctor K J C ⋙ lim) G).obj k)
      (NatTrans.app
        (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
          Iso.hom
            ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip))
              G))
        k)
      (NatTrans.app
        (Iso.hom
            ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip))
              F) ≫
          map (flipFunctor K J C ⋙ lim) η)
        k)
⊢ Eq (α := obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F ⟶ obj (flipFunctor K J C ⋙ lim) G)
    (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
      Iso.hom
        ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) G))
    (Iso.hom
        ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) F) ≫
      map (flipFunctor K J C ⋙ lim) η)

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
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : K ⥤ Functor.{v₁, v, u₁, u} J C
η : F ⟶ G
k : K
w :
  ∀ (j : J),
    Eq (α :=
      (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
        ((obj (flipFunctor K J C) G).obj j).obj k)
      (CategoryStruct.comp (Y := (limit (obj (flipFunctor K J C) G)).obj k)
        (NatTrans.app
          (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
            Iso.hom
              ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip))
                G))
          k)
        (NatTrans.app (limit.π (obj (flipFunctor K J C) G) j) k))
      (CategoryStruct.comp (Y := (limit (obj (flipFunctor K J C) G)).obj k)
        (NatTrans.app
            (Iso.hom
                ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦
                    (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip))
                  F) ≫
              map (flipFunctor K J C ⋙ lim) η)
            k :
          (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
            (obj (flipFunctor K J C ⋙ lim) G).obj k)
        (NatTrans.app (limit.π (obj (flipFunctor K J C) G) j) k))
⊢ Eq (α :=
    (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
      (obj (flipFunctor K J C ⋙ lim) G).obj k)
    (NatTrans.app
      (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
        Iso.hom
          ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) G))
      k)
    (NatTrans.app
      (Iso.hom
          ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) F) ≫
        map (flipFunctor K J C ⋙ lim) η)
      k)

Tactic:
apply limit_obj_ext

Premises used: CategoryTheory.Limits.limit_obj_ext
-- 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
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : K ⥤ Functor.{v₁, v, u₁, u} J C
η : F ⟶ G
k : K
j : J
⊢ Eq (α :=
    (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
      ((obj (flipFunctor K J C) G).obj j).obj k)
    (CategoryStruct.comp (Y := (limit (obj (flipFunctor K J C) G)).obj k)
      (NatTrans.app
        (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
          Iso.hom
            ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip))
              G))
        k)
      (NatTrans.app (limit.π (obj (flipFunctor K J C) G) j) k))
    (CategoryStruct.comp (Y := (limit (obj (flipFunctor K J C) G)).obj k)
      (NatTrans.app
          (Iso.hom
              ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip))
                F) ≫
            map (flipFunctor K J C ⋙ lim) η)
          k :
        (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
          (obj (flipFunctor K J C ⋙ lim) G).obj k)
      (NatTrans.app (limit.π (obj (flipFunctor K J C) G) j) k))

Tactic:
simp [comp_evaluation, ← NatTrans.comp_app (limMap _)]

Premises used: CategoryTheory.comp_evaluation, CategoryTheory.Limits.limMap, CategoryTheory.NatTrans.comp_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
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
w :
  ∀ (k : K),
    Eq (α :=
      (obj colim F).obj k ⟶
        (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
      (NatTrans.app (map colim η ≫ Iso.hom (colimitIsoFlipCompColim G)) k)
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
          (Iso.hom (colimitIsoFlipCompColim F))
          (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
        k)
⊢ Eq (α := obj colim F ⟶ obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G)
    (map colim η ≫ Iso.hom (colimitIsoFlipCompColim G))
    (CategoryStruct.comp (Y := obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
      (Iso.hom (colimitIsoFlipCompColim F))
      (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))

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
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
k : K
w :
  ∀ (j : J),
    Eq (α :=
      (F.obj j).obj k ⟶
        (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
      (CategoryStruct.comp (Y := (colimit F).obj k) (NatTrans.app (colimit.ι F j) k)
        (NatTrans.app (map colim η ≫ Iso.hom (colimitIsoFlipCompColim G)) k))
      (CategoryStruct.comp (Y := (colimit F).obj k)
        (NatTrans.app (colimit.ι F j) k : (F.obj j).obj k ⟶ (colimit F).obj k)
        (NatTrans.app
            (CategoryStruct.comp (Y :=
              obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
              (Iso.hom (colimitIsoFlipCompColim F))
              (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
            k :
          (obj colim F).obj k ⟶
            (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k))
⊢ Eq (α :=
    (obj colim F).obj k ⟶
      (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
    (NatTrans.app (map colim η ≫ Iso.hom (colimitIsoFlipCompColim G)) k)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
        (Iso.hom (colimitIsoFlipCompColim F))
        (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
      k)

Tactic:
apply colimit_obj_ext

Premises used: CategoryTheory.Limits.colimit_obj_ext
-- 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
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
k : K
j : J
⊢ Eq (α :=
    (F.obj j).obj k ⟶ (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
    (CategoryStruct.comp (Y := (colimit F).obj k) (NatTrans.app (colimit.ι F j) k)
      (NatTrans.app (map colim η ≫ Iso.hom (colimitIsoFlipCompColim G)) k))
    (CategoryStruct.comp (Y := (colimit F).obj k) (NatTrans.app (colimit.ι F j) k : (F.obj j).obj k ⟶ (colimit F).obj k)
      (NatTrans.app
          (CategoryStruct.comp (Y :=
            obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
            (Iso.hom (colimitIsoFlipCompColim F))
            (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
          k :
        (obj colim F).obj k ⟶
          (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k))

Tactic:
simp [comp_evaluation, ← NatTrans.comp_app_assoc _ (colimMap η)]

Premises used: CategoryTheory.comp_evaluation, CategoryTheory.NatTrans.comp_app_assoc, CategoryTheory.Limits.colimMap
-- 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
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F G : K ⥤ Functor.{v₁, v, u₁, u} J C
η : F ⟶ G
w :
  ∀ (k : K),
    Eq (α :=
      (obj (flipFunctor K J C ⋙ colim) F).obj k ⟶
        (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
      (NatTrans.app (map (flipFunctor K J C ⋙ colim) η ≫ Iso.hom (colimitFlipIsoCompColim G)) k)
      (NatTrans.app
        (CategoryStruct.comp (Y := obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
          (Iso.hom (colimitFlipIsoCompColim F)) (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
        k)
⊢ Eq (α := obj (flipFunctor K J C ⋙ colim) F ⟶ obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G)
    (map (flipFunctor K J C ⋙ colim) η ≫ Iso.hom (colimitFlipIsoCompColim G))
    (CategoryStruct.comp (Y := obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
      (Iso.hom (colimitFlipIsoCompColim F)) (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))

Tactic:
ext k