-- 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) } })
⊢ Eq (α :=
    obj (𝟭 (Grothendieck (G ⋙ typeToCat))) { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } } ⟶
      (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj
        { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } : Grothendieck (G ⋙ typeToCat) })
    (CategoryStruct.comp (Y :=
      obj (𝟭 (Grothendieck (G ⋙ typeToCat))) { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } })
      (Functor.map (𝟭 (Grothendieck (G ⋙ typeToCat)))
        { base := base,
          fiber :=
            {
              down :=
                { down := f :
                  PLift
                    ((((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) } :
                            Grothendieck (G ⋙ typeToCat) })) } :
              ULift.{w, 0}
                (PLift
                  ((((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) } :
                          Grothendieck (G ⋙ typeToCat) }))) } })
      (Iso.hom
        ((fun (X : Grothendieck (G ⋙ typeToCat)) ↦
            (casesOn (motive := fun (x : Grothendieck (G ⋙ typeToCat)) ↦
                obj (𝟭 (Grothendieck (G ⋙ typeToCat))) x ≅
                  (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj x)
                X fun (base : C) (fiber : (↑((G ⋙ typeToCat).obj base) : Type w)) ↦
                Discrete.casesOn (motive := fun (x : (↑((G ⋙ typeToCat).obj base) : Type w)) ↦
                  obj (𝟭 (Grothendieck (G ⋙ typeToCat))) { base := base, fiber := x : Grothendieck (G ⋙ typeToCat) } ≅
                    (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj { base := base, fiber := x })
                  fiber fun (as : G.obj base) ↦
                  Iso.refl
                    (obj (𝟭 (Grothendieck (G ⋙ typeToCat)))
                      { base := base, fiber := { as := as : Discrete (G.obj base) } }) :
              obj (𝟭 (Grothendieck (G ⋙ typeToCat))) X ≅
                (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj X))
          { base := base_2, fiber := { as := as_1 : Discrete (G.obj base_2) } })))
    (Iso.hom
        ((fun (X : Grothendieck (G ⋙ typeToCat)) ↦
            (casesOn (motive := fun (x : Grothendieck (G ⋙ typeToCat)) ↦
                obj (𝟭 (Grothendieck (G ⋙ typeToCat))) x ≅
                  (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj x)
                X fun (base : C) (fiber : (↑((G ⋙ typeToCat).obj base) : Type w)) ↦
                Discrete.casesOn (motive := fun (x : (↑((G ⋙ typeToCat).obj base) : Type w)) ↦
                  obj (𝟭 (Grothendieck (G ⋙ typeToCat))) { base := base, fiber := x : Grothendieck (G ⋙ typeToCat) } ≅
                    (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj { base := base, fiber := x })
                  fiber fun (as : G.obj base) ↦
                  Iso.refl
                    (obj (𝟭 (Grothendieck (G ⋙ typeToCat)))
                      { base := base, fiber := { as := as : Discrete (G.obj base) } }) :
              obj (𝟭 (Grothendieck (G ⋙ typeToCat))) X ≅
                (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj X))
          { base := base_1, fiber := { as := as : Discrete (G.obj base_1) } }) ≫
      (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).map
        { base := base,
          fiber :=
            {
              down :=
                { down := f :
                  PLift
                    ((((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) } :
                            Grothendieck (G ⋙ typeToCat) })) } :
              ULift.{w, 0}
                (PLift
                  ((((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) } :
                          Grothendieck (G ⋙ typeToCat) }))) } :
          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 dsimp : { 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: dsimp at *