-- 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 ⥤ Over.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t : Cone K
t₁ t₂ : Cone (Functor.obj liftFromOver K)
f : t₁ ⟶ t₂
j : J
⊢ Eq (α :=
    Cone.pt (J := J) (F := K)
        {
          pt :=
            Over.mk (Y :=
              Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₁.pt)
                star)
              (t₁.π.app star),
          π := { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } } ⟶
      K.obj j)
    (CategoryStruct.comp (Y :=
        Cone.pt (J := J) (F := K)
          {
            pt :=
              Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₂.pt)
                  star)
                (t₂.π.app star),
            π := { app := fun (a : J) ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } })
        (Over.homMk f.hom ⋯)
        (NatTrans.app
          (Cone.π
            {
              pt :=
                Over.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₂.pt)
                    star)
                  (t₂.π.app star),
              π := { app := fun (a : J) ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } })
          j) :
      Cone.pt (J := J) (F := K)
          {
            pt :=
              Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₁.pt)
                  star)
                (t₁.π.app star),
            π := { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } } ⟶
        K.obj j)
    (NatTrans.app
        (Cone.π
          {
            pt :=
              Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₁.pt)
                  star)
                (t₁.π.app star),
            π := { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } })
        j :
      Functor.obj
          (Functor.obj (Functor.const J)
            (Cone.pt (J := J) (F := K)
              {
                pt :=
                  Over.mk (Y :=
                    Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J)
                      (Functor.obj (Functor.const (WithTerminal J)) t₁.pt) star)
                    (t₁.π.app star),
                π := { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }))
          j ⟶
        K.obj j)
have h : Eq (α :=
  Over.left (X := X)
      (Cone.pt (J := J) (F := K)
          {
            pt :=
              Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₁.pt)
                  star)
                (t₁.π.app star),
            π :=
              { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) sorry, naturality := sorry :
                NatTrans
                  (Functor.obj (Functor.const J)
                    (Over.mk (Y :=
                      Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J)
                        (Functor.obj (Functor.const (WithTerminal J)) t₁.pt) star)
                      (t₁.π.app star)))
                  K } :
            Cone K } :
        Over.{v₁, u₁} X) ⟶
    (K.obj j).left)
  (Over.Hom.left
      (CategoryStruct.comp (Y :=
        Cone.pt (J := J) (F := K)
          {
            pt :=
              Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₂.pt)
                  star)
                (t₂.π.app star),
            π := { app := fun (a : J) ↦ Over.homMk (t₂.π.app (of a)) sorry, naturality := sorry } })
        (Over.homMk f.hom sorry)
        (NatTrans.app
          (Cone.π
            {
              pt :=
                Over.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₂.pt)
                    star)
                  (t₂.π.app star),
              π := { app := fun (a : J) ↦ Over.homMk (t₂.π.app (of a)) sorry, naturality := sorry } })
          j)) :
    Over.left (X := X)
        (Cone.pt (J := J) (F := K)
            {
              pt :=
                Over.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₁.pt)
                    star)
                  (t₁.π.app star),
              π :=
                { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) sorry, naturality := sorry :
                  NatTrans
                    (Functor.obj (Functor.const J)
                      (Over.mk (Y :=
                        Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J)
                          (Functor.obj (Functor.const (WithTerminal J)) t₁.pt) star)
                        (t₁.π.app star)))
                    K } :
              Cone K } :
          Over.{v₁, u₁} X) ⟶
      (K.obj j).left)
  (Over.Hom.left
      (NatTrans.app
        (Cone.π
          {
            pt :=
              Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₁.pt)
                  star)
                (t₁.π.app star),
            π := { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) sorry, naturality := sorry } })
        j) :
    Over.left (X := X)
        (Cone.pt (J := J) (F := K)
            {
              pt :=
                Over.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₁.pt)
                    star)
                  (t₁.π.app star),
              π :=
                { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) sorry, naturality := sorry :
                  NatTrans
                    (Functor.obj (Functor.const J)
                      (Over.mk (Y :=
                        Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J)
                          (Functor.obj (Functor.const (WithTerminal J)) t₁.pt) star)
                        (t₁.π.app star)))
                    K } :
              Cone K } :
          Over.{v₁, u₁} X) ⟶
      (K.obj j).left)
Tactic: ext