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