-- 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
t : WithInitial C
w :
  ∀ (a : C),
    Eq (α :=
      (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithInitial C) D)) x).obj (of a) ⟶
        (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
          (of a))
      (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))
        (of a))
      (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)
        (of a))
w₁ :
  Eq (α :=
    (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithInitial C) D)) x).obj star ⟶
      (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
        star)
    (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))
      star)
    (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)
      star)
⊢ 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)

Tactic:
cases t