-- 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 : Functor.{v, v_1, u, u_1} (WithInitial C) D
⊢ Eq (α :=
    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)) }
        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)) }
        x)
    (Functor.map
          { obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithInitial C) D} ↦ mkCommaMorphism,
            map_id := ⋯, map_comp := ⋯ }
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (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)) ⋯)
                ⋯))
            x) ≫
        NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun
                  (F :
                    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))) ↦
                Iso.refl
                  (Functor.obj
                    ({ 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 } ⋙
                      { 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)) })
                    F))
              ⋯))
          (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)) }
            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)) }
          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)) }
          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)) }
          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)) }
          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)) }
          x)
have simp : mkCommaMorphism
    (Iso.hom
      (NatIso.ofComponents
        (fun (X : WithInitial C) ↦
          match (motive :=
            (X : WithInitial C) →
              x.obj X ≅
                match (motive := WithInitial C → D) X with
                | of x_1 => x.obj (Functor.obj.{v, v, u, u} incl x_1)
                | star => x.obj star)
            X with
          | of x_1 => Iso.app (Iso.refl (incl ⋙ x)) x_1
          | star => Iso.refl (x.obj star))
        sorry)) =
  𝟙 (mkCommaObject x)
Tactic: simp only [Functor.id_obj, Functor.comp_obj, liftUnique, lift_obj, NatIso.ofComponents_hom_app,
      Iso.refl_hom, Category.comp_id]