-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
X : WalkingParallelPair
_ :
  ∀ {Y Z : WalkingParallelPair} (f : X ⟶ Y) (g : Y ⟶ Z),
    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, f ≫ 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) Y 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))
            Y, X, f 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, Y, 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))
⊢ ∀ {Y Z : WalkingParallelPair} (f : X ⟶ Y) (g : Y ⟶ Z),
    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, f ≫ 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) Y 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))
            Y, X, f 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, Y, 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:
_