-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : Functor.{v, max ?u.73182 ?u.73183, u, max (?u.73182 + 1) (?u.73183 + 1)} C Cat
α : F ⟶ G
X Y : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X ⟶ Y
w_fiber :
  Eq (α :=
    Quiver.Hom (V := AsSmall.{w, v₂, u₂} (↑(G.obj Y.base) : Type u₂))
      (obj AsSmall.up
        ((G.map (𝟙 Y.base)).toFunctor.obj
          (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))))
      (obj AsSmall.up ((G.map (𝟙 Y.base)).toFunctor.obj (obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber.down))))
    (Functor.map AsSmall.up
      ((G.map (𝟙 Y.base)).toFunctor.map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down)))
    (CategoryStruct.comp (Y :=
      obj AsSmall.up (obj (Cat.Hom.toFunctor (α.app Y.base)) ((F.map f.base).toFunctor.obj X.fiber.down))) (eqToHom ⋯)
      (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down) ≫ eqToHom ⋯))
⊢ CategoryStruct.comp (Y :=
      obj
        (Cat.Hom.toFunctor
          ((G ⋙ Cat.asSmallFunctor).map
            (Hom.base
              ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
                Iso.hom
                  ((fun (X : Grothendieck (F ⋙ Cat.asSmallFunctor)) ↦
                      (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X) :
                        (map (whiskerRight α Cat.asSmallFunctor)).obj X ≅
                          (map (whiskerRight α Cat.asSmallFunctor)).obj X))
                    Y)))))
        ((map (whiskerRight α Cat.asSmallFunctor)).obj X).fiber)
      (eqToHom ⋯)
      (Hom.fiber
        ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
          Iso.hom
            ((fun (X : Grothendieck (F ⋙ Cat.asSmallFunctor)) ↦
                (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X) :
                  (map (whiskerRight α Cat.asSmallFunctor)).obj X ≅ (map (whiskerRight α Cat.asSmallFunctor)).obj X))
              Y))) =
    Hom.fiber
      (Iso.hom
          ((fun (X : Grothendieck (F ⋙ Cat.asSmallFunctor)) ↦
              (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X) :
                (map (whiskerRight α Cat.asSmallFunctor)).obj X ≅ (map (whiskerRight α Cat.asSmallFunctor)).obj X))
            X) ≫
        ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f)

Tactic:
simp only [compAsSmallFunctorEquivalence_functor, compAsSmallFunctorEquivalence_inverse,
        comp_obj, compAsSmallFunctorEquivalenceInverse_obj_base, map_obj_base,
        compAsSmallFunctorEquivalenceFunctor_obj_base, Cat.asSmallFunctor_obj, Cat.of_α,
        Iso.refl_hom, Functor.comp_map, comp_base, id_base,
        compAsSmallFunctorEquivalenceInverse_map_base, map_map_base,
        compAsSmallFunctorEquivalenceFunctor_map_base, Cat.asSmallFunctor_map, toCatHom_toFunctor,
        map_obj_fiber, whiskerRight_app, AsSmall.down_obj, AsSmall.up_obj_down,
        compAsSmallFunctorEquivalenceInverse_obj_fiber,
        compAsSmallFunctorEquivalenceFunctor_obj_fiber, comp_fiber, map_map_fiber, AsSmall.down_map,
        down_comp, eqToHom_down, AsSmall.up_map_down, map_comp, eqToHom_map, id_fiber,
        Category.assoc, eqToHom_trans_assoc, compAsSmallFunctorEquivalenceInverse_map_fiber,
        compAsSmallFunctorEquivalenceFunctor_map_fiber, eqToHom_comp_iff, comp_eqToHom_iff]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Cat.asSmallFunctor_obj, CategoryTheory.Category.assoc, CategoryTheory.Cat.of_α, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber, CategoryTheory.Grothendieck.comp_base, CategoryTheory.eqToHom_map, CategoryTheory.AsSmall.down_obj, CategoryTheory.Grothendieck.id_fiber, CategoryTheory.Grothendieck.comp_fiber, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber, CategoryTheory.AsSmall.up_obj_down, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_functor, CategoryTheory.Grothendieck.id_base, CategoryTheory.AsSmall.up_map_down, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_inverse, CategoryTheory.Grothendieck.map_obj_fiber, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base, CategoryTheory.eqToHom_down, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_base, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Grothendieck.map_obj_base, CategoryTheory.comp_eqToHom_iff, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber, CategoryTheory.Functor.map_comp, CategoryTheory.Grothendieck.map_map_fiber, CategoryTheory.Cat.asSmallFunctor_map, CategoryTheory.Grothendieck.map_map_base, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.eqToHom_comp_iff, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base, CategoryTheory.AsSmall.down_map, CategoryTheory.Iso.refl_hom, CategoryTheory.Functor.comp_map, CategoryTheory.down_comp, CategoryTheory.Functor.toCatHom_toFunctor