-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x : WithTerminal Cᵒᵖ
of :
  ∀ (a : Cᵒᵖ),
    Eq.{v + 1} (α :=
      Quiver.Hom (V := (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
          | WithTerminal.of x => op (WithInitial.of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
          | WithTerminal.of x => op (WithInitial.of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ))
      (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 (WithInitial.of (unop x))
                  | WithTerminal.star => op star :
                  (WithInitial C)ᵒᵖ)
                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                  | WithTerminal.of x => op (WithInitial.of (unop x))
                  | WithTerminal.star => op star :
                  (WithInitial C)ᵒᵖ))
          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
            (Limits.IsInitial.to starInitial
              (Opposite.unop
                (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of (op unop) with
                | WithTerminal.of x => op (WithInitial.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 (WithInitial.of (unop x))
            | WithTerminal.star => op star) :
        Quiver.Hom (V := (WithInitial C)ᵒᵖ)
          (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
            | WithTerminal.of x => op (WithInitial.of (unop x))
            | WithTerminal.star => op star :
            (WithInitial C)ᵒᵖ)
          (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
            | WithTerminal.of x => op (WithInitial.of (unop x))
            | WithTerminal.star => op star :
            (WithInitial C)ᵒᵖ))
      (𝟙
          (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
          | WithTerminal.of x => op (WithInitial.of (unop x))
          | WithTerminal.star => op star) :
        Quiver.Hom (V := (WithInitial C)ᵒᵖ)
          (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
            | WithTerminal.of x => op (WithInitial.of (unop x))
            | WithTerminal.star => op star :
            (WithInitial C)ᵒᵖ)
          (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
            | WithTerminal.of x => op (WithInitial.of (unop x))
            | WithTerminal.star => op star :
            (WithInitial C)ᵒᵖ))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
        | WithTerminal.of x => op (WithInitial.of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
        | WithTerminal.of x => op (WithInitial.of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ))
    (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 (WithInitial.of (unop x))
                | WithTerminal.star => op star :
                (WithInitial C)ᵒᵖ)
              (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                | WithTerminal.of x => op (WithInitial.of (unop x))
                | WithTerminal.star => op star :
                (WithInitial C)ᵒᵖ))
        x, x, 𝟙 x 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 (WithInitial.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 (WithInitial.of (unop x))
          | WithTerminal.star => op star) :
      Quiver.Hom (V := (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
          | WithTerminal.of x => op (WithInitial.of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
          | WithTerminal.of x => op (WithInitial.of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ))
    (𝟙
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
        | WithTerminal.of x => op (WithInitial.of (unop x))
        | WithTerminal.star => op star) :
      Quiver.Hom (V := (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
          | WithTerminal.of x => op (WithInitial.of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
          | WithTerminal.of x => op (WithInitial.of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ))
have star : Eq.{v + 1} (α :=
  Quiver.Hom (V := (WithInitial C)ᵒᵖ)
    (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
      | WithTerminal.of x => op (WithInitial.of (unop x))
      | WithTerminal.star => op star :
      (WithInitial C)ᵒᵖ)
    (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
      | WithTerminal.of x => op (WithInitial.of (unop x))
      | WithTerminal.star => op star :
      (WithInitial C)ᵒᵖ))
  (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 (WithInitial.of (unop x))
              | WithTerminal.star => op star :
              (WithInitial C)ᵒᵖ)
            (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
              | WithTerminal.of x => op (WithInitial.of (unop x))
              | WithTerminal.star => op star :
              (WithInitial C)ᵒᵖ))
      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
        (Limits.IsInitial.to starInitial
          (Opposite.unop
            (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of (op unop) with
            | WithTerminal.of x => op (WithInitial.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 (WithInitial.of (unop x))
        | WithTerminal.star => op star) :
    Quiver.Hom (V := (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
        | WithTerminal.of x => op (WithInitial.of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
        | WithTerminal.of x => op (WithInitial.of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ))
  (𝟙
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
      | WithTerminal.of x => op (WithInitial.of (unop x))
      | WithTerminal.star => op star) :
    Quiver.Hom (V := (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
        | WithTerminal.of x => op (WithInitial.of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
        | WithTerminal.of x => op (WithInitial.of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ))
Tactic: cases x
Cleared hypotheses: x