-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x : WithInitial Cᵒᵖ
of :
  ∀ (a : Cᵒᵖ),
    Eq.{v + 1} (α :=
      Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ))
      (match (motive :=
          (x y : WithInitial Cᵒᵖ) →
            (x ⟶ y) →
              Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
                (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
                  | WithInitial.of x => op (WithTerminal.of (unop x))
                  | WithInitial.star => op WithTerminal.star :
                  (WithTerminal C)ᵒᵖ)
                (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) y with
                  | WithInitial.of x => op (WithTerminal.of (unop x))
                  | WithInitial.star => op WithTerminal.star :
                  (WithTerminal C)ᵒᵖ))
          WithInitial.of a, WithInitial.of a, 𝟙 (WithInitial.of a) with
        | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
        | WithInitial.star, WithInitial.of (op unop), x =>
          op
            (Limits.IsTerminal.from starTerminal
              (Opposite.unop
                (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of (op unop) with
                | WithInitial.of x => op (WithTerminal.of (Opposite.unop x))
                | WithInitial.star => op WithTerminal.star)))
        | WithInitial.star, WithInitial.star, x =>
          𝟙
            (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
            | WithInitial.of x => op (WithTerminal.of (unop x))
            | WithInitial.star => op WithTerminal.star) :
        Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
          (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
            | WithInitial.of x => op (WithTerminal.of (unop x))
            | WithInitial.star => op WithTerminal.star :
            (WithTerminal C)ᵒᵖ)
          (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
            | WithInitial.of x => op (WithTerminal.of (unop x))
            | WithInitial.star => op WithTerminal.star :
            (WithTerminal C)ᵒᵖ))
      (𝟙
          (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star) :
        Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
          (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
            | WithInitial.of x => op (WithTerminal.of (unop x))
            | WithInitial.star => op WithTerminal.star :
            (WithTerminal C)ᵒᵖ)
          (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
            | WithInitial.of x => op (WithTerminal.of (unop x))
            | WithInitial.star => op WithTerminal.star :
            (WithTerminal C)ᵒᵖ))
star :
  Eq.{v + 1} (α :=
    Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
      (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
        | WithInitial.of x => op (WithTerminal.of (unop x))
        | WithInitial.star => op WithTerminal.star :
        (WithTerminal C)ᵒᵖ)
      (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
        | WithInitial.of x => op (WithTerminal.of (unop x))
        | WithInitial.star => op WithTerminal.star :
        (WithTerminal C)ᵒᵖ))
    (match (motive :=
        (x y : WithInitial Cᵒᵖ) →
          (x ⟶ y) →
            Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
                | WithInitial.of x => op (WithTerminal.of (unop x))
                | WithInitial.star => op WithTerminal.star :
                (WithTerminal C)ᵒᵖ)
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) y with
                | WithInitial.of x => op (WithTerminal.of (unop x))
                | WithInitial.star => op WithTerminal.star :
                (WithTerminal C)ᵒᵖ))
        WithInitial.star, WithInitial.star, 𝟙 WithInitial.star with
      | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
      | WithInitial.star, WithInitial.of (op unop), x =>
        op
          (Limits.IsTerminal.from starTerminal
            (Opposite.unop
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of (op unop) with
              | WithInitial.of x => op (WithTerminal.of (Opposite.unop x))
              | WithInitial.star => op WithTerminal.star)))
      | WithInitial.star, WithInitial.star, x =>
        𝟙
          (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star) :
      Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ))
    (𝟙
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
        | WithInitial.of x => op (WithTerminal.of (unop x))
        | WithInitial.star => op WithTerminal.star) :
      Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
      (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
        | WithInitial.of x => op (WithTerminal.of (unop x))
        | WithInitial.star => op WithTerminal.star :
        (WithTerminal C)ᵒᵖ)
      (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
        | WithInitial.of x => op (WithTerminal.of (unop x))
        | WithInitial.star => op WithTerminal.star :
        (WithTerminal C)ᵒᵖ))
    (match (motive :=
        (x y : WithInitial Cᵒᵖ) →
          (x ⟶ y) →
            Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
                | WithInitial.of x => op (WithTerminal.of (unop x))
                | WithInitial.star => op WithTerminal.star :
                (WithTerminal C)ᵒᵖ)
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) y with
                | WithInitial.of x => op (WithTerminal.of (unop x))
                | WithInitial.star => op WithTerminal.star :
                (WithTerminal C)ᵒᵖ))
        x, x, 𝟙 x with
      | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
      | WithInitial.star, WithInitial.of (op unop), x =>
        op
          (Limits.IsTerminal.from starTerminal
            (Opposite.unop
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of (op unop) with
              | WithInitial.of x => op (WithTerminal.of (Opposite.unop x))
              | WithInitial.star => op WithTerminal.star)))
      | WithInitial.star, WithInitial.star, x =>
        𝟙
          (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star) :
      Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ))
    (𝟙
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
        | WithInitial.of x => op (WithTerminal.of (unop x))
        | WithInitial.star => op WithTerminal.star) :
      Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
          | WithInitial.of x => op (WithTerminal.of (unop x))
          | WithInitial.star => op WithTerminal.star :
          (WithTerminal C)ᵒᵖ))

Tactic:
cases x