-- 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_base :
  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)) =
    Hom.base
      (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)
w_fiber :
  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)
⊢ (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) =
    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:
fapply Grothendieck.ext

Premises used: CategoryTheory.Grothendieck.ext