-- 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 g : X ⟶ Y
zero zero₁ zero₂ zero₃ :
  Eq (α :=
    obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.zero ⟶
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj WalkingParallelPair.zero)
    (map (parallelPair f.op g.op) (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj x))
          WalkingParallelPair.zero))
    (Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj x))
          WalkingParallelPair.zero) ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map
        (WalkingParallelPairHom.id WalkingParallelPair.zero))
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.zero ⟶
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj WalkingParallelPair.zero)
    (map (parallelPair f.op g.op) (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj x))
          WalkingParallelPair.zero))
    (Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj x))
          WalkingParallelPair.zero) ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map
        (WalkingParallelPairHom.id WalkingParallelPair.zero))

Tactic:
cat_disch