-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x_1 y_1 : (WithInitial C)ᵒᵖ
f_1 : x_1 ⟶ y_1
x y : C
f : op (of x) ⟶ op (of y)
simp : f = down (WithTerminal.down (unop f)).op
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) (op (of x)) ⟶
      Functor.obj.{v, v, u, u}
        (Functor.comp (D := WithTerminal Cᵒᵖ)
          {
            obj := fun (x : (WithInitial C)ᵒᵖ) ↦
              match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
              | op x =>
                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star,
            map := fun {x y : (WithInitial C)ᵒᵖ} (x_2 : x ⟶ y) ↦
              match (motive :=
                (x ⟶ y) →
                  Quiver.Hom (V := WithTerminal Cᵒᵖ)
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                      | op x =>
                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star :
                      WithTerminal Cᵒᵖ)
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                      | op x =>
                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star :
                      WithTerminal Cᵒᵖ))
                x_2 with
              | op f =>
                match (motive :=
                  (x y : (WithInitial C)ᵒᵖ) →
                    (unop y ⟶ unop x) →
                      (x ⟶ y) →
                        Quiver.Hom (V := WithTerminal Cᵒᵖ)
                          (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                            | op x =>
                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                              | of x => WithTerminal.of (op x)
                              | star => WithTerminal.star :
                            WithTerminal Cᵒᵖ)
                          (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                            | op x =>
                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                              | of x => WithTerminal.of (op x)
                              | star => WithTerminal.star :
                            WithTerminal Cᵒᵖ))
                  x, y, f, x_2 with
                | op (of x), op (of y), f, x_3 => (WithTerminal.down f).op
                | op (of a), op star, x, x_3 =>
                  Limits.IsTerminal.from WithTerminal.starTerminal
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
                    | op x =>
                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star)
                | op star, op star, x, x_3 =>
                  𝟙
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
                    | op x =>
                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star),
            map_id := ⋯, map_comp := ⋯ }
          {
            obj := fun (x : WithTerminal Cᵒᵖ) ↦
              match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
              | WithTerminal.of x => op (of (unop x))
              | WithTerminal.star => op star,
            map := fun {x y : WithTerminal Cᵒᵖ} (f : x ⟶ y) ↦
              match (motive :=
                (x y : WithTerminal Cᵒᵖ) →
                  (x ⟶ y) →
                    Quiver.Hom (V := (WithInitial C)ᵒᵖ)
                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                        | WithTerminal.of x => op (of (unop x))
                        | WithTerminal.star => op star :
                        (WithInitial C)ᵒᵖ)
                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                        | WithTerminal.of x => op (of (unop x))
                        | WithTerminal.star => op star :
                        (WithInitial C)ᵒᵖ))
                x, y, f with
              | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
              | WithTerminal.of (op unop), WithTerminal.star, x =>
                op
                  (Limits.IsInitial.to starInitial
                    (Opposite.unop
                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of (op unop) with
                      | WithTerminal.of x => op (of (Opposite.unop x))
                      | WithTerminal.star => op star)))
              | WithTerminal.star, WithTerminal.star, x =>
                𝟙
                  (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
                  | WithTerminal.of x => op (of (unop x))
                  | WithTerminal.star => op star),
            map_id := ⋯, map_comp := ⋯ })
        (op (of y)))
    (Functor.map (𝟭 (WithInitial C)ᵒᵖ) f ≫
      Iso.hom
        ((fun (x : (WithInitial C)ᵒᵖ) ↦
            (match (motive :=
                (x : (WithInitial C)ᵒᵖ) →
                  Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) x ≅
                    Functor.obj.{v, v, u, u}
                      (Functor.comp (D := WithTerminal Cᵒᵖ)
                        {
                          obj := fun (x : (WithInitial C)ᵒᵖ) ↦
                            match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                            | op x =>
                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                              | of x => WithTerminal.of (op x)
                              | star => WithTerminal.star,
                          map := fun {x y : (WithInitial C)ᵒᵖ} (x_2 : x ⟶ y) ↦
                            match (motive :=
                              (x ⟶ y) →
                                Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                    | op x =>
                                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star :
                                    WithTerminal Cᵒᵖ)
                                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                    | op x =>
                                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star :
                                    WithTerminal Cᵒᵖ))
                              x_2 with
                            | op f =>
                              match (motive :=
                                (x y : (WithInitial C)ᵒᵖ) →
                                  (unop y ⟶ unop x) →
                                    (x ⟶ y) →
                                      Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                        (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                          | op x =>
                                            match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                            | of x => WithTerminal.of (op x)
                                            | star => WithTerminal.star :
                                          WithTerminal Cᵒᵖ)
                                        (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                          | op x =>
                                            match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                            | of x => WithTerminal.of (op x)
                                            | star => WithTerminal.star :
                                          WithTerminal Cᵒᵖ))
                                x, y, f, x_2 with
                              | op (of x), op (of y), f, x_3 => (WithTerminal.down f).op
                              | op (of a), op star, x, x_3 =>
                                Limits.IsTerminal.from WithTerminal.starTerminal
                                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
                                  | op x =>
                                    match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                    | of x => WithTerminal.of (op x)
                                    | star => WithTerminal.star)
                              | op star, op star, x, x_3 =>
                                𝟙
                                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
                                  | op x =>
                                    match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                    | of x => WithTerminal.of (op x)
                                    | star => WithTerminal.star),
                          map_id := ⋯, map_comp := ⋯ }
                        {
                          obj := fun (x : WithTerminal Cᵒᵖ) ↦
                            match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                            | WithTerminal.of x => op (of (unop x))
                            | WithTerminal.star => op star,
                          map := fun {x y : WithTerminal Cᵒᵖ} (f : x ⟶ y) ↦
                            match (motive :=
                              (x y : WithTerminal Cᵒᵖ) →
                                (x ⟶ y) →
                                  Quiver.Hom (V := (WithInitial C)ᵒᵖ)
                                    (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                                      | WithTerminal.of x => op (of (unop x))
                                      | WithTerminal.star => op star :
                                      (WithInitial C)ᵒᵖ)
                                    (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                                      | WithTerminal.of x => op (of (unop x))
                                      | WithTerminal.star => op star :
                                      (WithInitial C)ᵒᵖ))
                              x, y, f with
                            | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
                            | WithTerminal.of (op unop), WithTerminal.star, x =>
                              op
                                (Limits.IsInitial.to starInitial
                                  (Opposite.unop
                                    (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ)
                                      WithTerminal.of (op unop) with
                                    | WithTerminal.of x => op (of (Opposite.unop x))
                                    | WithTerminal.star => op star)))
                            | WithTerminal.star, WithTerminal.star, x =>
                              𝟙
                                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
                                | WithTerminal.of x => op (of (unop x))
                                | WithTerminal.star => op star),
                          map_id := ⋯, map_comp := ⋯ })
                      x)
                x with
              | op x =>
                match (motive :=
                  (x : WithInitial C) →
                    Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) (op x) ≅
                      Functor.obj.{v, v, u, u}
                        (Functor.comp (D := WithTerminal Cᵒᵖ)
                          {
                            obj := fun (x : (WithInitial C)ᵒᵖ) ↦
                              match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                              | op x =>
                                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                | of x => WithTerminal.of (op x)
                                | star => WithTerminal.star,
                            map := fun {x y : (WithInitial C)ᵒᵖ} (x_2 : x ⟶ y) ↦
                              match (motive :=
                                (x ⟶ y) →
                                  Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                      | op x =>
                                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                        | of x => WithTerminal.of (op x)
                                        | star => WithTerminal.star :
                                      WithTerminal Cᵒᵖ)
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                      | op x =>
                                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                        | of x => WithTerminal.of (op x)
                                        | star => WithTerminal.star :
                                      WithTerminal Cᵒᵖ))
                                x_2 with
                              | op f =>
                                match (motive :=
                                  (x y : (WithInitial C)ᵒᵖ) →
                                    (unop y ⟶ unop x) →
                                      (x ⟶ y) →
                                        Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                          (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                            | op x =>
                                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                              | of x => WithTerminal.of (op x)
                                              | star => WithTerminal.star :
                                            WithTerminal Cᵒᵖ)
                                          (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                            | op x =>
                                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                              | of x => WithTerminal.of (op x)
                                              | star => WithTerminal.star :
                                            WithTerminal Cᵒᵖ))
                                  x, y, f, x_2 with
                                | op (of x), op (of y), f, x_3 => (WithTerminal.down f).op
                                | op (of a), op star, x, x_3 =>
                                  Limits.IsTerminal.from WithTerminal.starTerminal
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
                                    | op x =>
                                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star)
                                | op star, op star, x, x_3 =>
                                  𝟙
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
                                    | op x =>
                                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star),
                            map_id := ⋯, map_comp := ⋯ }
                          {
                            obj := fun (x : WithTerminal Cᵒᵖ) ↦
                              match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                              | WithTerminal.of x => op (of (unop x))
                              | WithTerminal.star => op star,
                            map := fun {x y : WithTerminal Cᵒᵖ} (f : x ⟶ y) ↦
                              match (motive :=
                                (x y : WithTerminal Cᵒᵖ) →
                                  (x ⟶ y) →
                                    Quiver.Hom (V := (WithInitial C)ᵒᵖ)
                                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                                        | WithTerminal.of x => op (of (unop x))
                                        | WithTerminal.star => op star :
                                        (WithInitial C)ᵒᵖ)
                                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                                        | WithTerminal.of x => op (of (unop x))
                                        | WithTerminal.star => op star :
                                        (WithInitial C)ᵒᵖ))
                                x, y, f with
                              | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
                              | WithTerminal.of (op unop), WithTerminal.star, x =>
                                op
                                  (Limits.IsInitial.to starInitial
                                    (Opposite.unop
                                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ)
                                        WithTerminal.of (op unop) with
                                      | WithTerminal.of x => op (of (Opposite.unop x))
                                      | WithTerminal.star => op star)))
                              | WithTerminal.star, WithTerminal.star, x =>
                                𝟙
                                  (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
                                  | WithTerminal.of x => op (of (unop x))
                                  | WithTerminal.star => op star),
                            map_id := ⋯, map_comp := ⋯ })
                        (op x))
                  x with
                | of x => Iso.refl (Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) (op (of x)))
                | star => Iso.refl (Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) (op star)) :
              Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) x ≅
                Functor.obj.{v, v, u, u}
                  (Functor.comp (D := WithTerminal Cᵒᵖ)
                    {
                      obj := fun (x : (WithInitial C)ᵒᵖ) ↦
                        match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                        | op x =>
                          match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                          | of x => WithTerminal.of (op x)
                          | star => WithTerminal.star,
                      map := fun {x y : (WithInitial C)ᵒᵖ} (x_2 : x ⟶ y) ↦
                        match (motive :=
                          (x ⟶ y) →
                            Quiver.Hom (V := WithTerminal Cᵒᵖ)
                              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                | op x =>
                                  match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                  | of x => WithTerminal.of (op x)
                                  | star => WithTerminal.star :
                                WithTerminal Cᵒᵖ)
                              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                | op x =>
                                  match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                  | of x => WithTerminal.of (op x)
                                  | star => WithTerminal.star :
                                WithTerminal Cᵒᵖ))
                          x_2 with
                        | op f =>
                          match (motive :=
                            (x y : (WithInitial C)ᵒᵖ) →
                              (unop y ⟶ unop x) →
                                (x ⟶ y) →
                                  Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                      | op x =>
                                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                        | of x => WithTerminal.of (op x)
                                        | star => WithTerminal.star :
                                      WithTerminal Cᵒᵖ)
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                      | op x =>
                                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                        | of x => WithTerminal.of (op x)
                                        | star => WithTerminal.star :
                                      WithTerminal Cᵒᵖ))
                            x, y, f, x_2 with
                          | op (of x), op (of y), f, x_3 => (WithTerminal.down f).op
                          | op (of a), op star, x, x_3 =>
                            Limits.IsTerminal.from WithTerminal.starTerminal
                              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
                              | op x =>
                                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                | of x => WithTerminal.of (op x)
                                | star => WithTerminal.star)
                          | op star, op star, x, x_3 =>
                            𝟙
                              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
                              | op x =>
                                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                | of x => WithTerminal.of (op x)
                                | star => WithTerminal.star),
                      map_id := ⋯, map_comp := ⋯ }
                    {
                      obj := fun (x : WithTerminal Cᵒᵖ) ↦
                        match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                        | WithTerminal.of x => op (of (unop x))
                        | WithTerminal.star => op star,
                      map := fun {x y : WithTerminal Cᵒᵖ} (f : x ⟶ y) ↦
                        match (motive :=
                          (x y : WithTerminal Cᵒᵖ) →
                            (x ⟶ y) →
                              Quiver.Hom (V := (WithInitial C)ᵒᵖ)
                                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                                  | WithTerminal.of x => op (of (unop x))
                                  | WithTerminal.star => op star :
                                  (WithInitial C)ᵒᵖ)
                                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                                  | WithTerminal.of x => op (of (unop x))
                                  | WithTerminal.star => op star :
                                  (WithInitial C)ᵒᵖ))
                          x, y, f with
                        | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
                        | WithTerminal.of (op unop), WithTerminal.star, x =>
                          op
                            (Limits.IsInitial.to starInitial
                              (Opposite.unop
                                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of (op unop) with
                                | WithTerminal.of x => op (of (Opposite.unop x))
                                | WithTerminal.star => op star)))
                        | WithTerminal.star, WithTerminal.star, x =>
                          𝟙
                            (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
                            | WithTerminal.of x => op (of (unop x))
                            | WithTerminal.star => op star),
                      map_id := ⋯, map_comp := ⋯ })
                  x))
          (op (of y))))
    (Iso.hom
        ((fun (x : (WithInitial C)ᵒᵖ) ↦
            (match (motive :=
                (x : (WithInitial C)ᵒᵖ) →
                  Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) x ≅
                    Functor.obj.{v, v, u, u}
                      (Functor.comp (D := WithTerminal Cᵒᵖ)
                        {
                          obj := fun (x : (WithInitial C)ᵒᵖ) ↦
                            match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                            | op x =>
                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                              | of x => WithTerminal.of (op x)
                              | star => WithTerminal.star,
                          map := fun {x y : (WithInitial C)ᵒᵖ} (x_2 : x ⟶ y) ↦
                            match (motive :=
                              (x ⟶ y) →
                                Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                    | op x =>
                                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star :
                                    WithTerminal Cᵒᵖ)
                                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                    | op x =>
                                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star :
                                    WithTerminal Cᵒᵖ))
                              x_2 with
                            | op f =>
                              match (motive :=
                                (x y : (WithInitial C)ᵒᵖ) →
                                  (unop y ⟶ unop x) →
                                    (x ⟶ y) →
                                      Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                        (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                          | op x =>
                                            match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                            | of x => WithTerminal.of (op x)
                                            | star => WithTerminal.star :
                                          WithTerminal Cᵒᵖ)
                                        (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                          | op x =>
                                            match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                            | of x => WithTerminal.of (op x)
                                            | star => WithTerminal.star :
                                          WithTerminal Cᵒᵖ))
                                x, y, f, x_2 with
                              | op (of x), op (of y), f, x_3 => (WithTerminal.down f).op
                              | op (of a), op star, x, x_3 =>
                                Limits.IsTerminal.from WithTerminal.starTerminal
                                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
                                  | op x =>
                                    match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                    | of x => WithTerminal.of (op x)
                                    | star => WithTerminal.star)
                              | op star, op star, x, x_3 =>
                                𝟙
                                  (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
                                  | op x =>
                                    match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                    | of x => WithTerminal.of (op x)
                                    | star => WithTerminal.star),
                          map_id := ⋯, map_comp := ⋯ }
                        {
                          obj := fun (x : WithTerminal Cᵒᵖ) ↦
                            match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                            | WithTerminal.of x => op (of (unop x))
                            | WithTerminal.star => op star,
                          map := fun {x y : WithTerminal Cᵒᵖ} (f : x ⟶ y) ↦
                            match (motive :=
                              (x y : WithTerminal Cᵒᵖ) →
                                (x ⟶ y) →
                                  Quiver.Hom (V := (WithInitial C)ᵒᵖ)
                                    (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                                      | WithTerminal.of x => op (of (unop x))
                                      | WithTerminal.star => op star :
                                      (WithInitial C)ᵒᵖ)
                                    (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                                      | WithTerminal.of x => op (of (unop x))
                                      | WithTerminal.star => op star :
                                      (WithInitial C)ᵒᵖ))
                              x, y, f with
                            | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
                            | WithTerminal.of (op unop), WithTerminal.star, x =>
                              op
                                (Limits.IsInitial.to starInitial
                                  (Opposite.unop
                                    (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ)
                                      WithTerminal.of (op unop) with
                                    | WithTerminal.of x => op (of (Opposite.unop x))
                                    | WithTerminal.star => op star)))
                            | WithTerminal.star, WithTerminal.star, x =>
                              𝟙
                                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
                                | WithTerminal.of x => op (of (unop x))
                                | WithTerminal.star => op star),
                          map_id := ⋯, map_comp := ⋯ })
                      x)
                x with
              | op x =>
                match (motive :=
                  (x : WithInitial C) →
                    Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) (op x) ≅
                      Functor.obj.{v, v, u, u}
                        (Functor.comp (D := WithTerminal Cᵒᵖ)
                          {
                            obj := fun (x : (WithInitial C)ᵒᵖ) ↦
                              match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                              | op x =>
                                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                | of x => WithTerminal.of (op x)
                                | star => WithTerminal.star,
                            map := fun {x y : (WithInitial C)ᵒᵖ} (x_2 : x ⟶ y) ↦
                              match (motive :=
                                (x ⟶ y) →
                                  Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                      | op x =>
                                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                        | of x => WithTerminal.of (op x)
                                        | star => WithTerminal.star :
                                      WithTerminal Cᵒᵖ)
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                      | op x =>
                                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                        | of x => WithTerminal.of (op x)
                                        | star => WithTerminal.star :
                                      WithTerminal Cᵒᵖ))
                                x_2 with
                              | op f =>
                                match (motive :=
                                  (x y : (WithInitial C)ᵒᵖ) →
                                    (unop y ⟶ unop x) →
                                      (x ⟶ y) →
                                        Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                          (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                            | op x =>
                                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                              | of x => WithTerminal.of (op x)
                                              | star => WithTerminal.star :
                                            WithTerminal Cᵒᵖ)
                                          (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                            | op x =>
                                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                              | of x => WithTerminal.of (op x)
                                              | star => WithTerminal.star :
                                            WithTerminal Cᵒᵖ))
                                  x, y, f, x_2 with
                                | op (of x), op (of y), f, x_3 => (WithTerminal.down f).op
                                | op (of a), op star, x, x_3 =>
                                  Limits.IsTerminal.from WithTerminal.starTerminal
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
                                    | op x =>
                                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star)
                                | op star, op star, x, x_3 =>
                                  𝟙
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
                                    | op x =>
                                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                      | of x => WithTerminal.of (op x)
                                      | star => WithTerminal.star),
                            map_id := ⋯, map_comp := ⋯ }
                          {
                            obj := fun (x : WithTerminal Cᵒᵖ) ↦
                              match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                              | WithTerminal.of x => op (of (unop x))
                              | WithTerminal.star => op star,
                            map := fun {x y : WithTerminal Cᵒᵖ} (f : x ⟶ y) ↦
                              match (motive :=
                                (x y : WithTerminal Cᵒᵖ) →
                                  (x ⟶ y) →
                                    Quiver.Hom (V := (WithInitial C)ᵒᵖ)
                                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                                        | WithTerminal.of x => op (of (unop x))
                                        | WithTerminal.star => op star :
                                        (WithInitial C)ᵒᵖ)
                                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                                        | WithTerminal.of x => op (of (unop x))
                                        | WithTerminal.star => op star :
                                        (WithInitial C)ᵒᵖ))
                                x, y, f with
                              | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
                              | WithTerminal.of (op unop), WithTerminal.star, x =>
                                op
                                  (Limits.IsInitial.to starInitial
                                    (Opposite.unop
                                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ)
                                        WithTerminal.of (op unop) with
                                      | WithTerminal.of x => op (of (Opposite.unop x))
                                      | WithTerminal.star => op star)))
                              | WithTerminal.star, WithTerminal.star, x =>
                                𝟙
                                  (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
                                  | WithTerminal.of x => op (of (unop x))
                                  | WithTerminal.star => op star),
                            map_id := ⋯, map_comp := ⋯ })
                        (op x))
                  x with
                | of x => Iso.refl (Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) (op (of x)))
                | star => Iso.refl (Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) (op star)) :
              Functor.obj.{v, v, u, u} (𝟭 (WithInitial C)ᵒᵖ) x ≅
                Functor.obj.{v, v, u, u}
                  (Functor.comp (D := WithTerminal Cᵒᵖ)
                    {
                      obj := fun (x : (WithInitial C)ᵒᵖ) ↦
                        match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                        | op x =>
                          match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                          | of x => WithTerminal.of (op x)
                          | star => WithTerminal.star,
                      map := fun {x y : (WithInitial C)ᵒᵖ} (x_2 : x ⟶ y) ↦
                        match (motive :=
                          (x ⟶ y) →
                            Quiver.Hom (V := WithTerminal Cᵒᵖ)
                              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                | op x =>
                                  match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                  | of x => WithTerminal.of (op x)
                                  | star => WithTerminal.star :
                                WithTerminal Cᵒᵖ)
                              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                | op x =>
                                  match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                  | of x => WithTerminal.of (op x)
                                  | star => WithTerminal.star :
                                WithTerminal Cᵒᵖ))
                          x_2 with
                        | op f =>
                          match (motive :=
                            (x y : (WithInitial C)ᵒᵖ) →
                              (unop y ⟶ unop x) →
                                (x ⟶ y) →
                                  Quiver.Hom (V := WithTerminal Cᵒᵖ)
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                                      | op x =>
                                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                        | of x => WithTerminal.of (op x)
                                        | star => WithTerminal.star :
                                      WithTerminal Cᵒᵖ)
                                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                                      | op x =>
                                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                        | of x => WithTerminal.of (op x)
                                        | star => WithTerminal.star :
                                      WithTerminal Cᵒᵖ))
                            x, y, f, x_2 with
                          | op (of x), op (of y), f, x_3 => (WithTerminal.down f).op
                          | op (of a), op star, x, x_3 =>
                            Limits.IsTerminal.from WithTerminal.starTerminal
                              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
                              | op x =>
                                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                | of x => WithTerminal.of (op x)
                                | star => WithTerminal.star)
                          | op star, op star, x, x_3 =>
                            𝟙
                              (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
                              | op x =>
                                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                                | of x => WithTerminal.of (op x)
                                | star => WithTerminal.star),
                      map_id := ⋯, map_comp := ⋯ }
                    {
                      obj := fun (x : WithTerminal Cᵒᵖ) ↦
                        match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                        | WithTerminal.of x => op (of (unop x))
                        | WithTerminal.star => op star,
                      map := fun {x y : WithTerminal Cᵒᵖ} (f : x ⟶ y) ↦
                        match (motive :=
                          (x y : WithTerminal Cᵒᵖ) →
                            (x ⟶ y) →
                              Quiver.Hom (V := (WithInitial C)ᵒᵖ)
                                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                                  | WithTerminal.of x => op (of (unop x))
                                  | WithTerminal.star => op star :
                                  (WithInitial C)ᵒᵖ)
                                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                                  | WithTerminal.of x => op (of (unop x))
                                  | WithTerminal.star => op star :
                                  (WithInitial C)ᵒᵖ))
                          x, y, f with
                        | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
                        | WithTerminal.of (op unop), WithTerminal.star, x =>
                          op
                            (Limits.IsInitial.to starInitial
                              (Opposite.unop
                                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of (op unop) with
                                | WithTerminal.of x => op (of (Opposite.unop x))
                                | WithTerminal.star => op star)))
                        | WithTerminal.star, WithTerminal.star, x =>
                          𝟙
                            (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
                            | WithTerminal.of x => op (of (unop x))
                            | WithTerminal.star => op star),
                      map_id := ⋯, map_comp := ⋯ })
                  x))
          (op (of x))) ≫
      Functor.map
        (Functor.comp (D := WithTerminal Cᵒᵖ)
          {
            obj := fun (x : (WithInitial C)ᵒᵖ) ↦
              match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
              | op x =>
                match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                | of x => WithTerminal.of (op x)
                | star => WithTerminal.star,
            map := fun {x y : (WithInitial C)ᵒᵖ} (x_2 : x ⟶ y) ↦
              match (motive :=
                (x ⟶ y) →
                  Quiver.Hom (V := WithTerminal Cᵒᵖ)
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                      | op x =>
                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star :
                      WithTerminal Cᵒᵖ)
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                      | op x =>
                        match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star :
                      WithTerminal Cᵒᵖ))
                x_2 with
              | op f =>
                match (motive :=
                  (x y : (WithInitial C)ᵒᵖ) →
                    (unop y ⟶ unop x) →
                      (x ⟶ y) →
                        Quiver.Hom (V := WithTerminal Cᵒᵖ)
                          (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) x with
                            | op x =>
                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                              | of x => WithTerminal.of (op x)
                              | star => WithTerminal.star :
                            WithTerminal Cᵒᵖ)
                          (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) y with
                            | op x =>
                              match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                              | of x => WithTerminal.of (op x)
                              | star => WithTerminal.star :
                            WithTerminal Cᵒᵖ))
                  x, y, f, x_2 with
                | op (of x), op (of y), f, x_3 => (WithTerminal.down f).op
                | op (of a), op star, x, x_3 =>
                  Limits.IsTerminal.from WithTerminal.starTerminal
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op (of a) with
                    | op x =>
                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star)
                | op star, op star, x, x_3 =>
                  𝟙
                    (match (motive := (WithInitial C)ᵒᵖ → WithTerminal Cᵒᵖ) op star with
                    | op x =>
                      match (motive := WithInitial C → WithTerminal Cᵒᵖ) x with
                      | of x => WithTerminal.of (op x)
                      | star => WithTerminal.star),
            map_id := ⋯, map_comp := ⋯ : Functor.{v, v, u, u} (WithInitial C)ᵒᵖ (WithTerminal Cᵒᵖ) }
          {
            obj := fun (x : WithTerminal Cᵒᵖ) ↦
              match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
              | WithTerminal.of x => op (of (unop x))
              | WithTerminal.star => op star,
            map := fun {x y : WithTerminal Cᵒᵖ} (f : x ⟶ y) ↦
              match (motive :=
                (x y : WithTerminal Cᵒᵖ) →
                  (x ⟶ y) →
                    Quiver.Hom (V := (WithInitial C)ᵒᵖ)
                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                        | WithTerminal.of x => op (of (unop x))
                        | WithTerminal.star => op star :
                        (WithInitial C)ᵒᵖ)
                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                        | WithTerminal.of x => op (of (unop x))
                        | WithTerminal.star => op star :
                        (WithInitial C)ᵒᵖ))
                x, y, f with
              | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
              | WithTerminal.of (op unop), WithTerminal.star, x =>
                op
                  (Limits.IsInitial.to starInitial
                    (Opposite.unop
                      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of (op unop) with
                      | WithTerminal.of x => op (of (Opposite.unop x))
                      | WithTerminal.star => op star)))
              | WithTerminal.star, WithTerminal.star, x =>
                𝟙
                  (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
                  | WithTerminal.of x => op (of (unop x))
                  | WithTerminal.star => op star),
            map_id := ⋯, map_comp := ⋯ : Functor.{v, v, u, u} (WithTerminal Cᵒᵖ) (WithInitial C)ᵒᵖ })
        f)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj,
              Functor.id_map, Iso.refl_hom, Category.comp_id, Functor.comp_map, Category.id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.id_map, CategoryTheory.Category.comp_id, CategoryTheory.Functor.id_obj, CategoryTheory.Iso.refl_hom, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp