Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : Cᵒᵖ
⊢ (match 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
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match WithInitial.of a✝ with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)

pp: case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (match 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
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match WithInitial.star with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)

Tactic:
<;>

Goal state after:
case of
C : Type u
inst✝ : Category.{v, u} C
a✝ : Cᵒᵖ
⊢ (match 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
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match WithInitial.of a✝ with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)

case star
C : Type u
inst✝ : Category.{v, u} C
⊢ (match 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
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match WithInitial.star with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)