-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.mk.injEq : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (toIntInst rangeExpr : Lean.Expr)
  (range : Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval) (toInt wrap : Lean.Expr) (ofWrap0? : Option Lean.Expr)
  (ofEq ofDiseq : Lean.Expr) (lowerThm? upperThm? : Option Lean.Expr)
  (ofLE? ofNotLE? ofLT? ofNotLT? : Option (Option Lean.Expr))
  (addThms? mulThms? : Option Lean.Meta.Grind.Arith.Cutsat.ToIntThms)
  (subThm? negThm? divThm? modThm? powThm? zeroThm? ofNatThm? : Option (Option Lean.Expr)) (id_1 : ℕ)
  (type_1 : Lean.Expr) (u_1 : Lean.Level) (toIntInst_1 rangeExpr_1 : Lean.Expr)
  (range_1 : Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval) (toInt_1 wrap_1 : Lean.Expr)
  (ofWrap0?_1 : Option Lean.Expr) (ofEq_1 ofDiseq_1 : Lean.Expr) (lowerThm?_1 upperThm?_1 : Option Lean.Expr)
  (ofLE?_1 ofNotLE?_1 ofLT?_1 ofNotLT?_1 : Option (Option Lean.Expr))
  (addThms?_1 mulThms?_1 : Option Lean.Meta.Grind.Arith.Cutsat.ToIntThms)
  (subThm?_1 negThm?_1 divThm?_1 modThm?_1 powThm?_1 zeroThm?_1 ofNatThm?_1 : Option (Option Lean.Expr)),
  ({ id := id, type := type, u := u, toIntInst := toIntInst, rangeExpr := rangeExpr, range := range, toInt := toInt,
        wrap := wrap, ofWrap0? := ofWrap0?, ofEq := ofEq, ofDiseq := ofDiseq, lowerThm? := lowerThm?,
        upperThm? := upperThm?, ofLE? := ofLE?, ofNotLE? := ofNotLE?, ofLT? := ofLT?, ofNotLT? := ofNotLT?,
        addThms? := addThms?, mulThms? := mulThms?, subThm? := subThm?, negThm? := negThm?, divThm? := divThm?,
        modThm? := modThm?, powThm? := powThm?, zeroThm? := zeroThm?, ofNatThm? := ofNatThm? } =
      { id := id_1, type := type_1, u := u_1, toIntInst := toIntInst_1, rangeExpr := rangeExpr_1, range := range_1,
        toInt := toInt_1, wrap := wrap_1, ofWrap0? := ofWrap0?_1, ofEq := ofEq_1, ofDiseq := ofDiseq_1,
        lowerThm? := lowerThm?_1, upperThm? := upperThm?_1, ofLE? := ofLE?_1, ofNotLE? := ofNotLE?_1, ofLT? := ofLT?_1,
        ofNotLT? := ofNotLT?_1, addThms? := addThms?_1, mulThms? := mulThms?_1, subThm? := subThm?_1,
        negThm? := negThm?_1, divThm? := divThm?_1, modThm? := modThm?_1, powThm? := powThm?_1, zeroThm? := zeroThm?_1,
        ofNatThm? := ofNatThm?_1 }) =
    (id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          toIntInst = toIntInst_1 ∧
            rangeExpr = rangeExpr_1 ∧
              range = range_1 ∧
                toInt = toInt_1 ∧
                  wrap = wrap_1 ∧
                    ofWrap0? = ofWrap0?_1 ∧
                      ofEq = ofEq_1 ∧
                        ofDiseq = ofDiseq_1 ∧
                          lowerThm? = lowerThm?_1 ∧
                            upperThm? = upperThm?_1 ∧
                              ofLE? = ofLE?_1 ∧
                                ofNotLE? = ofNotLE?_1 ∧
                                  ofLT? = ofLT?_1 ∧
                                    ofNotLT? = ofNotLT?_1 ∧
                                      addThms? = addThms?_1 ∧
                                        mulThms? = mulThms?_1 ∧
                                          subThm? = subThm?_1 ∧
                                            negThm? = negThm?_1 ∧
                                              divThm? = divThm?_1 ∧
                                                modThm? = modThm?_1 ∧
                                                  powThm? = powThm?_1 ∧ zeroThm? = zeroThm?_1 ∧ ofNatThm? = ofNatThm?_1)