-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
P : C
ι : P ⟶ X_1
w : ι ≫ f_1 = ι ≫ g
X Y : WalkingParallelPair
f : X ⟶ Y
zero :
  ∀ (f : WalkingParallelPair.zero ⟶ Y),
    Eq.{v + 1} (α :=
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPair.zero ⟶
        (parallelPair f_1 g).obj Y)
      (Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) f ≫
        WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
          (h : Y = t) →
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) Y ⟶ (parallelPair f_1 g).obj Y)
          Y
          (fun (h : Y = WalkingParallelPair.zero) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶
                (parallelPair f_1 g).obj X)
              ι ⋯)
          (fun (h : Y = WalkingParallelPair.one) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶
                (parallelPair f_1 g).obj X)
              (ι ≫ f_1) ⋯)
          ⋯)
      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
          (h : WalkingParallelPair.zero = t) →
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPair.zero ⟶
              (parallelPair f_1 g).obj WalkingParallelPair.zero)
          WalkingParallelPair.zero
          (fun (h : WalkingParallelPair.zero = WalkingParallelPair.zero) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶
                (parallelPair f_1 g).obj X)
              ι ⋯)
          (fun (h : WalkingParallelPair.zero = WalkingParallelPair.one) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶
                (parallelPair f_1 g).obj X)
              (ι ≫ f_1) ⋯)
          ⋯ ≫
        (parallelPair f_1 g).map f)
one :
  ∀ (f : WalkingParallelPair.one ⟶ Y),
    Eq.{v + 1} (α :=
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPair.one ⟶
        (parallelPair f_1 g).obj Y)
      (Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) f ≫
        WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
          (h : Y = t) →
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) Y ⟶ (parallelPair f_1 g).obj Y)
          Y
          (fun (h : Y = WalkingParallelPair.zero) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶
                (parallelPair f_1 g).obj X)
              ι ⋯)
          (fun (h : Y = WalkingParallelPair.one) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶
                (parallelPair f_1 g).obj X)
              (ι ≫ f_1) ⋯)
          ⋯)
      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
          (h : WalkingParallelPair.one = t) →
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPair.one ⟶
              (parallelPair f_1 g).obj WalkingParallelPair.one)
          WalkingParallelPair.one
          (fun (h : WalkingParallelPair.one = WalkingParallelPair.zero) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶
                (parallelPair f_1 g).obj X)
              ι ⋯)
          (fun (h : WalkingParallelPair.one = WalkingParallelPair.one) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶
                (parallelPair f_1 g).obj X)
              (ι ≫ f_1) ⋯)
          ⋯ ≫
        (parallelPair f_1 g).map f)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶ (parallelPair f_1 g).obj Y)
    (Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) f ≫
      WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : Y = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) Y ⟶ (parallelPair f_1 g).obj Y)
        Y
        (fun (h : Y = WalkingParallelPair.zero) ↦
          Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶ (parallelPair f_1 g).obj X)
            ι ⋯)
        (fun (h : Y = WalkingParallelPair.one) ↦
          Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶ (parallelPair f_1 g).obj X)
            (ι ≫ f_1) ⋯)
        ⋯)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
        (h : X = t) →
          Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶ (parallelPair f_1 g).obj X)
        X
        (fun (h : X = WalkingParallelPair.zero) ↦
          Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶ (parallelPair f_1 g).obj X)
            ι ⋯)
        (fun (h : X = WalkingParallelPair.one) ↦
          Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶ (parallelPair f_1 g).obj X)
            (ι ≫ f_1) ⋯)
        ⋯ ≫
      (parallelPair f_1 g).map f)

Tactic:
cases X