awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasLimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cone K
hc : IsLimit c
t :
  (k : C) →
    IsLimit (F := (K ⋙ obj (whiskeringLeft C E D) F) ⋙ obj (evaluation C D) k)
      (mapCone (obj (evaluation C D) k) (mapCone (obj (whiskeringLeft C E D) F) c))
⊢ IsLimit (F := K ⋙ obj (whiskeringLeft C E D) F) (mapCone (obj (whiskeringLeft C E D) F) c)

Tactic:
apply evaluationJointlyReflectsLimits

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsLimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasLimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cone K
hc : IsLimit c
Y : C
t : IsLimit (F := K ⋙ obj (evaluation E D) (F.obj Y)) (mapCone (obj (evaluation E D) (F.obj Y)) c)
⊢ IsLimit (F := (K ⋙ obj (whiskeringLeft C E D) F) ⋙ obj (evaluation C D) Y)
    (mapCone (obj (evaluation C D) Y) (mapCone (obj (whiskeringLeft C E D) F) c))

Tactic:
change IsLimit (((evaluation E D).obj (F.obj Y)).mapCone c)

Premises used: CategoryTheory.Limits.IsLimit, CategoryTheory.evaluation, CategoryTheory.Functor.mapCone, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasLimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cone K
hc : IsLimit c
Y : C
⊢ IsLimit (F := K ⋙ obj (evaluation E D) (F.obj Y)) (mapCone (obj (evaluation E D) (F.obj Y)) c)

Tactic:
exact isLimitOfPreserves _ hc

Premises used: CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cocone K
hc : IsColimit c
t :
  (k : C) →
    IsColimit (F := (K ⋙ obj (whiskeringLeft C E D) F) ⋙ obj (evaluation C D) k)
      (mapCocone (obj (evaluation C D) k) (mapCocone (obj (whiskeringLeft C E D) F) c))
⊢ IsColimit (F := K ⋙ obj (whiskeringLeft C E D) F) (mapCocone (obj (whiskeringLeft C E D) F) c)

Tactic:
apply evaluationJointlyReflectsColimits

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsColimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cocone K
hc : IsColimit c
Y : C
t : IsColimit (F := K ⋙ obj (evaluation E D) (F.obj Y)) (mapCocone (obj (evaluation E D) (F.obj Y)) c)
⊢ IsColimit (F := (K ⋙ obj (whiskeringLeft C E D) F) ⋙ obj (evaluation C D) Y)
    (mapCocone (obj (evaluation C D) Y) (mapCocone (obj (whiskeringLeft C E D) F) c))

Tactic:
change IsColimit (((evaluation E D).obj (F.obj Y)).mapCocone c)

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₂, u₂} J D
F : Functor.{v₁, v₃, u₁, u₃} C E
K : J ⥤ Functor.{v₃, v₂, u₃, u₂} E D
c : Cocone K
hc : IsColimit c
Y : C
⊢ IsColimit (F := K ⋙ obj (evaluation E D) (F.obj Y)) (mapCocone (obj (evaluation E D) (F.obj Y)) c)

Tactic:
exact isColimitOfPreserves _ hc

Premises used: CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasColimitsOfSize.{w, w', v₂, u₂} D
F : Functor.{v₁, v₃, u₁, u₃} C E
⊢ PreservesColimitsOfSize.{w, w', max u₃ v₂, max u₁ v₂, max (max (max u₂ u₃) v₂) v₃, max (max (max u₁ u₂) v₁) v₂} (C :=
    Functor.{v₃, v₂, u₃, u₂} E D) (obj (whiskeringLeft C E D) F)

Tactic:
⟨fun {J} _ => whiskeringLeft_preservesColimitsOfShape J F⟩

Premises used: CategoryTheory.Limits.PreservesColimitsOfSize.mk, CategoryTheory.whiskeringLeft_preservesColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit c
apply :
  (k : C) →
    IsLimit (F := (K ⋙ obj (whiskeringRight C D E) F) ⋙ obj (evaluation C E) k)
      (mapCone (obj (evaluation C E) k) (mapCone (obj (whiskeringRight C D E) F) c))
⊢ IsLimit (F := K ⋙ obj (whiskeringRight C D E) F) (mapCone (obj (whiskeringRight C D E) F) c)

Tactic:
apply evaluationJointlyReflectsLimits _ (fun k => ?_)

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsLimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit c
k : C
change : IsLimit (F := K ⋙ obj (evaluation C D) k ⋙ F) (mapCone (obj (evaluation C D) k ⋙ F) c)
⊢ IsLimit (F := (K ⋙ obj (whiskeringRight C D E) F) ⋙ obj (evaluation C E) k)
    (mapCone (obj (evaluation C E) k) (mapCone (obj (whiskeringRight C D E) F) c))

Tactic:
change IsLimit (((evaluation _ _).obj k ⋙ F).mapCone c)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.IsLimit, CategoryTheory.evaluation, CategoryTheory.Functor.mapCone, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit c
k : C
⊢ IsLimit (F := K ⋙ obj (evaluation C D) k ⋙ F) (mapCone (obj (evaluation C D) k ⋙ F) c)

Tactic:
exact isLimitOfPreserves _ hc

Premises used: CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : F.ReflectsIsomorphisms
inst_9 : PreservesLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
⊢ ReflectsLimitsOfShape (C := Functor.{v_1, v_2, u_1, u_2} C D) J (obj (whiskeringRight C D E) F)

Tactic:
reflectsLimitsOfShape_of_reflectsIsomorphisms

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_3, u_3} J E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : ReflectsLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit (F := K ⋙ obj (whiskeringRight C D E) F) (mapCone (obj (whiskeringRight C D E) F) c)
apply : (k : C) → IsLimit (F := K ⋙ obj (evaluation C D) k) (mapCone (obj (evaluation C D) k) c)
⊢ IsLimit c

Tactic:
apply evaluationJointlyReflectsLimits _ (fun k ↦ ?_)

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsLimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_3, u_3} J E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : ReflectsLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit (F := K ⋙ obj (whiskeringRight C D E) F) (mapCone (obj (whiskeringRight C D E) F) c)
k : C
t : IsLimit (F := (K ⋙ obj (evaluation C D) k) ⋙ F) (F.mapCone (mapCone (obj (evaluation C D) k) c))
⊢ IsLimit (F := K ⋙ obj (evaluation C D) k) (mapCone (obj (evaluation C D) k) c)

Tactic:
apply isLimitOfReflects F

Premises used: CategoryTheory.Limits.isLimitOfReflects
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasLimitsOfShape.{v_4, u_4, v_3, u_3} J E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : ReflectsLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cone K
hc : IsLimit (F := K ⋙ obj (whiskeringRight C D E) F) (mapCone (obj (whiskeringRight C D E) F) c)
k : C
⊢ IsLimit (F := (K ⋙ obj (evaluation C D) k) ⋙ F) (F.mapCone (mapCone (obj (evaluation C D) k) c))

Tactic:
exact isLimitOfPreserves ((evaluation C E).obj k) hc

Premises used: CategoryTheory.evaluation, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : Type u_4
inst_3 : Category.{v_4, u_4} J
inst_4 : HasLimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_5 : PreservesLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
G : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
j : J
⊢ Eq (α := limit G ⋙ F ⟶ (G ⋙ obj (whiskeringRight C D E) F).obj j)
    (CategoryStruct.comp (Y := limit (G ⋙ obj (whiskeringRight C D E) F))
        (Iso.inv (limitCompWhiskeringRightIsoLimitComp F G) : limit G ⋙ F ⟶ limit (G ⋙ obj (whiskeringRight C D E) F))
        (limit.π (G ⋙ obj (whiskeringRight C D E) F) j :
          limit (G ⋙ obj (whiskeringRight C D E) F) ⟶ (G ⋙ obj (whiskeringRight C D E) F).obj j) :
      limit G ⋙ F ⟶ (G ⋙ obj (whiskeringRight C D E) F).obj j)
    (whiskerRight (limit.π G j) F : limit G ⋙ F ⟶ G.obj j ⋙ F)

Tactic:
simp [limitCompWhiskeringRightIsoLimitComp]

Premises used: CategoryTheory.limitCompWhiskeringRightIsoLimitComp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : Type u_4
inst_3 : Category.{v_4, u_4} J
inst_4 : HasLimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_5 : PreservesLimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
G : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
j : J
⊢ Eq (α := limit (G ⋙ obj (whiskeringRight C D E) F) ⟶ G.obj j ⋙ F)
    (CategoryStruct.comp (Y := limit G ⋙ F)
        (Iso.hom (limitCompWhiskeringRightIsoLimitComp F G) : limit (G ⋙ obj (whiskeringRight C D E) F) ⟶ limit G ⋙ F)
        (whiskerRight (limit.π G j) F : limit G ⋙ F ⟶ G.obj j ⋙ F) :
      limit (G ⋙ obj (whiskeringRight C D E) F) ⟶ G.obj j ⋙ F)
    (limit.π (G ⋙ obj (whiskeringRight C D E) F) j :
      limit (G ⋙ obj (whiskeringRight C D E) F) ⟶ (G ⋙ obj (whiskeringRight C D E) F).obj j)

Tactic:
simp [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasColimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesColimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cocone K
hc : IsColimit c
apply :
  (k : C) →
    IsColimit (F := (K ⋙ obj (whiskeringRight C D E) F) ⋙ obj (evaluation C E) k)
      (mapCocone (obj (evaluation C E) k) (mapCocone (obj (whiskeringRight C D E) F) c))
⊢ IsColimit (F := K ⋙ obj (whiskeringRight C D E) F) (mapCocone (obj (whiskeringRight C D E) F) c)

Tactic:
apply evaluationJointlyReflectsColimits _ (fun k => ?_)

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsColimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasColimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesColimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cocone K
hc : IsColimit c
k : C
change : IsColimit (F := K ⋙ obj (evaluation C D) k ⋙ F) (mapCocone (obj (evaluation C D) k ⋙ F) c)
⊢ IsColimit (F := (K ⋙ obj (whiskeringRight C D E) F) ⋙ obj (evaluation C E) k)
    (mapCocone (obj (evaluation C E) k) (mapCocone (obj (whiskeringRight C D E) F) c))

Tactic:
change IsColimit (((evaluation _ _).obj k ⋙ F).mapCocone c)

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.comp, CategoryTheory.Limits.IsColimit, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
J : Type u_4
inst_6 : Category.{v_4, u_4} J
inst_7 : HasColimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : PreservesColimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
K : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
c : Cocone K
hc : IsColimit c
k : C
⊢ IsColimit (F := K ⋙ obj (evaluation C D) k ⋙ F) (mapCocone (obj (evaluation C D) k ⋙ F) c)

Tactic:
exact isColimitOfPreserves _ hc

Premises used: CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : Type u_4
inst_3 : Category.{v_4, u_4} J
inst_4 : HasColimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_5 : PreservesColimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
G : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
j : J
⊢ Eq (α := (G ⋙ obj (whiskeringRight C D E) F).obj j ⟶ colimit G ⋙ F)
    (CategoryStruct.comp (Y := colimit (G ⋙ obj (whiskeringRight C D E) F))
        (colimit.ι (G ⋙ obj (whiskeringRight C D E) F) j :
          (G ⋙ obj (whiskeringRight C D E) F).obj j ⟶ colimit (G ⋙ obj (whiskeringRight C D E) F))
        (Iso.hom (colimitCompWhiskeringRightIsoColimitComp F G) :
          colimit (G ⋙ obj (whiskeringRight C D E) F) ⟶ colimit G ⋙ F) :
      (G ⋙ obj (whiskeringRight C D E) F).obj j ⟶ colimit G ⋙ F)
    (whiskerRight (colimit.ι G j) F : G.obj j ⋙ F ⟶ colimit G ⋙ F)

Tactic:
simp [colimitCompWhiskeringRightIsoColimitComp]

Premises used: CategoryTheory.colimitCompWhiskeringRightIsoColimitComp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : Type u_4
inst_3 : Category.{v_4, u_4} J
inst_4 : HasColimitsOfShape.{v_4, u_4, v_2, u_2} J D
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_5 : PreservesColimitsOfShape.{v_4, u_4, v_2, v_3, u_2, u_3} J F
G : J ⥤ Functor.{v_1, v_2, u_1, u_2} C D
j : J
⊢ Eq (α := G.obj j ⋙ F ⟶ colimit (G ⋙ obj (whiskeringRight C D E) F))
    (CategoryStruct.comp (Y := colimit G ⋙ F) (whiskerRight (colimit.ι G j) F : G.obj j ⋙ F ⟶ colimit G ⋙ F)
        (Iso.inv (colimitCompWhiskeringRightIsoColimitComp F G) :
          colimit G ⋙ F ⟶ colimit (G ⋙ obj (whiskeringRight C D E) F)) :
      G.obj j ⋙ F ⟶ colimit (G ⋙ obj (whiskeringRight C D E) F))
    (colimit.ι (G ⋙ obj (whiskeringRight C D E) F) j :
      (G ⋙ obj (whiskeringRight C D E) F).obj j ⟶ colimit (G ⋙ obj (whiskeringRight C D E) F))

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_6 : HasLimitsOfSize.{w, w', v_2, u_2} D
inst_7 : PreservesLimitsOfSize.{w, w', v_2, v_3, u_2, u_3} F
⊢ PreservesLimitsOfSize.{w, w', max u_1 v_2, max u_1 v_3, max (max (max u_1 u_2) v_1) v_2,
      max (max (max u_1 u_3) v_1) v_3}
    (C := Functor.{v_1, v_2, u_1, u_2} C D) (obj (whiskeringRight C D E) F)

Tactic:
⟨inferInstance⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.mk, inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
E_1 : Type u₃
inst_2 : Category.{v₃, u₃} E_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
E : Type u_3
inst_5 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_6 : HasColimitsOfSize.{w, w', v_2, u_2} D
inst_7 : PreservesColimitsOfSize.{w, w', v_2, v_3, u_2, u_3} F
⊢ PreservesColimitsOfSize.{w, w', max u_1 v_2, max u_1 v_3, max (max (max u_1 u_2) v_1) v_2,
      max (max (max u_1 u_3) v_1) v_3}
    (C := Functor.{v_1, v_2, u_1, u_2} C D) (obj (whiskeringRight C D E) F)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
J : Type u
inst_2 : SmallCategory J
inst_3 : PreservesLimitsOfShape (C := Cᵒᵖ ⥤ Type u) J F.op.lan
⊢ PreservesLimitsOfShape J F

Tactic:
letI := preservesLimitsOfShape_of_natIso (J := J)
    (Presheaf.compULiftYonedaIsoULiftYonedaCompLan.{u} F).symm
  preservesLimitsOfShape_of_reflects_of_preserves F uliftYoneda.{u}

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves, CategoryTheory.uliftYoneda
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : C ⥤ Functor.{v_1, v_2, u_1, u_2} D E
h : ∀ (d : D), PreservesFiniteLimits (F ⋙ obj (evaluation D E) d)
⊢ PreservesFiniteLimits F

Tactic:
⟨fun J _ _ => preservesLimitsOfShape_of_evaluation F J fun k => (h k).preservesFiniteLimits _⟩

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_evaluation, CategoryTheory.Limits.PreservesFiniteLimits.mk, CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
E : Type u_2
inst_2 : Category.{v_2, u_2} E
F : C ⥤ Functor.{v_1, v_2, u_1, u_2} D E
h : ∀ (d : D), PreservesFiniteColimits (F ⋙ obj (evaluation D E) d)
⊢ PreservesFiniteColimits F

Tactic:
⟨fun J _ _ => preservesColimitsOfShape_of_evaluation F J fun k => (h k).preservesFiniteColimits _⟩

Premises used: CategoryTheory.Limits.PreservesFiniteColimits.mk, CategoryTheory.Limits.preservesColimitsOfShape_of_evaluation, CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
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
D : Type u₃
inst_3 : Category.{v₃, u₃} D
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_5 : HasColimitsOfShape.{v₂, u₂, v, u} K C
inst_6 : PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J colim
d : D
X : K ⥤ Functor.{v₃, v, u₃, u} D C
⊢ colimit (X ⋙ obj (evaluation D C) d) ≅
    colimit
      (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)) ⋙
        obj (evaluation (K ⥤ Functor.{v₃, v, u₃, u} D C) C) X)

Tactic:
exact HasColimit.isoOfNatIso (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.HasColimit.isoOfNatIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
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
D : Type u₃
inst_3 : Category.{v₃, u₃} D
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
inst_5 : HasLimitsOfShape.{v₂, u₂, v, u} K C
inst_6 : PreservesColimitsOfShape (C := Functor.{v₂, v, u₂, u} K C) J lim
d : D
X : K ⥤ Functor.{v₃, v, u₃, u} D C
⊢ limit (X ⋙ obj (evaluation D C) d) ≅
    limit
      (Functor.flip (obj (whiskeringRight K (Functor.{v₃, v, u₃, u} D C) C) (obj (evaluation D C) d)) ⋙
        obj (evaluation (K ⥤ Functor.{v₃, v, u₃, u} D C) C) X)

Tactic:
exact HasLimit.isoOfNatIso (Iso.refl _)

Premises used: CategoryTheory.Limits.HasLimit.isoOfNatIso, CategoryTheory.Iso.refl