Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: ⊢ ∀ {X Y Z : WalkingParallelPair} (f : X ⟶ Y) (g : Y ⟶ Z),
    WalkingParallelPairHom.casesOn (motive := fun a a_1 t ↦
        X = a →
          Z = a_1 →
            f ≫ g ≍ t →
              (op
                  (match X with
                  | zero => one
                  | one => zero) ⟶
                op
                  (match Z with
                  | zero => one
                  | one => zero)))
        (f ≫ g)
        (fun h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z) →
              Z = one →
                f ≍ left →
                  (op
                      (match X with
                      | zero => one
                      | one => zero) ⟶
                    op
                      (match Z with
                      | zero => one
                      | one => zero)))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : zero ⟶ Y) →
                  f ≍ left →
                    (op
                        (match zero with
                        | zero => one
                        | one => zero) ⟶
                      op
                        (match Y with
                        | zero => one
                        | one => zero)))
                (fun f h ↦ Quiver.Hom.op left) ⋯ f)
            ⋯ (f ≫ g))
        (fun h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z) →
              Z = one →
                f ≍ right →
                  (op
                      (match X with
                      | zero => one
                      | one => zero) ⟶
                    op
                      (match Z with
                      | zero => one
                      | one => zero)))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : zero ⟶ Y) →
                  f ≍ right →
                    (op
                        (match zero with
                        | zero => one
                        | one => zero) ⟶
                      op
                        (match Y with
                        | zero => one
                        | one => zero)))
                (fun f h ↦ Quiver.Hom.op right) ⋯ f)
            ⋯ (f ≫ g))
        (fun X_1 h ↦
          Eq.ndrec (motive := fun X_2 ↦
            Z = X_2 →
              f ≫ g ≍ WalkingParallelPairHom.id X_2 →
                (op
                    (match X with
                    | zero => one
                    | one => zero) ⟶
                  op
                    (match Z with
                    | zero => one
                    | one => zero)))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : X ⟶ Y) →
                  f ≍ WalkingParallelPairHom.id X →
                    (op
                        (match X with
                        | zero => one
                        | one => zero) ⟶
                      op
                        (match Y with
                        | zero => one
                        | one => zero)))
                (fun f h ↦
                  Quiver.Hom.op
                    (WalkingParallelPairHom.id
                      (match X with
                      | zero => one
                      | one => zero)))
                ⋯ (f ≫ g))
            h)
        ⋯ ⋯ ⋯ =
      WalkingParallelPairHom.casesOn (motive := fun a a_1 t ↦
          X = a →
            Y = a_1 →
              f ≍ t →
                (op
                    (match X with
                    | zero => one
                    | one => zero) ⟶
                  op
                    (match Y with
                    | zero => one
                    | one => zero)))
          f
          (fun h ↦
            Eq.ndrec (motive := fun {X} ↦
              (f : X ⟶ Y) →
                Y = one →
                  f ≍ left →
                    (op
                        (match X with
                        | zero => one
                        | one => zero) ⟶
                      op
                        (match Y with
                        | zero => one
                        | one => zero)))
              (fun f h ↦
                Eq.ndrec (motive := fun {Y} ↦
                  (f : zero ⟶ Y) →
                    f ≍ left →
                      (op
                          (match zero with
                          | zero => one
                          | one => zero) ⟶
                        op
                          (match Y with
                          | zero => one
                          | one => zero)))
                  (fun f h ↦ Quiver.Hom.op left) ⋯ f)
              ⋯ f)
          (fun h ↦
            Eq.ndrec (motive := fun {X} ↦
              (f : X ⟶ Y) →
                Y = one →
                  f ≍ right →
                    (op
                        (match X with
                        | zero => one
                        | one => zero) ⟶
                      op
                        (match Y with
                        | zero => one
                        | one => zero)))
              (fun f h ↦
                Eq.ndrec (motive := fun {Y} ↦
                  (f : zero ⟶ Y) →
                    f ≍ right →
                      (op
                          (match zero with
                          | zero => one
                          | one => zero) ⟶
                        op
                          (match Y with
                          | zero => one
                          | one => zero)))
                  (fun f h ↦ Quiver.Hom.op right) ⋯ f)
              ⋯ f)
          (fun X_1 h ↦
            Eq.ndrec (motive := fun X_2 ↦
              Y = X_2 →
                f ≍ WalkingParallelPairHom.id X_2 →
                  (op
                      (match X with
                      | zero => one
                      | one => zero) ⟶
                    op
                      (match Y with
                      | zero => one
                      | one => zero)))
              (fun h ↦
                Eq.ndrec (motive := fun {Y} ↦
                  (f : X ⟶ Y) →
                    f ≍ WalkingParallelPairHom.id X →
                      (op
                          (match X with
                          | zero => one
                          | one => zero) ⟶
                        op
                          (match Y with
                          | zero => one
                          | one => zero)))
                  (fun f h ↦
                    Quiver.Hom.op
                      (WalkingParallelPairHom.id
                        (match X with
                        | zero => one
                        | one => zero)))
                  ⋯ f)
              h)
          ⋯ ⋯ ⋯ ≫
        WalkingParallelPairHom.casesOn (motive := fun a a_1 t ↦
          Y = a →
            Z = a_1 →
              g ≍ t →
                (op
                    (match Y with
                    | zero => one
                    | one => zero) ⟶
                  op
                    (match Z with
                    | zero => one
                    | one => zero)))
          g
          (fun h ↦
            Eq.ndrec (motive := fun {X} ↦
              (f : X ⟶ Z) →
                Z = one →
                  f ≍ left →
                    (op
                        (match X with
                        | zero => one
                        | one => zero) ⟶
                      op
                        (match Z with
                        | zero => one
                        | one => zero)))
              (fun f h ↦
                Eq.ndrec (motive := fun {Y} ↦
                  (f : zero ⟶ Y) →
                    f ≍ left →
                      (op
                          (match zero with
                          | zero => one
                          | one => zero) ⟶
                        op
                          (match Y with
                          | zero => one
                          | one => zero)))
                  (fun f h ↦ Quiver.Hom.op left) ⋯ f)
              ⋯ g)
          (fun h ↦
            Eq.ndrec (motive := fun {X} ↦
              (f : X ⟶ Z) →
                Z = one →
                  f ≍ right →
                    (op
                        (match X with
                        | zero => one
                        | one => zero) ⟶
                      op
                        (match Z with
                        | zero => one
                        | one => zero)))
              (fun f h ↦
                Eq.ndrec (motive := fun {Y} ↦
                  (f : zero ⟶ Y) →
                    f ≍ right →
                      (op
                          (match zero with
                          | zero => one
                          | one => zero) ⟶
                        op
                          (match Y with
                          | zero => one
                          | one => zero)))
                  (fun f h ↦ Quiver.Hom.op right) ⋯ f)
              ⋯ g)
          (fun X h ↦
            Eq.ndrec (motive := fun X ↦
              Z = X →
                g ≍ WalkingParallelPairHom.id X →
                  (op
                      (match Y with
                      | zero => one
                      | one => zero) ⟶
                    op
                      (match Z with
                      | zero => one
                      | one => zero)))
              (fun h ↦
                Eq.ndrec (motive := fun {Y_1} ↦
                  (f : Y ⟶ Y_1) →
                    f ≍ WalkingParallelPairHom.id Y →
                      (op
                          (match Y with
                          | zero => one
                          | one => zero) ⟶
                        op
                          (match Y_1 with
                          | zero => one
                          | one => zero)))
                  (fun f h ↦
                    Quiver.Hom.op
                      (WalkingParallelPairHom.id
                        (match Y with
                        | zero => one
                        | one => zero)))
                  ⋯ g)
              h)
          ⋯ ⋯ ⋯

Tactic:
by

Goal state after: