-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.mk.sizeOf_spec : ∀ (id : ℕ) (ringId? : Option ℕ) (type : Lean.Expr) (u : Lean.Level) (intModuleInst : Lean.Expr)
  (leInst? ltInst? lawfulOrderLTInst? isPreorderInst? orderedAddInst? isLinearInst? noNatDivInst? ringInst?
    commRingInst? orderedRingInst? fieldInst? : Option Lean.Expr)
  (charInst? : Option (Lean.Expr × ℕ)) (zero ofNatZero : Lean.Expr) (one? leFn? ltFn? : Option Lean.Expr)
  (addFn zsmulFn nsmulFn : Lean.Expr) (zsmulFn? nsmulFn? homomulFn? : Option Lean.Expr) (subFn negFn : Lean.Expr)
  (vars : Lean.PArray Lean.Expr) (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.Linarith.Var)
  (lowers uppers : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Linear.IneqCnstr))
  (diseqs : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Linear.DiseqCnstr)) (assignment : Lean.PArray ℚ)
  (caseSplits : Bool) (conflict? : Option Lean.Meta.Grind.Arith.Linear.UnsatProof)
  (diseqSplits : Lean.PHashMap Lean.Grind.Linarith.Poly Lean.FVarId)
  (elimEqs : Lean.PArray (Option Lean.Meta.Grind.Arith.Linear.EqCnstr)) (elimStack : List Lean.Grind.Linarith.Var)
  (occurs : Lean.PArray Lean.Meta.Grind.Arith.Linear.VarSet) (ignored : Lean.PArray Lean.Expr),
  sizeOf
      { id := id, ringId? := ringId?, type := type, u := u, intModuleInst := intModuleInst, leInst? := leInst?,
        ltInst? := ltInst?, lawfulOrderLTInst? := lawfulOrderLTInst?, isPreorderInst? := isPreorderInst?,
        orderedAddInst? := orderedAddInst?, isLinearInst? := isLinearInst?, noNatDivInst? := noNatDivInst?,
        ringInst? := ringInst?, commRingInst? := commRingInst?, orderedRingInst? := orderedRingInst?,
        fieldInst? := fieldInst?, charInst? := charInst?, zero := zero, ofNatZero := ofNatZero, one? := one?,
        leFn? := leFn?, ltFn? := ltFn?, addFn := addFn, zsmulFn := zsmulFn, nsmulFn := nsmulFn, zsmulFn? := zsmulFn?,
        nsmulFn? := nsmulFn?, homomulFn? := homomulFn?, subFn := subFn, negFn := negFn, vars := vars, varMap := varMap,
        lowers := lowers, uppers := uppers, diseqs := diseqs, assignment := assignment, caseSplits := caseSplits,
        conflict? := conflict?, diseqSplits := diseqSplits, elimEqs := elimEqs, elimStack := elimStack,
        occurs := occurs, ignored := ignored } =
    ⋯ + sizeOf zero + sizeOf ofNatZero + sizeOf one? + sizeOf leFn? + sizeOf ltFn? + sizeOf addFn + sizeOf zsmulFn +
                                          sizeOf nsmulFn +
                                        sizeOf zsmulFn? +
                                      sizeOf nsmulFn? +
                                    sizeOf homomulFn? +
                                  sizeOf subFn +
                                sizeOf negFn +
                              sizeOf vars +
                            sizeOf varMap +
                          sizeOf lowers +
                        sizeOf uppers +
                      sizeOf diseqs +
                    sizeOf assignment +
                  sizeOf caseSplits +
                sizeOf conflict? +
              sizeOf diseqSplits +
            sizeOf elimEqs +
          sizeOf elimStack +
        sizeOf occurs +
      sizeOf ignored