-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
x y : Functor.{v, v_1, u, u_1} (WithTerminal C) D
f : x ⟶ y
⊢ Eq (α :=
    Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithTerminal C) D)) x ⟶
      Functor.obj
        ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithTerminal C) D} ↦ mkCommaMorphism,
            map_id := ⋯, map_comp := ⋯ :
            Functor.{v, v_1, u, u_1} (WithTerminal C) D ⥤
              Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) } ⋙
          { obj := ofCommaObject,
            map :=
              fun
                {X Y : Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)} ↦
              ofCommaMorphism,
            map_id := ⋯, map_comp := ⋯ :
            Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) ⥤
              Functor.{v, v_1, u, u_1} (WithTerminal C) D })
        y)
    (Functor.map (𝟭 (Functor.{v, v_1, u, u_1} (WithTerminal C) D)) f ≫
      Iso.hom
        ((fun (F : Functor.{v, v_1, u, u_1} (WithTerminal C) D) ↦
            (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) ⋯ F
                (Iso.refl (incl ⋙ F)) (Iso.refl (F.obj star)) ⋯ :
              F ≅
                lift (Z := F.obj star) (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) ⋯))
          y))
    (Iso.hom
        ((fun (F : Functor.{v, v_1, u, u_1} (WithTerminal C) D) ↦
            (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) ⋯ F
                (Iso.refl (incl ⋙ F)) (Iso.refl (F.obj star)) ⋯ :
              F ≅
                lift (Z := F.obj star) (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) ⋯))
          x) ≫
      Functor.map
        ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithTerminal C) D} ↦ mkCommaMorphism,
            map_id := ⋯, map_comp := ⋯ :
            Functor.{v, v_1, u, u_1} (WithTerminal C) D ⥤
              Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) } ⋙
          { obj := ofCommaObject,
            map :=
              fun
                {X Y : Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)} ↦
              ofCommaMorphism,
            map_id := ⋯, map_comp := ⋯ :
            Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) ⥤
              Functor.{v, v_1, u, u_1} (WithTerminal C) D })
        f)
have w : ∀ (t : WithTerminal C),
  Eq (α :=
    (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithTerminal C) D)) x).obj t ⟶
      (Functor.obj
            ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithTerminal C) D} ↦ mkCommaMorphism,
                map_id := sorry, map_comp := sorry :
                Functor.{v, v_1, u, u_1} (WithTerminal C) D ⥤
                  Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) } ⋙
              { obj := ofCommaObject,
                map :=
                  fun
                    {X Y :
                      Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)} ↦
                  ofCommaMorphism,
                map_id := sorry, map_comp := sorry :
                Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) ⥤
                  Functor.{v, v_1, u, u_1} (WithTerminal C) D })
            y).obj
        t)
    (NatTrans.app
      (Functor.map (𝟭 (Functor.{v, v_1, u, u_1} (WithTerminal C) D)) f ≫
        Iso.hom
          ((fun (F : Functor.{v, v_1, u, u_1} (WithTerminal C) D) ↦
              (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) sorry F
                  (Iso.refl (incl ⋙ F)) (Iso.refl (F.obj star)) sorry :
                F ≅
                  lift (Z := F.obj star) (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x)))
                    sorry))
            y))
      t)
    (NatTrans.app
      (Iso.hom
          ((fun (F : Functor.{v, v_1, u, u_1} (WithTerminal C) D) ↦
              (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) sorry F
                  (Iso.refl (incl ⋙ F)) (Iso.refl (F.obj star)) sorry :
                F ≅
                  lift (Z := F.obj star) (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x)))
                    sorry))
            x) ≫
        Functor.map
          ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithTerminal C) D} ↦ mkCommaMorphism,
              map_id := sorry, map_comp := sorry :
              Functor.{v, v_1, u, u_1} (WithTerminal C) D ⥤
                Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) } ⋙
            { obj := ofCommaObject,
              map :=
                fun
                  {X Y :
                    Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)} ↦
                ofCommaMorphism,
              map_id := sorry, map_comp := sorry :
              Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) ⥤
                Functor.{v, v_1, u, u_1} (WithTerminal C) D })
          f)
      t)
Tactic: ext t