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

Tactic:
cases f