-- 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)
fst : C
snd : G.obj fst
fst_1 : C
snd_1 : G.obj fst_1
f :
  (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).fst (β := fun (c : C) ↦ G.obj c) ⟶
    (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ G.obj c)
e :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) :
        (a : (fun (X : Type w) ↦ X) (G.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (G.obj ⟨fst_1, snd_1⟩.fst))
      ((Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).snd (β := fun (c : C) ↦ G.obj c)) =
    (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ G.obj c)
⊢ Eq (α :=
    (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj
        (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd) ⟶
      obj (𝟭 G.Elements) (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1))
    ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).map
        (Subtype.mk (p :=
          fun
            (f :
              (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).fst (β := fun (c : C) ↦ G.obj c) ⟶
                (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ G.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) :
                (a : (fun (X : Type w) ↦ X) (G.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (G.obj ⟨fst_1, snd_1⟩.fst))
              ((Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).snd (β := fun (c : C) ↦ G.obj c)) =
            (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ G.obj c))
          f e) ≫
      Iso.hom
        ((fun (X : G.Elements) ↦
            (Sigma.casesOn (β := fun (c : C) ↦ G.obj c) (motive := fun (t : (c : C) × G.obj c) ↦
                (h : X = t) →
                  (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ obj (𝟭 G.Elements) X)
                X
                (fun (fst : C) (snd : G.obj fst) (h : X = Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd) ↦
                  Eq.ndrec (motive := fun (X : G.Elements) ↦
                    (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ obj (𝟭 G.Elements) X)
                    (Iso.refl
                      ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj
                        (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd)))
                    ⋯)
                ⋯ :
              (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ obj (𝟭 G.Elements) X))
          (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1)))
    (CategoryStruct.comp (Y := obj (𝟭 G.Elements) (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd))
      (Iso.hom
        ((fun (X : G.Elements) ↦
            (Sigma.casesOn (β := fun (c : C) ↦ G.obj c) (motive := fun (t : (c : C) × G.obj c) ↦
                (h : X = t) →
                  (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ obj (𝟭 G.Elements) X)
                X
                (fun (fst : C) (snd : G.obj fst) (h : X = Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd) ↦
                  Eq.ndrec (motive := fun (X : G.Elements) ↦
                    (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ obj (𝟭 G.Elements) X)
                    (Iso.refl
                      ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj
                        (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd)))
                    ⋯)
                ⋯ :
              (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ obj (𝟭 G.Elements) X))
          (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd)))
      (Functor.map (𝟭 G.Elements)
        (Subtype.mk (p :=
          fun
            (f :
              (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).fst (β := fun (c : C) ↦ G.obj c) ⟶
                (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).fst (β := fun (c : C) ↦ G.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) :
                (a : (fun (X : Type w) ↦ X) (G.obj ⟨fst, snd⟩.fst)) → (fun (X : Type w) ↦ X) (G.obj ⟨fst_1, snd_1⟩.fst))
              ((Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd).snd (β := fun (c : C) ↦ G.obj c)) =
            (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1).snd (β := fun (c : C) ↦ G.obj c))
          f e)))
have dsimp : (grothendieckTypeToCatFunctor G).map
      ((grothendieckTypeToCatInverse G).map
        (Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e)) ≫
    𝟙
      ((grothendieckTypeToCatFunctor G).obj
        ((grothendieckTypeToCatInverse G).obj (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst_1 snd_1))) =
  𝟙
      ((grothendieckTypeToCatFunctor G).obj
        ((grothendieckTypeToCatInverse G).obj (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd))) ≫
    Subtype.mk (p := fun (f : fst ⟶ fst_1) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f) : (a : G.obj fst) → G.obj fst_1) snd = snd_1) f e
Tactic: dsimp at *