-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
⊢ ∀ {X Y : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)} (f : X ⟶ Y),
    Eq (α :=
      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 := ⋯ }
            {
              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 (𝟭 (MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C))) Y)
      (Functor.map
          (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) })
          f ≫
        Iso.hom
          ((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 := ⋯ }
                            {
                              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
                    (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 := ⋯ }
                      {
                        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 (𝟭 (MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C))) X))
            Y))
      (Iso.hom
          ((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 := ⋯ }
                            {
                              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
                    (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 := ⋯ }
                      {
                        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 (𝟭 (MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C))) X))
            X) ≫
        Functor.map (𝟭 (MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C))) f)

Tactic:
subsingleton