-- 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
α : F ⟶ G
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
simp :
  Eq (α :=
    obj
        (Cat.Hom.toFunctor
          (G.map
            (Hom.base
              ({ base := f.base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                  { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                    { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
                { base := g.base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
                  { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G }.Hom
                    { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }))))
        (obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber) ⟶
      obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber)
    (eqToHom ⋯ ≫
        (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app Z.base)) (eqToHom ⋯) ≫
            (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (α.app Y.base ≫ G.map g.base)) f.fiber ≫ eqToHom ⋯) ≫
              Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
      obj
          (Cat.Hom.toFunctor
            (G.map
              (Hom.base
                ({ base := f.base,
                    fiber :=
                      (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                    { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                      { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
                  { base := g.base,
                    fiber :=
                      (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
                    { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G }.Hom
                      { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }))))
          (obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber) ⟶
        obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber)
    (eqToHom ⋯ ≫
        ((G.map g.base).toFunctor.map ((Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber) ≫
            (G.map g.base).toFunctor.map (Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber)) ≫
          (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
      obj
          (Cat.Hom.toFunctor
            (G.map
              (Hom.base
                ({ base := f.base,
                    fiber :=
                      (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                    { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                      { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
                  { base := g.base,
                    fiber :=
                      (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
                    { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G }.Hom
                      { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }))))
          (obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber) ⟶
        obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber)
⊢ Eq (α :=
    obj
        (Cat.Hom.toFunctor
          (G.map
            (Hom.base
              ({ base := f.base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                  { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                    { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
                { base := g.base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
                  { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G }.Hom
                    { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }))))
        { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.fiber ⟶
      { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G }.fiber)
    (CategoryStruct.comp (Y :=
        (G.map
                { base := (f ≫ g).base,
                    fiber :=
                      (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app Z.base)) (f ≫ g).fiber :
                    { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                      { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber :
                        Grothendieck G } }.base).toFunctor.obj
          { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber }.fiber)
        (eqToHom ⋯)
        { base := (f ≫ g).base,
            fiber :=
              (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
                Functor.map (Cat.Hom.toFunctor (α.app Z.base)) (f ≫ g).fiber }.fiber :
      obj
          (Cat.Hom.toFunctor
            (G.map
              (Hom.base
                ({ base := f.base,
                    fiber :=
                      (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                    { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                      { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
                  { base := g.base,
                    fiber :=
                      (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
                    { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G }.Hom
                      { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }))))
          { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.fiber ⟶
        { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G }.fiber)
    (Hom.fiber
        ({ base := f.base,
            fiber :=
              (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
            { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
              { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
          { base := g.base,
            fiber :=
              (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫
                Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber }) :
      obj
          (Cat.Hom.toFunctor
            (G.map
              (Hom.base
                ({ base := f.base,
                    fiber :=
                      (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                    { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                      { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
                  { base := g.base,
                    fiber :=
                      (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
                    { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G }.Hom
                      { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }))))
          { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.fiber ⟶
        { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G }.fiber)

Tactic:
simp only [comp_fiber, map_comp, ← Cat.Hom.comp_map,
      Functor.congr_hom congr($(α.naturality g.base).toFunctor) f.fiber]

Premises used: congrArg, CategoryTheory.Functor.congr_hom, CategoryTheory.Grothendieck.comp_fiber, id, CategoryTheory.Cat.Hom.comp_map, CategoryTheory.Grothendieck.Hom.fiber, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Cat.Hom.toFunctor, CategoryTheory.Grothendieck.Hom.base