-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
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
⊢ 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)
have 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 sorry)
    (Functor.map AsSmall.up (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber.down) ≫ eqToHom sorry))
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]