no goals
C : Type ?u.14362
D : Type ?u.14365
inst✝¹ : Category C
inst✝ : Category D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (𝟙 X).base).obj X.fiber = X.fiber
erw [CategoryTheory.Functor.map_id, Functor.id_obj X.fiber]