-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
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))
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))
id₂ :
  Eq (α :=
    Quiver.Hom (V := WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one :
        WalkingReflexivePair)
      (match (motive := WalkingParallelPair → WalkingReflexivePair) X 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))
        X, X, WalkingParallelPairHom.id 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) :
      Quiver.Hom (V := WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) X 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))
          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)) :
      Quiver.Hom (V := WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) X with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one :
          WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) X 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))

Tactic:
cases g