-- 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 : Cone K
t₁ t₂ : Cone (Functor.obj liftFromOver K)
f : t₁ ⟶ t₂
j : J
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)) ⋯, naturality := ⋯ :
                  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)) ⋯, 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)) :
      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)) ⋯, naturality := ⋯ :
                    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)) ⋯, naturality := ⋯ } })
          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)) ⋯, naturality := ⋯ :
                    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)
⊢ 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)

Tactic:
ext