-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
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
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)) ⋯)) :
      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)) ⋯ ≫ 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)
⊢ 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)

Tactic:
ext