Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : Cᵒᵖ
⊢ (match WithTerminal.of a✝, WithTerminal.of a✝, 𝟙 (WithTerminal.of a✝) with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match WithTerminal.of a✝ with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

pp: case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (match WithTerminal.star, WithTerminal.star, 𝟙 WithTerminal.star with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match WithTerminal.star with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

Tactic:
<;>

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : Cᵒᵖ
⊢ (match WithTerminal.of a✝, WithTerminal.of a✝, 𝟙 (WithTerminal.of a✝) with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match WithTerminal.of a✝ with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (match WithTerminal.star, WithTerminal.star, 𝟙 WithTerminal.star with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match WithTerminal.star with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)