-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
one one₁ one₂ one₃ :
  Eq (α :=
    Quiver.Hom (V := WalkingParallelPair)
      (Functor.obj.{w, 0, w, 0} (C := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
        WalkingParallelFamily.one)
      (Functor.obj.{w, 0, w, 0} (C := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
        WalkingParallelFamily.one))
    (Functor.map
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
        ((NatIso.ofComponents (fun (X : WalkingParallelFamily (ULift.{w, 0} Bool)) ↦ eqToIso ⋯)
                @walkingParallelFamilyEquivWalkingParallelPair._proof_2).hom.app
          WalkingParallelFamily.one) ≫
      (NatIso.ofComponents (fun (X : WalkingParallelPair) ↦ eqToIso ⋯)
              @walkingParallelFamilyEquivWalkingParallelPair._proof_4).hom.app
        (Functor.obj.{w, 0, w, 0} (C := WalkingParallelFamily (ULift.{w, 0} Bool))
          (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
          WalkingParallelFamily.one))
    (𝟙
      (Functor.obj.{w, 0, w, 0} (C := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
        WalkingParallelFamily.one))
⊢ Eq (α :=
    Quiver.Hom (V := WalkingParallelPair)
      (Functor.obj.{w, 0, w, 0} (C := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
        WalkingParallelFamily.one)
      (Functor.obj.{w, 0, w, 0} (C := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
        WalkingParallelFamily.one))
    (Functor.map
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
        ((NatIso.ofComponents (fun (X : WalkingParallelFamily (ULift.{w, 0} Bool)) ↦ eqToIso ⋯)
                @walkingParallelFamilyEquivWalkingParallelPair._proof_2).hom.app
          WalkingParallelFamily.one) ≫
      (NatIso.ofComponents (fun (X : WalkingParallelPair) ↦ eqToIso ⋯)
              @walkingParallelFamilyEquivWalkingParallelPair._proof_4).hom.app
        (Functor.obj.{w, 0, w, 0} (C := WalkingParallelFamily (ULift.{w, 0} Bool))
          (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
          WalkingParallelFamily.one))
    (𝟙
      (Functor.obj.{w, 0, w, 0} (C := WalkingParallelFamily (ULift.{w, 0} Bool))
        (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
          bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right)
        WalkingParallelFamily.one))

Tactic:
cat_disch