[GOAL]
C : Type v₁
inst✝⁹ : SmallCategory C
D : Type v₁
inst✝⁸ : SmallCategory D
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesFilteredColimits (forget A)
inst✝¹ : ReflectsIsomorphisms (forget A)
G : C ⥤ D
inst✝ : RepresentablyFlat G
⊢ PreservesFiniteLimits (Sites.pushforward A J K G)
[PROOFSTEP]
have : PreservesFiniteLimits (lan (Functor.op G) ⋙ presheafToSheaf K A) := compPreservesFiniteLimits _ _
[GOAL]
C : Type v₁
inst✝⁹ : SmallCategory C
D : Type v₁
inst✝⁸ : SmallCategory D
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesFilteredColimits (forget A)
inst✝¹ : ReflectsIsomorphisms (forget A)
G : C ⥤ D
inst✝ : RepresentablyFlat G
this : PreservesFiniteLimits (lan G.op ⋙ presheafToSheaf K A)
⊢ PreservesFiniteLimits (Sites.pushforward A J K G)
[PROOFSTEP]
apply compPreservesFiniteLimits
