-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x y z : (WithInitial C)ᵒᵖ
f_1 : unop y ⟶ unop x
g_1 : unop z ⟶ unop y
x_1 x_2 : (WithInitial C)ᵒᵖ
f : unop x_2 ⟶ unop x_1
g : unop (op star) ⟶ unop x_2
x_3 : x_1 ⟶ x_2
x_4 : x_2 ⟶ op star
⊢ Eq (α :=
    Quiver.Hom (V := WithTerminal Cᵒᵖ)
      (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x_1 with
        | op x =>
          match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
          | of x => WithTerminal.of (op x)
          | star => WithTerminal.star :
        WithTerminal Cᵒᵖ)
      (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
        | op x =>
          match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
          | of x => WithTerminal.of (op x)
          | star => WithTerminal.star :
        WithTerminal Cᵒᵖ))
    (match (motive :=
        (x_1 ⟶ op star) →
          Quiver.Hom (V := WithTerminal Cᵒᵖ)
            (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x_1 with
              | op x =>
                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star :
              WithTerminal Cᵒᵖ)
            (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
              | op x =>
                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star :
              WithTerminal Cᵒᵖ))
        op f ≫ op g with
      | op f_2 =>
        match (motive :=
          (x y : (WithInitial C)ᵒᵖ) →
            (unop y ⟶ unop x) →
              (x ⟶ y) →
                Quiver.Hom (V := WithTerminal Cᵒᵖ)
                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                    | op x =>
                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star :
                    WithTerminal Cᵒᵖ)
                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                    | op x =>
                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star :
                    WithTerminal Cᵒᵖ))
          x_1, op star, f_2, op f ≫ op g with
        | op (of x), op (of y), f, x_5 => (WithTerminal.down f).op
        | op (of a), op star, x, x_5 =>
          Limits.IsTerminal.from WithTerminal.starTerminal
            (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
            | op x =>
              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
              | of x => WithTerminal.of (op x)
              | star => WithTerminal.star)
        | op star, op star, x, x_5 =>
          𝟙
            (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
            | op x =>
              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
              | of x => WithTerminal.of (op x)
              | star => WithTerminal.star) :
      Quiver.Hom (V := WithTerminal Cᵒᵖ)
        (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x_1 with
          | op x =>
            match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star :
          WithTerminal Cᵒᵖ)
        (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
          | op x =>
            match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star :
          WithTerminal Cᵒᵖ))
    (CategoryStruct.comp (Y :=
        match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x_2 with
        | op x =>
          match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
          | of x => WithTerminal.of (op x)
          | star => WithTerminal.star)
        (match (motive :=
          (x_1 ⟶ x_2) →
            Quiver.Hom (V := WithTerminal Cᵒᵖ)
              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x_1 with
                | op x =>
                  match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                  | of x => WithTerminal.of (op x)
                  | star => WithTerminal.star :
                WithTerminal Cᵒᵖ)
              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x_2 with
                | op x =>
                  match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                  | of x => WithTerminal.of (op x)
                  | star => WithTerminal.star :
                WithTerminal Cᵒᵖ))
          op f with
        | op f_2 =>
          match (motive :=
            (x y : (WithInitial C)ᵒᵖ) →
              (unop y ⟶ unop x) →
                (x ⟶ y) →
                  Quiver.Hom (V := WithTerminal Cᵒᵖ)
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                      | op x =>
                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star :
                      WithTerminal Cᵒᵖ)
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                      | op x =>
                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star :
                      WithTerminal Cᵒᵖ))
            x_1, x_2, f_2, op f with
          | op (of x), op (of y), f, x_5 => (WithTerminal.down f).op
          | op (of a), op star, x, x_5 =>
            Limits.IsTerminal.from WithTerminal.starTerminal
              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
              | op x =>
                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star)
          | op star, op star, x, x_5 =>
            𝟙
              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
              | op x =>
                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star))
        (match (motive :=
          (x_2 ⟶ op star) →
            Quiver.Hom (V := WithTerminal Cᵒᵖ)
              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x_2 with
                | op x =>
                  match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                  | of x => WithTerminal.of (op x)
                  | star => WithTerminal.star :
                WithTerminal Cᵒᵖ)
              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
                | op x =>
                  match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                  | of x => WithTerminal.of (op x)
                  | star => WithTerminal.star :
                WithTerminal Cᵒᵖ))
          op g with
        | op f =>
          match (motive :=
            (x y : (WithInitial C)ᵒᵖ) →
              (unop y ⟶ unop x) →
                (x ⟶ y) →
                  Quiver.Hom (V := WithTerminal Cᵒᵖ)
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                      | op x =>
                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star :
                      WithTerminal Cᵒᵖ)
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                      | op x =>
                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star :
                      WithTerminal Cᵒᵖ))
            x_2, op star, f, op g with
          | op (of x), op (of y), f, x_5 => (WithTerminal.down f).op
          | op (of a), op star, x, x_5 =>
            Limits.IsTerminal.from WithTerminal.starTerminal
              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
              | op x =>
                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star)
          | op star, op star, x, x_5 =>
            𝟙
              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
              | op x =>
                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star)) :
      Quiver.Hom (V := WithTerminal Cᵒᵖ)
        (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x_1 with
          | op x =>
            match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star :
          WithTerminal Cᵒᵖ)
        (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
          | op x =>
            match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star :
          WithTerminal Cᵒᵖ))

Tactic:
subsingleton