C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
⊢ RepresentablyFlat F
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
⊢ RepresentablyFlat F
skip
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this : PreservesFiniteLimits (lan (Functor.op F))
⊢ RepresentablyFlat F
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
⊢ RepresentablyFlat F
haveI := preservesFiniteLimitsOfFlat (lan F.op : _ ⥤ Dᵒᵖ ⥤ Type u₁)
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this✝ : PreservesFiniteLimits (lan (Functor.op F))
this : PreservesFiniteLimits F
⊢ RepresentablyFlat F
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this : PreservesFiniteLimits (lan (Functor.op F))
⊢ RepresentablyFlat F
haveI : PreservesFiniteLimits F := by
  apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁}
  intros ; skip; apply preservesLimitOfLanPreservesLimit
no goals
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this✝ : PreservesFiniteLimits (lan (Functor.op F))
this : PreservesFiniteLimits F
⊢ RepresentablyFlat F
apply flat_of_preservesFiniteLimits
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this : PreservesFiniteLimits (lan (Functor.op F))
⊢ (J : Type u₁) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this : PreservesFiniteLimits (lan (Functor.op F))
⊢ PreservesFiniteLimits F
apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁}
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this : PreservesFiniteLimits (lan (Functor.op F))
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this : PreservesFiniteLimits (lan (Functor.op F))
⊢ (J : Type u₁) → {𝒥 : SmallCategory J} → FinCategory J → PreservesLimitsOfShape J F
intros
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this : PreservesFiniteLimits (lan (Functor.op F))
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this : PreservesFiniteLimits (lan (Functor.op F))
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F
skip
no goals
case h
C D : Type u₁
inst✝⁹ : SmallCategory C
inst✝⁸ : SmallCategory D
E : Type u₂
inst✝⁷ : Category E
inst✝⁶ : ConcreteCategory E
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (lan (Functor.op F))
this : PreservesFiniteLimits (lan (Functor.op F))
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F
apply preservesLimitOfLanPreservesLimit