-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
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} (WithInitial C) D
f : x ⟶ y
w :
  ∀ (t : WithInitial C),
    Eq (α :=
      (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithInitial C) D)) x).obj t ⟶
        (Functor.obj
              ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithInitial C) D} ↦ mkCommaMorphism,
                  map_id := ⋯, map_comp := ⋯ :
                  Functor.{v, v_1, u, u_1} (WithInitial C) D ⥤
                    Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                      (𝟭 (Functor.{v, v_1, u, u_1} C D)) } ⋙
                { obj := ofCommaObject,
                  map :=
                    fun
                      {X Y :
                        Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                          (𝟭 (Functor.{v, v_1, u, u_1} C D))} ↦
                    ofCommaMorphism,
                  map_id := ⋯, map_comp := ⋯ :
                  Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                      (𝟭 (Functor.{v, v_1, u, u_1} C D)) ⥤
                    Functor.{v, v_1, u, u_1} (WithInitial C) D })
              y).obj
          t)
      (NatTrans.app
        (Functor.map (𝟭 (Functor.{v, v_1, u, u_1} (WithInitial C) D)) f ≫
          Iso.hom
            ((fun (F : Functor.{v, v_1, u, u_1} (WithInitial C) D) ↦
                (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (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.IsInitial.to starInitial (of x))) ⋯))
              y))
        t)
      (NatTrans.app
        (Iso.hom
            ((fun (F : Functor.{v, v_1, u, u_1} (WithInitial C) D) ↦
                (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (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.IsInitial.to starInitial (of x))) ⋯))
              x) ≫
          Functor.map
            ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithInitial C) D} ↦ mkCommaMorphism,
                map_id := ⋯, map_comp := ⋯ :
                Functor.{v, v_1, u, u_1} (WithInitial C) D ⥤
                  Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                    (𝟭 (Functor.{v, v_1, u, u_1} C D)) } ⋙
              { obj := ofCommaObject,
                map :=
                  fun
                    {X Y :
                      Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                        (𝟭 (Functor.{v, v_1, u, u_1} C D))} ↦
                  ofCommaMorphism,
                map_id := ⋯, map_comp := ⋯ :
                Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                    (𝟭 (Functor.{v, v_1, u, u_1} C D)) ⥤
                  Functor.{v, v_1, u, u_1} (WithInitial C) D })
            f)
        t)
⊢ Eq (α :=
    Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithInitial C) D)) x ⟶
      Functor.obj
        ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithInitial C) D} ↦ mkCommaMorphism,
            map_id := ⋯, map_comp := ⋯ :
            Functor.{v, v_1, u, u_1} (WithInitial C) D ⥤
              Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                (𝟭 (Functor.{v, v_1, u, u_1} C D)) } ⋙
          { obj := ofCommaObject,
            map :=
              fun
                {X Y :
                  Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                    (𝟭 (Functor.{v, v_1, u, u_1} C D))} ↦
              ofCommaMorphism,
            map_id := ⋯, map_comp := ⋯ :
            Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C) (𝟭 (Functor.{v, v_1, u, u_1} C D)) ⥤
              Functor.{v, v_1, u, u_1} (WithInitial C) D })
        y)
    (Functor.map (𝟭 (Functor.{v, v_1, u, u_1} (WithInitial C) D)) f ≫
      Iso.hom
        ((fun (F : Functor.{v, v_1, u, u_1} (WithInitial C) D) ↦
            (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (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.IsInitial.to starInitial (of x))) ⋯))
          y))
    (Iso.hom
        ((fun (F : Functor.{v, v_1, u, u_1} (WithInitial C) D) ↦
            (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (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.IsInitial.to starInitial (of x))) ⋯))
          x) ≫
      Functor.map
        ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithInitial C) D} ↦ mkCommaMorphism,
            map_id := ⋯, map_comp := ⋯ :
            Functor.{v, v_1, u, u_1} (WithInitial C) D ⥤
              Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                (𝟭 (Functor.{v, v_1, u, u_1} C D)) } ⋙
          { obj := ofCommaObject,
            map :=
              fun
                {X Y :
                  Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                    (𝟭 (Functor.{v, v_1, u, u_1} C D))} ↦
              ofCommaMorphism,
            map_id := ⋯, map_comp := ⋯ :
            Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C) (𝟭 (Functor.{v, v_1, u, u_1} C D)) ⥤
              Functor.{v, v_1, u, u_1} (WithInitial C) D })
        f)

Tactic:
ext t