-- 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
⊢ 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 := bi, fiber := fi }, hom := { base := gbi, fiber := gfi } }))
    (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 := bi, fiber := (F.map gbi).toFunctor.obj f })
            { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })))
      (StructuredArrow.hom
        (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
          { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) }))
      ((pre F G).map { base := _root_.id (𝟙 bi), fiber := eqToHom ⋯ ≫ gfi }))
    (StructuredArrow.hom
      { left := { as := PUnit.unit }, right := { base := bi, fiber := fi }, hom := { base := gbi, fiber := gfi } })
have w_fiber : Eq (α :=
  obj
      (Cat.Hom.toFunctor
        (F.map
          (Hom.base
            (StructuredArrow.hom
              { left := { as := PUnit.unit : Discrete PUnit.{1} },
                right := { base := bi, fiber := fi : Grothendieck (G ⋙ F) },
                hom :=
                  { base := gbi, fiber := gfi :
                    (obj (fromPUnit { base := d, fiber := f : Grothendieck F })
                          { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                      ((pre F G).obj { base := bi, fiber := fi : 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 := bi, fiber := fi : Grothendieck (G ⋙ F) },
            hom :=
              { base := gbi, fiber := gfi :
                (obj (fromPUnit { base := d, fiber := f : Grothendieck F })
                      { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                  ((pre F G).obj { base := bi, fiber := fi : 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 := bi, fiber := (F.map gbi).toFunctor.obj f : Grothendieck (G ⋙ F) })
                    { base := gbi,
                      fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) :
                      { base := d, fiber := f : Grothendieck F }.Hom
                        ((pre F G).obj { base := bi, fiber := (F.map gbi).toFunctor.obj f : Grothendieck (G ⋙ F) }) })))
              (StructuredArrow.hom
                (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f : Grothendieck (G ⋙ F) })
                  { base := gbi,
                    fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) :
                    { base := d, fiber := f : Grothendieck F }.Hom
                      ((pre F G).obj { base := bi, fiber := (F.map gbi).toFunctor.obj f : Grothendieck (G ⋙ F) }) }))
              ((pre F G).map
                { base := _root_.id (𝟙 bi), fiber := eqToHom sorry ≫ gfi :
                  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 := bi, fiber := (F.map gbi).toFunctor.obj f : Grothendieck (G ⋙ F) })
                        { base := gbi,
                          fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) :
                          { base := d, fiber := f : Grothendieck F }.Hom
                            ((pre F G).obj
                              { base := bi, fiber := (F.map gbi).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 := bi, fiber := fi : Grothendieck (G ⋙ F) },
                        hom :=
                          { base := gbi, fiber := gfi :
                            (obj (fromPUnit { base := d, fiber := f : Grothendieck F })
                                  { as := PUnit.unit : Discrete PUnit.{1} }).Hom
                              ((pre F G).obj { base := bi, fiber := fi : Grothendieck (G ⋙ F) }) } :
                        Comma (fromPUnit { base := d, fiber := f : Grothendieck F }) (pre F G) }) })))))
      { base := d, fiber := f : Grothendieck F }.fiber)
    (eqToHom sorry)
    (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 := bi, fiber := (F.map gbi).toFunctor.obj f })
              { base := gbi,
                fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) })))
        (StructuredArrow.hom
          (StructuredArrow.mk (Y := { base := bi, fiber := (F.map gbi).toFunctor.obj f })
            { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f : Grothendieck F }.fiber) }))
        ((pre F G).map { base := _root_.id (𝟙 bi), fiber := eqToHom sorry ≫ gfi }))))
  (Hom.fiber
    (StructuredArrow.hom
      { left := { as := PUnit.unit }, right := { base := bi, fiber := fi }, hom := { base := gbi, fiber := gfi } }))
Tactic: apply Grothendieck.ext