-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
X Y Z : WalkingParallelPair
f : X ⟶ Y
g : Y ⟶ Z
left :
  ∀ (g : one ⟶ Z),
    Eq (α :=
      Quiver.Hom (V := WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) zero 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, zero, WalkingParallelPairHom.left ≫ 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) zero 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) one 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))
          (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, one, 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) zero with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one :
            WalkingReflexivePair)
          (match (motive := WalkingParallelPair → WalkingReflexivePair) Z with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one :
            WalkingReflexivePair))
right :
  ∀ (g : one ⟶ Z),
    Eq (α :=
      Quiver.Hom (V := WalkingReflexivePair)
        (match (motive := WalkingParallelPair → WalkingReflexivePair) zero 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, zero, WalkingParallelPairHom.right ≫ 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) zero 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) one 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))
          (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, one, 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) zero with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one :
            WalkingReflexivePair)
          (match (motive := WalkingParallelPair → WalkingReflexivePair) Z 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, 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))
have id : ∀ (g : X ⟶ 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, 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 f
Cleared hypotheses: Y, f, g