-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
bi : C
fi : (↑(F.obj (G.obj bi)) : Type u_2)
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : (↑(F.obj (G.obj bj)) : Type u_2)
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
w_fiber :
  Eq (α :=
    obj
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              (StructuredArrow.hom
                { left := { as := PUnit.unit : Discrete PUnit.{1} },
                  right := { base := bj, fiber := fj : Grothendieck (G ⋙ F) },
                  hom :=
                    { base := gbj, fiber := gfj :
                      (obj (fromPUnit { base := d, fiber := f : Grothendieck F })
                            { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                        ((pre F G).obj { base := bj, fiber := fj : Grothendieck (G ⋙ F) }) } :
                  Comma (fromPUnit { base := d, fiber := f : Grothendieck F }) (pre F G) }))))
        { base := d, fiber := f : Grothendieck F }.fiber ⟶
      ((pre F G).obj
          (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F }) (T := pre F G)
            { left := { as := PUnit.unit : Discrete PUnit.{1} },
              right := { base := bj, fiber := fj : Grothendieck (G ⋙ F) },
              hom :=
                { base := gbj, fiber := gfj :
                  (obj (fromPUnit { base := d, fiber := f : Grothendieck F })
                        { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                    ((pre F G).obj { base := bj, fiber := fj : Grothendieck (G ⋙ F) }) } :
              Comma (fromPUnit { base := d, fiber := f : Grothendieck F }) (pre F G) })).fiber)
    (CategoryStruct.comp (Y :=
      obj
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              (CategoryStruct.comp (Y :=
                (pre F G).obj
                  (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F }) (T :=
                    pre F G)
                    (StructuredArrow.mk (Y :=
                      { base := bj, fiber := (F.map gbj).toFunctor.obj f : Grothendieck (G ⋙ F) })
                      { base := gbj,
                        fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) :
                        { base := d, fiber := f : Grothendieck F }.Hom
                          ((pre F G).obj
                            { base := bj, fiber := (F.map gbj).toFunctor.obj f : Grothendieck (G ⋙ F) }) })))
                (StructuredArrow.hom
                  (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f : Grothendieck (G ⋙ F) })
                    { base := gbj,
                      fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) :
                      { base := d, fiber := f : Grothendieck F }.Hom
                        ((pre F G).obj { base := bj, fiber := (F.map gbj).toFunctor.obj f : Grothendieck (G ⋙ F) }) }))
                ((pre F G).map
                  { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj :
                    Hom.{u₁, v₁, u_2, u_1} (F := G ⋙ F)
                      (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F })
                        (T := pre F G)
                        (StructuredArrow.mk (Y :=
                          { base := bj, fiber := (F.map gbj).toFunctor.obj f : Grothendieck (G ⋙ F) })
                          { base := gbj,
                            fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) :
                            { base := d, fiber := f : Grothendieck F }.Hom
                              ((pre F G).obj
                                { base := bj, fiber := (F.map gbj).toFunctor.obj f : Grothendieck (G ⋙ F) }) }))
                      (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F })
                        (T := pre F G)
                        { left := { as := PUnit.unit : Discrete PUnit.{1} },
                          right := { base := bj, fiber := fj : Grothendieck (G ⋙ F) },
                          hom :=
                            { base := gbj, fiber := gfj :
                              (obj (fromPUnit { base := d, fiber := f : Grothendieck F })
                                    { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                                ((pre F G).obj { base := bj, fiber := fj : Grothendieck (G ⋙ F) }) } :
                          Comma (fromPUnit { base := d, fiber := f : Grothendieck F }) (pre F G) }) })))))
        { base := d, fiber := f : Grothendieck F }.fiber)
      (eqToHom ⋯)
      (Hom.fiber
        (CategoryStruct.comp (Y :=
          (pre F G).obj
            (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f }) (T := pre F G)
              (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
                { base := gbj,
                  fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })))
          (StructuredArrow.hom
            (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
              { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) }))
          ((pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj }))))
    (Hom.fiber
      (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj }, hom := { base := gbj, fiber := gfj } }))
⊢ Eq (α :=
    { base := d, fiber := f : Grothendieck F } ⟶
      (pre F G).obj
        (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f }) (T := pre F G)
          { left := { as := PUnit.unit }, right := { base := bj, fiber := fj }, hom := { base := gbj, fiber := gfj } }))
    (CategoryStruct.comp (Y :=
      (pre F G).obj
        (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f }) (T := pre F G)
          (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
            { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })))
      (StructuredArrow.hom
        (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
          { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) }))
      ((pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj }))
    (StructuredArrow.hom
      { left := { as := PUnit.unit }, right := { base := bj, fiber := fj }, hom := { base := gbj, fiber := gfj } })
have w_base : Eq (α :=
  { base := d, fiber := f : Grothendieck F }.base ⟶
    ((pre F G).obj
        (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f : Grothendieck F }) (T := pre F G)
          { left := { as := PUnit.unit : Discrete PUnit.{1} },
            right := { base := bj, fiber := fj : Grothendieck (G ⋙ F) },
            hom :=
              { base := gbj, fiber := gfj :
                (obj (fromPUnit { base := d, fiber := f : Grothendieck F })
                      { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                  ((pre F G).obj { base := bj, fiber := fj : Grothendieck (G ⋙ F) }) } :
            Comma (fromPUnit { base := d, fiber := f : Grothendieck F }) (pre F G) })).base)
  (Hom.base
    (CategoryStruct.comp (Y :=
      (pre F G).obj
        (StructuredArrow.right (D := Grothendieck F) (S := { base := d, fiber := f }) (T := pre F G)
          (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
            { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })))
      (StructuredArrow.hom
        (StructuredArrow.mk (Y := { base := bj, fiber := (F.map gbj).toFunctor.obj f })
          { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) }))
      ((pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom sorry ≫ gfj })))
  (Hom.base
    (StructuredArrow.hom
      { left := { as := PUnit.unit }, right := { base := bj, fiber := fj }, hom := { base := gbj, fiber := gfj } }))
Tactic: apply Grothendieck.ext