-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
⊢ ∀ (X : Subterminals.{v₁, u₁} C),
    Eq.{v₁ + 1} (α :=
      Quiver.Hom (V := MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C))
        (Functor.obj
          {
            obj := fun (X : Subterminals.{v₁, u₁} C) ↦
              ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
            map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
            map_comp := ⋯ }
          X)
        (Functor.obj
          {
            obj := fun (X : Subterminals.{v₁, u₁} C) ↦
              ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
            map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
            map_comp := ⋯ }
          X))
      (Functor.map
            {
              obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                  (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
              map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
              map_comp := ⋯ }
            (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (X : Subterminals.{v₁, u₁} C) ↦ Iso.refl X) ⋯)) X) ≫
          NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (X : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)) ↦
                  MonoOver.isoMk
                    (Iso.refl
                      (Over.left.{v₁, u₁} (X := terminal.{v₁, u₁} C)
                        (ObjectProperty.FullSubcategory.obj (P := Over.isMono (terminal.{v₁, u₁} C))
                          (Functor.obj
                            (Functor.comp (D := Subterminals.{v₁, u₁} C)
                              {
                                obj := fun (X : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)) ↦
                                  ObjectProperty.FullSubcategory.mk (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)
                                    X.obj (P := Over.isMono (terminal.{v₁, u₁} C)).left ⋯,
                                map := fun {X Y : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)} (f : X ⟶ Y) ↦
                                  ObjectProperty.homMk (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A) f.hom.left,
                                map_id := ⋯, map_comp := ⋯ :
                                MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C) ⥤ Subterminals.{v₁, u₁} C }
                              {
                                obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                                  ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                                    (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
                                map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯,
                                map_id := ⋯, map_comp := ⋯ :
                                Subterminals.{v₁, u₁} C ⥤ MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C) })
                            X))))
                    ⋯)
                ⋯))
            (Functor.obj
              {
                obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                  ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                    (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
                map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
                map_comp := ⋯ : Subterminals.{v₁, u₁} C ⥤ MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C) }
              X) :
        Quiver.Hom (V := MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C))
          (Functor.obj
            {
              obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                  (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
              map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
              map_comp := ⋯ }
            X)
          (Functor.obj
            {
              obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                  (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
              map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
              map_comp := ⋯ }
            X))
      (𝟙
          (Functor.obj
            {
              obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                  (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
              map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
              map_comp := ⋯ }
            X) :
        Quiver.Hom (V := MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C))
          (Functor.obj
            {
              obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                  (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
              map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
              map_comp := ⋯ }
            X)
          (Functor.obj
            {
              obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                  (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
              map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
              map_comp := ⋯ }
            X))

Tactic:
subsingleton