-- 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 : C
as : G.obj base
⊢ (grothendieckTypeToCatFunctor G).map
        ((NatIso.ofComponents
                (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 : Grothendieck (G ⋙ typeToCat) })
                      fiber fun (as : G.obj base) ↦
                      Iso.refl
                        (obj (𝟭 (Grothendieck (G ⋙ typeToCat)))
                          { base := base, fiber := { as := as : Discrete (G.obj base) } :
                            Grothendieck (G ⋙ typeToCat) }))
                ⋯).hom.app
          { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) }) ≫
      (NatIso.ofComponents
              (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)))
                      ⋯)
                  ⋯)
              ⋯).hom.app
        ((grothendieckTypeToCatFunctor G).obj { base := base, fiber := { as := as : Discrete (G.obj base) } }) =
    𝟙
      ((grothendieckTypeToCatFunctor G).obj
        { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) })
have simp : Iso.hom
    (Sigma.rec (β := fun (c : C) ↦ G.obj c) (motive := fun (t : (c : C) × G.obj c) ↦
      (h :
          (grothendieckTypeToCatFunctor G).obj
              { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) } =
            t) →
        (grothendieckTypeToCatFunctor G).obj
            ((grothendieckTypeToCatInverse G).obj
              ((grothendieckTypeToCatFunctor G).obj
                { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) })) ≅
          (grothendieckTypeToCatFunctor G).obj { base := base, fiber := { as := as : Discrete (G.obj base) } })
      (fun (fst : C) (snd : G.obj fst)
          (h :
            (grothendieckTypeToCatFunctor G).obj
                { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) } =
              Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd) ↦
        Eq.rec (motive := fun (x : G.Elements) (x_1 : Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd = x) ↦
          (grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj x) ≅ x)
          (Iso.refl
            ((grothendieckTypeToCatFunctor G).obj
              ((grothendieckTypeToCatInverse G).obj (Sigma.mk (β := fun (c : C) ↦ G.obj c) fst snd))))
          sorry)
      ((grothendieckTypeToCatFunctor G).obj
        { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) })
      sorry) =
  𝟙
    ((grothendieckTypeToCatFunctor G).obj
      { base := base, fiber := { as := as : Discrete (G.obj base) } : Grothendieck (G ⋙ typeToCat) })
Tactic: simp