-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f_1 g : X ⟶ Y
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.one
zero :
  Eq (α :=
    obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero ⟶
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj WalkingParallelPair.one)
    (map (parallelPair f_1.op g.op) WalkingParallelPairHom.left ≫
      Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.one))
    (Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.zero) ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).map WalkingParallelPairHom.left)
zero₁ :
  Eq (α :=
    obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero ⟶
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj WalkingParallelPair.one)
    (map (parallelPair f_1.op g.op) WalkingParallelPairHom.right ≫
      Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.one))
    (Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.zero) ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).map WalkingParallelPairHom.right)
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero ⟶
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj WalkingParallelPair.one)
    (map (parallelPair f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.one))
    (Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.zero) ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).map f)

Tactic:
cases f