-- 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_1 : Cone K
t : Cone (Functor.obj liftFromOver K)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    Functor.obj
        (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)))
        x ⟶
      K.obj x_1)
    (CategoryStruct.comp (Y :=
        Functor.obj
          (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)))
          x_1)
        (Functor.map
          (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)))
          f)
        (Over.homMk (t.π.app (of x_1)) ⋯) :
      Functor.obj
          (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)))
          x ⟶
        K.obj x_1)
    (Over.homMk (t.π.app (of x)) ⋯ ≫ K.map f :
      Functor.obj
          (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)))
          x ⟶
        K.obj x_1)
have h : Eq (α :=
  Over.left (X := X)
      (Functor.obj
          (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)))
          x :
        Over.{v₁, u₁} X) ⟶
    (K.obj x_1).left)
  (Over.Hom.left
      (CategoryStruct.comp (Y :=
        Functor.obj
          (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)))
          x_1)
        (Functor.map
          (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)))
          f)
        (Over.homMk (t.π.app (of x_1)) sorry)) :
    Over.left (X := X)
        (Functor.obj
            (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)))
            x :
          Over.{v₁, u₁} X) ⟶
      (K.obj x_1).left)
  (Over.Hom.left (Over.homMk (t.π.app (of x)) sorry ≫ K.map f) :
    Over.left (X := X)
        (Functor.obj
            (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)))
            x :
          Over.{v₁, u₁} X) ⟶
      (K.obj x_1).left)
Tactic: ext