-- 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 ⥤ Under.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t t₁ t₂ : Cocone K
f : t₁ ⟶ t₂
a : J
⊢ Eq.{v₁ + 1} (α :=
    (Functor.obj liftFromUnder K).obj (of a) ⟶
      Cocone.pt.{w', v₁, w, u₁} (J := WithInitial J) (F := Functor.obj liftFromUnder K)
        { pt := t₂.pt.right,
          ι :=
            {
              app := fun (x : WithInitial J) ↦
                match (motive :=
                  (x : WithInitial J) →
                    (Functor.obj liftFromUnder K).obj x ⟶
                      Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t₂.pt.right) x)
                  x with
                | of a => Under.Hom.right (t₂.ι.app a)
                | star => t₂.pt.hom,
              naturality := ⋯ } })
    (NatTrans.app
          (Cocone.ι
            { pt := t₁.pt.right,
              ι :=
                {
                  app := fun (x : WithInitial J) ↦
                    match (motive :=
                      (x : WithInitial J) →
                        (Functor.obj liftFromUnder K).obj x ⟶
                          Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t₁.pt.right) x)
                      x with
                    | of a => Under.Hom.right (t₁.ι.app a)
                    | star => t₁.pt.hom,
                  naturality := ⋯ } })
          (of a) ≫
        Under.Hom.right f.hom :
      (Functor.obj liftFromUnder K).obj (of a) ⟶
        Cocone.pt.{w', v₁, w, u₁} (J := WithInitial J) (F := Functor.obj liftFromUnder K)
          { pt := t₂.pt.right,
            ι :=
              {
                app := fun (x : WithInitial J) ↦
                  match (motive :=
                    (x : WithInitial J) →
                      (Functor.obj liftFromUnder K).obj x ⟶
                        Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t₂.pt.right) x)
                    x with
                  | of a => Under.Hom.right (t₂.ι.app a)
                  | star => t₂.pt.hom,
                naturality := ⋯ } })
    (NatTrans.app
        (Cocone.ι
          { pt := t₂.pt.right,
            ι :=
              {
                app := fun (x : WithInitial J) ↦
                  match (motive :=
                    (x : WithInitial J) →
                      (Functor.obj liftFromUnder K).obj x ⟶
                        Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t₂.pt.right) x)
                    x with
                  | of a => Under.Hom.right (t₂.ι.app a)
                  | star => t₂.pt.hom,
                naturality := ⋯ } })
        (of a) :
      (Functor.obj liftFromUnder K).obj (of a) ⟶
        Functor.obj.{w', v₁, w, u₁}
          (Functor.obj (Functor.const (WithInitial J))
            (Cocone.pt.{w', v₁, w, u₁} (J := WithInitial J) (F := Functor.obj liftFromUnder K)
              { pt := t₂.pt.right,
                ι :=
                  {
                    app := fun (x : WithInitial J) ↦
                      match (motive :=
                        (x : WithInitial J) →
                          (Functor.obj liftFromUnder K).obj x ⟶
                            Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t₂.pt.right) x)
                        x with
                      | of a => Under.Hom.right (t₂.ι.app a)
                      | star => t₂.pt.hom,
                    naturality := ⋯ :
                    NatTrans (Functor.obj liftFromUnder K) (Functor.obj (Functor.const (WithInitial J)) t₂.pt.right) } :
                Cocone (Functor.obj liftFromUnder K) }))
          (of a))

Tactic:
simp [← Comma.comp_right]

Premises used: CategoryTheory.Comma.comp_right