[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
J✝ : Type w
inst✝³ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝² : PreservesFiniteLimits F
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
apply preservesLimitsOfShapeOfEquiv (FinCategory.equivAsType J)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J✝ : Type w
inst✝¹ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
haveI := preservesSmallestLimitsOfPreservesLimits F
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J✝ : Type w
inst✝¹ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
exact preservesLimitsOfShapeOfEquiv (FinCategory.equivAsType J) F
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
letI : Category (ULiftHom (ULift J)) := ULiftHom.category
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : Category.{?u.3382, ?u.3380} (ULiftHom (ULift J)) := ULiftHom.category
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this✝ : Category.{?u.3382, ?u.3380} (ULiftHom (ULift J)) := ULiftHom.category
this : PreservesLimitsOfShape (ULiftHom (ULift J)) F
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
exact preservesLimitsOfShapeOfEquiv (ULiftHomULiftCategory.equiv J).symm F
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
⊢ PreservesLimitsOfShape x✝² (𝟭 C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
J : Type w
inst✝² : SmallCategory J
K : J ⥤ C
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteLimits G
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
⊢ PreservesLimitsOfShape x✝² (F ⋙ G)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
J✝ : Type w
inst✝³ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝² : PreservesFiniteColimits F
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
apply preservesColimitsOfShapeOfEquiv (FinCategory.equivAsType J)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J✝ : Type w
inst✝¹ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
haveI := preservesSmallestColimitsOfPreservesColimits F
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J✝ : Type w
inst✝¹ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
exact preservesColimitsOfShapeOfEquiv (FinCategory.equivAsType J) F
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
letI : Category (ULiftHom (ULift J)) := ULiftHom.category
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : Category.{?u.13228, ?u.13226} (ULiftHom (ULift J)) := ULiftHom.category
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
J✝ : Type w
inst✝ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
h : (J : Type w) → {𝒥 : SmallCategory J} → FinCategory J → PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this✝ : Category.{?u.13228, ?u.13226} (ULiftHom (ULift J)) := ULiftHom.category
this : PreservesColimitsOfShape (ULiftHom (ULift J)) F
⊢ PreservesColimitsOfShape J F
[PROOFSTEP]
exact preservesColimitsOfShapeOfEquiv (ULiftHomULiftCategory.equiv J).symm F
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
J : Type w
inst✝² : SmallCategory J
K : J ⥤ C
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesFiniteColimits F
inst✝ : PreservesFiniteColimits G
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
⊢ PreservesColimitsOfShape x✝² (F ⋙ G)
[PROOFSTEP]
infer_instance
