{motive_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof → Sort u} →
    {motive_3 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Sort u} →
      {motive_4 : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred → Sort u} →
        {motive_5 : Lean.Meta.Grind.Arith.Cutsat.CooperSplit → Sort u} →
          {motive_6 : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof → Sort u} →
            {motive_7 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof → Sort u} →
              {motive_8 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Sort u} →
                {motive_9 : Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof → Sort u} →
                  {motive_10 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Sort u} →
                    {motive_11 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof → Sort u} →
                      {motive_12 : Lean.Meta.Grind.Arith.Cutsat.UnsatProof → Sort u} →
                        {motive_13 : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr) → Sort u} →
                          {motive_14 : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Sort u} →
                            {motive_15 : Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Sort u} →
                              {motive_16 : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof) → Sort u} →
                                {motive_17 : List (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr) → Sort u} →
                                  {motive_18 : List (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof) → Sort u} →
                                    {motive_19 : Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Sort u} →
                                      {motive_20 : Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof → Sort u} →
                                        {motive_21 : ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Sort u} →
                                          (t : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) →
                                            ((p : Int.Linear.Poly) →
                                                (h : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof) →
                                                  motive_2 h → motive_1 { p := p, h := h }) →
                                              ((a zero : Lean.Expr) →
                                                  motive_2 (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core0 a zero)) →
                                                ((a b : Lean.Expr) →
                                                    (p₁ p₂ : Int.Linear.Poly) →
                                                      motive_2
                                                        (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core a b p₁ p₂)) →
                                                  ((a b toIntThm : Lean.Expr) →
                                                      (lhs rhs : Int.Linear.Expr) →
                                                        motive_2
                                                          (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.coreToInt a b
                                                            toIntThm lhs rhs)) →
                                                    ((e : Lean.Expr) →
                                                        (p : Int.Linear.Poly) →
                                                          motive_2
                                                            (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn e p)) →
                                                      ((h : Lean.Expr) →
                                                          (x : Int.Linear.Var) →
                                                            (e' : Int.Linear.Expr) →
                                                              motive_2
                                                                (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat h x
                                                                  e')) →
                                                        ((c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                            motive_1 c →
                                                              motive_2
                                                                (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm c)) →
                                                          ((c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                              motive_1 c →
                                                                motive_2
                                                                  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.divCoeffs
                                                                    c)) →
                                                            ((x : Int.Linear.Var) →
                                                                (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                  motive_1 c₁ →
                                                                    motive_1 c₂ →
                                                                      motive_2
                                                                        (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst
                                                                          x c₁ c₂)) →
                                                              ((c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) →
                                                                  motive_8 c₁ →
                                                                    motive_8 c₂ →
                                                                      motive_2
                                                                        (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe
                                                                          c₁ c₂)) →
                                                                ((c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                    motive_1 c →
                                                                      motive_2
                                                                        (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder
                                                                          c)) →
                                                                  ((c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                      (e : Lean.Meta.Grind.Arith.CommRing.RingExpr) →
                                                                        (p : Lean.Grind.CommRing.Poly) →
                                                                          motive_1 c →
                                                                            motive_2
                                                                              (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm
                                                                                c e p)) →
                                                                    ((e : Lean.Expr) →
                                                                        (p : Int.Linear.Poly) →
                                                                          (re :
                                                                              Lean.Meta.Grind.Arith.CommRing.RingExpr) →
                                                                            (rp : Lean.Grind.CommRing.Poly) →
                                                                              (p' : Int.Linear.Poly) →
                                                                                motive_2
                                                                                  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing
                                                                                    e p re rp p')) →
                                                                      ((h : Lean.Expr) →
                                                                          (x : Int.Linear.Var) →
                                                                            (e' : Int.Linear.Expr) →
                                                                              (p : Int.Linear.Poly) →
                                                                                (re :
                                                                                    Lean.Meta.Grind.Arith.CommRing.RingExpr) →
                                                                                  (rp : Lean.Grind.CommRing.Poly) →
                                                                                    (p' : Int.Linear.Poly) →
                                                                                      motive_2
                                                                                        (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing
                                                                                          h x e' p re rp p')) →
                                                                        ((a? : Option Lean.Expr) →
                                                                            (cs :
                                                                                Array
                                                                                  (Lean.Expr ×
                                                                                    ℤ ×
                                                                                      Lean.Meta.Grind.Arith.Cutsat.EqCnstr)) →
                                                                              motive_13 cs →
                                                                                motive_2
                                                                                  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul
                                                                                    a? cs)) →
                                                                          ((k : ℤ) →
                                                                              (y? : Option Int.Linear.Var) →
                                                                                (c :
                                                                                    Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                                  motive_1 c →
                                                                                    motive_2
                                                                                      (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div
                                                                                        k y? c)) →
                                                                            ((k : ℤ) →
                                                                                (y? : Option Int.Linear.Var) →
                                                                                  (c :
                                                                                      Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                                    motive_1 c →
                                                                                      motive_2
                                                                                        (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod
                                                                                          k y? c)) →
                                                                              ((ka : ℤ) →
                                                                                  (ca? :
                                                                                      Option
                                                                                        Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                                    (kb : ℕ) →
                                                                                      (cb? :
                                                                                          Option
                                                                                            Lean.Meta.Grind.Arith.Cutsat.EqCnstr) →
                                                                                        motive_14 ca? →
                                                                                          motive_14 cb? →
                                                                                            motive_2
                                                                                              (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow
                                                                                                ka ca? kb cb?)) →
                                                                                ((d : ℤ) →
                                                                                    (p : Int.Linear.Poly) →
                                                                                      (h :
                                                                                          Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof) →
                                                                                        motive_7 h →
                                                                                          motive_3
                                                                                            { d := d, p := p,
                                                                                              h := h }) →
                                                                                  ((left : Bool) →
                                                                                      (c₁ c₂ :
                                                                                          Lean.Meta.Grind.Arith.Cutsat.LeCnstr) →
                                                                                        (c₃? :
                                                                                            Option
                                                                                              Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) →
                                                                                          motive_8 c₁ →
                                                                                            motive_8 c₂ →
                                                                                              motive_15 c₃? →
                                                                                                motive_4
                                                                                                  { left := left,
                                                                                                    c₁ := c₁, c₂ := c₂,
                                                                                                    c₃? := c₃? }) →
                                                                                    ((pred :
                                                                                          Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred) →
                                                                                        (k : ℕ) →
                                                                                          (h :
                                                                                              Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof) →
                                                                                            motive_4 pred →
                                                                                              motive_6 h →
                                                                                                motive_5
                                                                                                  { pred := pred,
                                                                                                    k := k, h := h }) →
                                                                                      ((h : Lean.FVarId) →
                                                                                          motive_6
                                                                                            (Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec
                                                                                              h)) →
                                                                                        ((hs :
                                                                                              Array
                                                                                                (Lean.FVarId ×
                                                                                                  Lean.Meta.Grind.Arith.Cutsat.UnsatProof)) →
                                                                                            (decVars :
                                                                                                Array Lean.FVarId) →
                                                                                              motive_16 hs →
                                                                                                motive_6
                                                                                                  (Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last
                                                                                                    hs decVars)) →
                                                                                          ((e : Lean.Expr) →
                                                                                              motive_7
                                                                                                (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core
                                                                                                  e)) →
                                                                                            ((e thm : Lean.Expr) →
                                                                                                (d : ℕ) →
                                                                                                  (a :
                                                                                                      Int.Linear.Expr) →
                                                                                                    motive_7
                                                                                                      (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat
                                                                                                        e thm d a)) →
                                                                                              ((c :
                                                                                                    Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) →
                                                                                                  motive_3 c →
                                                                                                    motive_7
                                                                                                      (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm
                                                                                                        c)) →
                                                                                                ((c :
                                                                                                      Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) →
                                                                                                    motive_3 c →
                                                                                                      motive_7
                                                                                                        (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs
                                                                                                          c)) →
                                                                                                  ((c₁ c₂ :
                                                                                                        Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) →
                                                                                                      motive_3 c₁ →
                                                                                                        motive_3 c₂ →
                                                                                                          motive_7
                                                                                                            (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine
                                                                                                              c₁ c₂)) →
                                                                                                    ((c₁ c₂ :
                                                                                                          Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) →
                                                                                                        motive_3 c₁ →
                                                                                                          motive_3 c₂ →
                                                                                                            motive_7
                                                                                                              (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveElim
                                                                                                                c₁
                                                                                                                c₂)) →
                                                                                                      ⋯