-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
X 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))
have 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))
Tactic: cases f
Cleared hypotheses: X, Y, f, g