Module: Mathlib.CategoryTheory.WithTerminal.Basic

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

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

Tactic:
<;>

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

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