-- 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)
right right₁ right₂ right₃ :
  Eq (α :=
    Functor.obj
        (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
          (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
          (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
        WalkingParallelPair.zero ⟶
      Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.one)
    (Functor.map
        (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
          (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : 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))
        WalkingParallelPairHom.right ≫
      Iso.hom
        ((fun (X : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj
                  (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
                    (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
                    (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one)
                      fun (p : ULift.{w, 0} Bool) ↦
                      bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
                  X ≅
                Functor.obj (𝟭 WalkingParallelPair) X))
          WalkingParallelPair.one))
    (Iso.hom
        ((fun (X : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj
                  (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
                    (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
                    (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one)
                      fun (p : ULift.{w, 0} Bool) ↦
                      bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
                  X ≅
                Functor.obj (𝟭 WalkingParallelPair) X))
          WalkingParallelPair.zero) ≫
      Functor.map (𝟭 WalkingParallelPair) WalkingParallelPairHom.right)
⊢ Eq (α :=
    Functor.obj
        (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
          (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
          (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one) fun (p : ULift.{w, 0} Bool) ↦
            bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
        WalkingParallelPair.zero ⟶
      Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.one)
    (Functor.map
        (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
          (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false : 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))
        WalkingParallelPairHom.right ≫
      Iso.hom
        ((fun (X : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj
                  (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
                    (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
                    (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one)
                      fun (p : ULift.{w, 0} Bool) ↦
                      bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
                  X ≅
                Functor.obj (𝟭 WalkingParallelPair) X))
          WalkingParallelPair.one))
    (Iso.hom
        ((fun (X : WalkingParallelPair) ↦
            (eqToIso ⋯ :
              Functor.obj
                  (Functor.comp.{0, w, 0, 0, w, 0} (D := WalkingParallelFamily (ULift.{w, 0} Bool))
                    (parallelPair (line { down := true : ULift.{w, 0} Bool }) (line { down := false }))
                    (parallelFamily (X := WalkingParallelPair.zero) (Y := WalkingParallelPair.one)
                      fun (p : ULift.{w, 0} Bool) ↦
                      bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right))
                  X ≅
                Functor.obj (𝟭 WalkingParallelPair) X))
          WalkingParallelPair.zero) ≫
      Functor.map (𝟭 WalkingParallelPair) WalkingParallelPairHom.right)

Tactic:
cat_disch