-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Cone (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Under.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t : Cocone K
t₁ t₂ : Cocone (Functor.obj liftFromUnder K)
f : t₁ ⟶ t₂
j : J
⊢ Eq (α :=
    K.obj j ⟶
      Cocone.pt (J := J) (F := K)
        {
          pt :=
            Under.mk (Y :=
              Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt) star)
              (t₂.ι.app star),
          ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } })
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := J) (F := K)
          {
            pt :=
              Under.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₁.pt)
                  star)
                (t₁.ι.app star),
            ι := { app := fun (a : J) ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } })
        (NatTrans.app
          (Cocone.ι
            {
              pt :=
                Under.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₁.pt)
                    star)
                  (t₁.ι.app star),
              ι := { app := fun (a : J) ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } })
          j)
        (Under.homMk f.hom ⋯) :
      K.obj j ⟶
        Cocone.pt (J := J) (F := K)
          {
            pt :=
              Under.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                  star)
                (t₂.ι.app star),
            ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } })
    (NatTrans.app
        (Cocone.ι
          {
            pt :=
              Under.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                  star)
                (t₂.ι.app star),
            ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } })
        j :
      K.obj j ⟶
        Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (J := J) (F := K)
              {
                pt :=
                  Under.mk (Y :=
                    Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                      star)
                    (t₂.ι.app star),
                ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } }))
          j)
have h : Eq (α :=
  (K.obj j).right ⟶
    Under.right (X := X)
      (Cocone.pt (J := J) (F := K)
          {
            pt :=
              Under.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                  star)
                (t₂.ι.app star),
            ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) sorry, naturality := sorry } } :
        Under.{v₁, u₁} X))
  (Under.Hom.right
      (CategoryStruct.comp (Y :=
        Cocone.pt (J := J) (F := K)
          {
            pt :=
              Under.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₁.pt)
                  star)
                (t₁.ι.app star),
            ι := { app := fun (a : J) ↦ Under.homMk (t₁.ι.app (of a)) sorry, naturality := sorry } })
        (NatTrans.app
          (Cocone.ι
            {
              pt :=
                Under.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₁.pt)
                    star)
                  (t₁.ι.app star),
              ι := { app := fun (a : J) ↦ Under.homMk (t₁.ι.app (of a)) sorry, naturality := sorry } })
          j)
        (Under.homMk f.hom sorry)) :
    (K.obj j).right ⟶
      Under.right (X := X)
        (Cocone.pt (J := J) (F := K)
            {
              pt :=
                Under.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                    star)
                  (t₂.ι.app star),
              ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) sorry, naturality := sorry } } :
          Under.{v₁, u₁} X))
  (Under.Hom.right
      (NatTrans.app
        (Cocone.ι
          {
            pt :=
              Under.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                  star)
                (t₂.ι.app star),
            ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) sorry, naturality := sorry } })
        j) :
    (K.obj j).right ⟶
      Under.right (X := X)
        (Cocone.pt (J := J) (F := K)
            {
              pt :=
                Under.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                    star)
                  (t₂.ι.app star),
              ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) sorry, naturality := sorry } } :
          Under.{v₁, u₁} X))
Tactic: ext