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

Tactic:
cases x