-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
base_1 : C
as : G.obj base_1
base_2 : C
as_1 : G.obj base_2
base :
  Grothendieck.base.{u, v, w, w} (F := G ⋙ typeToCat)
      { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } : Grothendieck (G ⋙ typeToCat) } ⟶
    Grothendieck.base.{u, v, w, w} (F := G ⋙ typeToCat)
      { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } }
f :
  (((G ⋙ typeToCat).map base).toFunctor.obj
        (fiber { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } : Grothendieck (G ⋙ typeToCat) })).as =
    Discrete.as (fiber { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } })
simp :
  { base := base,
      fiber :=
        {
          down :=
            { down := f :
              PLift
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                  as_1) } :
          ULift.{w, 0}
            (PLift
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                as_1)) } :
      Hom.{u, v, w, w} (F := G ⋙ typeToCat)
        { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } : Grothendieck (G ⋙ typeToCat) }
        { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } : Grothendieck (G ⋙ typeToCat) } } =
    (grothendieckTypeToCatInverse G).map
      ((grothendieckTypeToCatFunctor G).map
        { base := base,
          fiber :=
            {
              down :=
                { down := f :
                  PLift
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                      as_1) } :
              ULift.{w, 0}
                (PLift
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                    as_1)) } })
⊢ { base := base,
        fiber :=
          {
            down :=
              { down := f :
                PLift
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                    as_1) } :
            ULift.{w, 0}
              (PLift
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                  as_1)) } :
        Hom.{u, v, w, w} (F := G ⋙ typeToCat)
          { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } : Grothendieck (G ⋙ typeToCat) }
          { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } : Grothendieck (G ⋙ typeToCat) } } ≫
      𝟙 { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } } =
    𝟙 { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } : Grothendieck (G ⋙ typeToCat) } ≫
      (grothendieckTypeToCatInverse G).map
        ((grothendieckTypeToCatFunctor G).map
          { base := base,
            fiber :=
              {
                down :=
                  { down := f :
                    PLift
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                        as_1) } :
                ULift.{w, 0}
                  (PLift
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map base) : (a : G.obj base_1) → G.obj base_2) as =
                      as_1)) } :
            Hom.{u, v, w, w} (F := G ⋙ typeToCat)
              { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } : Grothendieck (G ⋙ typeToCat) }
              { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } : Grothendieck (G ⋙ typeToCat) } })

Tactic:
simp