-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
X Z : WalkingParallelPair
g : X ⟶ Z
id :
  Eq (α :=
    Quiver.Hom (V := WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) zero with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one :
        WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) one with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one :
        WalkingReflexivePair))
    (match (motive :=
        (Y X : WalkingParallelPair) →
          (X ⟶ Y) →
            Quiver.Hom (V := WalkingReflexivePair)
              (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
                | one => WalkingReflexivePair.zero
                | zero => WalkingReflexivePair.one :
                WalkingReflexivePair)
              (match (motive := WalkingParallelPair → WalkingReflexivePair) Y with
                | one => WalkingReflexivePair.zero
                | zero => WalkingReflexivePair.one :
                WalkingReflexivePair))
        one, zero, WalkingParallelPairHom.id zero ≫ WalkingParallelPairHom.left with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match (motive := WalkingParallelPair → WalkingReflexivePair) x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one) :
      Quiver.Hom (V := WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) zero with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) one with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingParallelPair → WalkingReflexivePair) zero with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)
        (match (motive :=
          (Y X : WalkingParallelPair) →
            (X ⟶ Y) →
              Quiver.Hom (V := WalkingReflexivePair)
                (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
                  | one => WalkingReflexivePair.zero
                  | zero => WalkingReflexivePair.one :
                  WalkingReflexivePair)
                (match (motive := WalkingParallelPair → WalkingReflexivePair) Y with
                  | one => WalkingReflexivePair.zero
                  | zero => WalkingReflexivePair.one :
                  WalkingReflexivePair))
          zero, zero, WalkingParallelPairHom.id zero with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match (motive := WalkingParallelPair → WalkingReflexivePair) x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one))
        (match (motive :=
          (Y X : WalkingParallelPair) →
            (X ⟶ Y) →
              Quiver.Hom (V := WalkingReflexivePair)
                (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
                  | one => WalkingReflexivePair.zero
                  | zero => WalkingReflexivePair.one :
                  WalkingReflexivePair)
                (match (motive := WalkingParallelPair → WalkingReflexivePair) Y with
                  | one => WalkingReflexivePair.zero
                  | zero => WalkingReflexivePair.one :
                  WalkingReflexivePair))
          one, zero, WalkingParallelPairHom.left with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match (motive := WalkingParallelPair → WalkingReflexivePair) x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)) :
      Quiver.Hom (V := WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) zero with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) one with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair))
⊢ Eq (α :=
    Quiver.Hom (V := WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one :
        WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) Z with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one :
        WalkingReflexivePair))
    (match (motive :=
        (Y X : WalkingParallelPair) →
          (X ⟶ Y) →
            Quiver.Hom (V := WalkingReflexivePair)
              (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
                | one => WalkingReflexivePair.zero
                | zero => WalkingReflexivePair.one :
                WalkingReflexivePair)
              (match (motive := WalkingParallelPair → WalkingReflexivePair) Y with
                | one => WalkingReflexivePair.zero
                | zero => WalkingReflexivePair.one :
                WalkingReflexivePair))
        Z, X, WalkingParallelPairHom.id X ≫ g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match (motive := WalkingParallelPair → WalkingReflexivePair) x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one) :
      Quiver.Hom (V := WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) Z with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingParallelPair → WalkingReflexivePair) X with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)
        (match (motive :=
          (Y X : WalkingParallelPair) →
            (X ⟶ Y) →
              Quiver.Hom (V := WalkingReflexivePair)
                (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
                  | one => WalkingReflexivePair.zero
                  | zero => WalkingReflexivePair.one :
                  WalkingReflexivePair)
                (match (motive := WalkingParallelPair → WalkingReflexivePair) Y with
                  | one => WalkingReflexivePair.zero
                  | zero => WalkingReflexivePair.one :
                  WalkingReflexivePair))
          X, X, WalkingParallelPairHom.id X with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match (motive := WalkingParallelPair → WalkingReflexivePair) x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one))
        (match (motive :=
          (Y X : WalkingParallelPair) →
            (X ⟶ Y) →
              Quiver.Hom (V := WalkingReflexivePair)
                (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
                  | one => WalkingReflexivePair.zero
                  | zero => WalkingReflexivePair.one :
                  WalkingReflexivePair)
                (match (motive := WalkingParallelPair → WalkingReflexivePair) Y with
                  | one => WalkingReflexivePair.zero
                  | zero => WalkingReflexivePair.one :
                  WalkingReflexivePair))
          Z, X, g with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match (motive := WalkingParallelPair → WalkingReflexivePair) x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)) :
      Quiver.Hom (V := WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) Z with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair))
have id₁ : Eq (α :=
  Quiver.Hom (V := WalkingReflexivePair)
    (match (motive := WalkingParallelPair → WalkingReflexivePair) zero with
      | one => WalkingReflexivePair.zero
      | zero => WalkingReflexivePair.one :
      WalkingReflexivePair)
    (match (motive := WalkingParallelPair → WalkingReflexivePair) one with
      | one => WalkingReflexivePair.zero
      | zero => WalkingReflexivePair.one :
      WalkingReflexivePair))
  (match (motive :=
      (Y X : WalkingParallelPair) →
        (X ⟶ Y) →
          Quiver.Hom (V := WalkingReflexivePair)
            (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
              | one => WalkingReflexivePair.zero
              | zero => WalkingReflexivePair.one :
              WalkingReflexivePair)
            (match (motive := WalkingParallelPair → WalkingReflexivePair) Y with
              | one => WalkingReflexivePair.zero
              | zero => WalkingReflexivePair.one :
              WalkingReflexivePair))
      one, zero, WalkingParallelPairHom.id zero ≫ WalkingParallelPairHom.right with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match (motive := WalkingParallelPair → WalkingReflexivePair) x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one) :
    Quiver.Hom (V := WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) zero with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one :
        WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) one with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one :
        WalkingReflexivePair))
  (CategoryStruct.comp (Y :=
      match (motive := WalkingParallelPair → WalkingReflexivePair) zero with
      | one => WalkingReflexivePair.zero
      | zero => WalkingReflexivePair.one)
      (match (motive :=
        (Y X : WalkingParallelPair) →
          (X ⟶ Y) →
            Quiver.Hom (V := WalkingReflexivePair)
              (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
                | one => WalkingReflexivePair.zero
                | zero => WalkingReflexivePair.one :
                WalkingReflexivePair)
              (match (motive := WalkingParallelPair → WalkingReflexivePair) Y with
                | one => WalkingReflexivePair.zero
                | zero => WalkingReflexivePair.one :
                WalkingReflexivePair))
        zero, zero, WalkingParallelPairHom.id zero with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match (motive := WalkingParallelPair → WalkingReflexivePair) x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one))
      (match (motive :=
        (Y X : WalkingParallelPair) →
          (X ⟶ Y) →
            Quiver.Hom (V := WalkingReflexivePair)
              (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
                | one => WalkingReflexivePair.zero
                | zero => WalkingReflexivePair.one :
                WalkingReflexivePair)
              (match (motive := WalkingParallelPair → WalkingReflexivePair) Y with
                | one => WalkingReflexivePair.zero
                | zero => WalkingReflexivePair.one :
                WalkingReflexivePair))
        one, zero, WalkingParallelPairHom.right with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match (motive := WalkingParallelPair → WalkingReflexivePair) x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) :
    Quiver.Hom (V := WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) zero with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one :
        WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) one with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one :
        WalkingReflexivePair))
Tactic: cases g
Cleared hypotheses: X, Z, g