-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g_1 : X ⟶ Y
X_1 Z : WalkingParallelPair
g : X_1 ⟶ Z
id :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingParallelPair → C) zero with
        | zero => X
        | one => Y :
        C)
      (match (motive := WalkingParallelPair → C) one with
        | zero => X
        | one => Y :
        C))
    (match (motive :=
        (X_2 Y_1 : WalkingParallelPair) →
          (X_2 ⟶ Y_1) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingParallelPair → C) X_2 with
                | zero => X
                | one => Y :
                C)
              (match (motive := WalkingParallelPair → C) Y_1 with
                | zero => X
                | one => Y :
                C))
        zero, one, WalkingParallelPairHom.id zero ≫ left with
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        𝟙
          (match (motive := WalkingParallelPair → C) x with
          | zero => X
          | one => Y)
      | .(zero), .(one), left => f
      | .(zero), .(one), right => g_1 :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingParallelPair → C) zero with
          | zero => X
          | one => Y :
          C)
        (match (motive := WalkingParallelPair → C) one with
          | zero => X
          | one => Y :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingParallelPair → C) zero with
        | zero => X
        | one => Y)
        (match (motive :=
          (X_2 Y_1 : WalkingParallelPair) →
            (X_2 ⟶ Y_1) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingParallelPair → C) X_2 with
                  | zero => X
                  | one => Y :
                  C)
                (match (motive := WalkingParallelPair → C) Y_1 with
                  | zero => X
                  | one => Y :
                  C))
          zero, zero, WalkingParallelPairHom.id zero with
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          𝟙
            (match (motive := WalkingParallelPair → C) x with
            | zero => X
            | one => Y)
        | .(zero), .(one), left => f
        | .(zero), .(one), right => g_1)
        (match (motive :=
          (X_2 Y_1 : WalkingParallelPair) →
            (X_2 ⟶ Y_1) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingParallelPair → C) X_2 with
                  | zero => X
                  | one => Y :
                  C)
                (match (motive := WalkingParallelPair → C) Y_1 with
                  | zero => X
                  | one => Y :
                  C))
          zero, one, left with
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          𝟙
            (match (motive := WalkingParallelPair → C) x with
            | zero => X
            | one => Y)
        | .(zero), .(one), left => f
        | .(zero), .(one), right => g_1) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingParallelPair → C) zero with
          | zero => X
          | one => Y :
          C)
        (match (motive := WalkingParallelPair → C) one with
          | zero => X
          | one => Y :
          C))
id₁ :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingParallelPair → C) zero with
        | zero => X
        | one => Y :
        C)
      (match (motive := WalkingParallelPair → C) one with
        | zero => X
        | one => Y :
        C))
    (match (motive :=
        (X_2 Y_1 : WalkingParallelPair) →
          (X_2 ⟶ Y_1) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingParallelPair → C) X_2 with
                | zero => X
                | one => Y :
                C)
              (match (motive := WalkingParallelPair → C) Y_1 with
                | zero => X
                | one => Y :
                C))
        zero, one, WalkingParallelPairHom.id zero ≫ right with
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        𝟙
          (match (motive := WalkingParallelPair → C) x with
          | zero => X
          | one => Y)
      | .(zero), .(one), left => f
      | .(zero), .(one), right => g_1 :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingParallelPair → C) zero with
          | zero => X
          | one => Y :
          C)
        (match (motive := WalkingParallelPair → C) one with
          | zero => X
          | one => Y :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingParallelPair → C) zero with
        | zero => X
        | one => Y)
        (match (motive :=
          (X_2 Y_1 : WalkingParallelPair) →
            (X_2 ⟶ Y_1) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingParallelPair → C) X_2 with
                  | zero => X
                  | one => Y :
                  C)
                (match (motive := WalkingParallelPair → C) Y_1 with
                  | zero => X
                  | one => Y :
                  C))
          zero, zero, WalkingParallelPairHom.id zero with
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          𝟙
            (match (motive := WalkingParallelPair → C) x with
            | zero => X
            | one => Y)
        | .(zero), .(one), left => f
        | .(zero), .(one), right => g_1)
        (match (motive :=
          (X_2 Y_1 : WalkingParallelPair) →
            (X_2 ⟶ Y_1) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingParallelPair → C) X_2 with
                  | zero => X
                  | one => Y :
                  C)
                (match (motive := WalkingParallelPair → C) Y_1 with
                  | zero => X
                  | one => Y :
                  C))
          zero, one, right with
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          𝟙
            (match (motive := WalkingParallelPair → C) x with
            | zero => X
            | one => Y)
        | .(zero), .(one), left => f
        | .(zero), .(one), right => g_1) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingParallelPair → C) zero with
          | zero => X
          | one => Y :
          C)
        (match (motive := WalkingParallelPair → C) one with
          | zero => X
          | one => Y :
          C))
id₂ :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingParallelPair → C) X_1 with
        | zero => X
        | one => Y :
        C)
      (match (motive := WalkingParallelPair → C) X_1 with
        | zero => X
        | one => Y :
        C))
    (match (motive :=
        (X_2 Y_1 : WalkingParallelPair) →
          (X_2 ⟶ Y_1) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingParallelPair → C) X_2 with
                | zero => X
                | one => Y :
                C)
              (match (motive := WalkingParallelPair → C) Y_1 with
                | zero => X
                | one => Y :
                C))
        X_1, X_1, WalkingParallelPairHom.id X_1 ≫ WalkingParallelPairHom.id X_1 with
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        𝟙
          (match (motive := WalkingParallelPair → C) x with
          | zero => X
          | one => Y)
      | .(zero), .(one), left => f
      | .(zero), .(one), right => g_1 :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingParallelPair → C) X_1 with
          | zero => X
          | one => Y :
          C)
        (match (motive := WalkingParallelPair → C) X_1 with
          | zero => X
          | one => Y :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingParallelPair → C) X_1 with
        | zero => X
        | one => Y)
        (match (motive :=
          (X_2 Y_1 : WalkingParallelPair) →
            (X_2 ⟶ Y_1) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingParallelPair → C) X_2 with
                  | zero => X
                  | one => Y :
                  C)
                (match (motive := WalkingParallelPair → C) Y_1 with
                  | zero => X
                  | one => Y :
                  C))
          X_1, X_1, WalkingParallelPairHom.id X_1 with
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          𝟙
            (match (motive := WalkingParallelPair → C) x with
            | zero => X
            | one => Y)
        | .(zero), .(one), left => f
        | .(zero), .(one), right => g_1)
        (match (motive :=
          (X_2 Y_1 : WalkingParallelPair) →
            (X_2 ⟶ Y_1) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingParallelPair → C) X_2 with
                  | zero => X
                  | one => Y :
                  C)
                (match (motive := WalkingParallelPair → C) Y_1 with
                  | zero => X
                  | one => Y :
                  C))
          X_1, X_1, WalkingParallelPairHom.id X_1 with
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          𝟙
            (match (motive := WalkingParallelPair → C) x with
            | zero => X
            | one => Y)
        | .(zero), .(one), left => f
        | .(zero), .(one), right => g_1) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingParallelPair → C) X_1 with
          | zero => X
          | one => Y :
          C)
        (match (motive := WalkingParallelPair → C) X_1 with
          | zero => X
          | one => Y :
          C))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (match (motive := WalkingParallelPair → C) X_1 with
        | zero => X
        | one => Y :
        C)
      (match (motive := WalkingParallelPair → C) Z with
        | zero => X
        | one => Y :
        C))
    (match (motive :=
        (X_2 Y_1 : WalkingParallelPair) →
          (X_2 ⟶ Y_1) →
            Quiver.Hom.{v, u} (V := C)
              (match (motive := WalkingParallelPair → C) X_2 with
                | zero => X
                | one => Y :
                C)
              (match (motive := WalkingParallelPair → C) Y_1 with
                | zero => X
                | one => Y :
                C))
        X_1, Z, WalkingParallelPairHom.id X_1 ≫ g with
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        𝟙
          (match (motive := WalkingParallelPair → C) x with
          | zero => X
          | one => Y)
      | .(zero), .(one), left => f
      | .(zero), .(one), right => g_1 :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingParallelPair → C) X_1 with
          | zero => X
          | one => Y :
          C)
        (match (motive := WalkingParallelPair → C) Z with
          | zero => X
          | one => Y :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := WalkingParallelPair → C) X_1 with
        | zero => X
        | one => Y)
        (match (motive :=
          (X_2 Y_1 : WalkingParallelPair) →
            (X_2 ⟶ Y_1) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingParallelPair → C) X_2 with
                  | zero => X
                  | one => Y :
                  C)
                (match (motive := WalkingParallelPair → C) Y_1 with
                  | zero => X
                  | one => Y :
                  C))
          X_1, X_1, WalkingParallelPairHom.id X_1 with
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          𝟙
            (match (motive := WalkingParallelPair → C) x with
            | zero => X
            | one => Y)
        | .(zero), .(one), left => f
        | .(zero), .(one), right => g_1)
        (match (motive :=
          (X_2 Y_1 : WalkingParallelPair) →
            (X_2 ⟶ Y_1) →
              Quiver.Hom.{v, u} (V := C)
                (match (motive := WalkingParallelPair → C) X_2 with
                  | zero => X
                  | one => Y :
                  C)
                (match (motive := WalkingParallelPair → C) Y_1 with
                  | zero => X
                  | one => Y :
                  C))
          X_1, Z, g with
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          𝟙
            (match (motive := WalkingParallelPair → C) x with
            | zero => X
            | one => Y)
        | .(zero), .(one), left => f
        | .(zero), .(one), right => g_1) :
      Quiver.Hom.{v, u} (V := C)
        (match (motive := WalkingParallelPair → C) X_1 with
          | zero => X
          | one => Y :
          C)
        (match (motive := WalkingParallelPair → C) Z with
          | zero => X
          | one => Y :
          C))

Tactic:
cases g