-- 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 : 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) } })
⊢ { 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) } })
have 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)) } })
Tactic: simp