Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝¹ : (WithInitial C)ᵒᵖ
x✝ : WithInitial C
x : C
⊢ {
            obj := fun x ↦
              match x with
              | op x =>
                match x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star,
            map := fun {x y} x_1 ↦
              match x_1 with
              | op f =>
                match x, y, f, x_1 with
                | op (of x), op (of y), f, x_2 => (WithTerminal.down f).op
                | op (of a), op star, x, x_2 =>
                  WithTerminal.starTerminal.from
                    (match op (of a) with
                    | op x =>
                      match x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star)
                | op star, op star, x, x_2 =>
                  𝟙
                    (match op star with
                    | op x =>
                      match x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star),
            map_id := ⋯, map_comp := ⋯ }.map
        ((NatIso.ofComponents
                (fun x ↦
                  match x with
                  | op x =>
                    match x with
                    | of x => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op (of x)))
                    | star => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op star)))
                ⋯).hom.app
          (op (of x))) ≫
      (NatIso.ofComponents
              (fun x ↦
                match x with
                | WithTerminal.of x =>
                  Iso.refl
                    (({
                            obj := fun x ↦
                              match x with
                              | WithTerminal.of x => op (of (unop x))
                              | WithTerminal.star => op star,
                            map := fun {x y} f ↦
                              match x, y, f 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),
                            map_id := ⋯, map_comp := ⋯ } ⋙
                          {
                            obj := fun x ↦
                              match x with
                              | op x =>
                                match x with
                                | of x => WithTerminal.of (op x)
                                | star => WithTerminal.star,
                            map := fun {x y} x_1 ↦
                              match x_1 with
                              | op f =>
                                match x, y, f, x_1 with
                                | op (of x), op (of y), f, x_2 => (WithTerminal.down f).op
                                | op (of a), op star, x, x_2 =>
                                  WithTerminal.starTerminal.from
                                    (match op (of a) with
                                    | op x =>
                                      match x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star)
                                | op star, op star, x, x_2 =>
                                  𝟙
                                    (match op star with
                                    | op x =>
                                      match x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star),
                            map_id := ⋯, map_comp := ⋯ }).obj
                      (WithTerminal.of x))
                | WithTerminal.star =>
                  Iso.refl
                    (({
                            obj := fun x ↦
                              match x with
                              | WithTerminal.of x => op (of (unop x))
                              | WithTerminal.star => op star,
                            map := fun {x y} f ↦
                              match x, y, f 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),
                            map_id := ⋯, map_comp := ⋯ } ⋙
                          {
                            obj := fun x ↦
                              match x with
                              | op x =>
                                match x with
                                | of x => WithTerminal.of (op x)
                                | star => WithTerminal.star,
                            map := fun {x y} x_1 ↦
                              match x_1 with
                              | op f =>
                                match x, y, f, x_1 with
                                | op (of x), op (of y), f, x_2 => (WithTerminal.down f).op
                                | op (of a), op star, x, x_2 =>
                                  WithTerminal.starTerminal.from
                                    (match op (of a) with
                                    | op x =>
                                      match x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star)
                                | op star, op star, x, x_2 =>
                                  𝟙
                                    (match op star with
                                    | op x =>
                                      match x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star),
                            map_id := ⋯, map_comp := ⋯ }).obj
                      WithTerminal.star))
              ⋯).hom.app
        ({
              obj := fun x ↦
                match x with
                | op x =>
                  match x with
                  | of x => WithTerminal.of (op x)
                  | star => WithTerminal.star,
              map := fun {x y} x_1 ↦
                match x_1 with
                | op f =>
                  match x, y, f, x_1 with
                  | op (of x), op (of y), f, x_2 => (WithTerminal.down f).op
                  | op (of a), op star, x, x_2 =>
                    WithTerminal.starTerminal.from
                      (match op (of a) with
                      | op x =>
                        match x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star)
                  | op star, op star, x, x_2 =>
                    𝟙
                      (match op star with
                      | op x =>
                        match x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star),
              map_id := ⋯, map_comp := ⋯ }.obj
          (op (of x))) =
    𝟙
      ({
            obj := fun x ↦
              match x with
              | op x =>
                match x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star,
            map := fun {x y} x_1 ↦
              match x_1 with
              | op f =>
                match x, y, f, x_1 with
                | op (of x), op (of y), f, x_2 => (WithTerminal.down f).op
                | op (of a), op star, x, x_2 =>
                  WithTerminal.starTerminal.from
                    (match op (of a) with
                    | op x =>
                      match x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star)
                | op star, op star, x, x_2 =>
                  𝟙
                    (match op star with
                    | op x =>
                      match x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star),
            map_id := ⋯, map_comp := ⋯ }.obj
        (op (of x)))

Tactic:
simp only [op_unop, Functor.id_obj, Functor.comp_obj, NatIso.ofComponents_hom_app,
          Iso.refl_hom, Category.comp_id]
        rfl

Goal state after: