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

Tactic:
cat_disch