Filteredness of Grothendieck construction

We show that if F : C ⥤ Cat is such that C is filtered and F.obj c is filtered for all c : C, then Grothendieck F is filtered.

instance CategoryTheory.instIsFilteredOrEmptyGrothendieckOfαCategoryObjCat {C : Type u} [Category.{v, u} C] (F : Functor C Cat) [IsFilteredOrEmpty C] [∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)] : IsFilteredOrEmpty (Grothendieck F)

instance CategoryTheory.instIsFilteredGrothendieckOfαCategoryObjCat {C : Type u} [Category.{v, u} C] (F : Functor C Cat) [IsFiltered C] [∀ (c : C), IsFiltered ↑(F.obj c)] : IsFiltered (Grothendieck F)