-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.mk.injEq : ∀ (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) (id_1 : ℕ)
  (ringId?_1 : Option ℕ) (type_1 : Lean.Expr) (u_1 : Lean.Level) (intModuleInst_1 : Lean.Expr)
  (leInst?_1 ltInst?_1 lawfulOrderLTInst?_1 isPreorderInst?_1 orderedAddInst?_1 isLinearInst?_1 noNatDivInst?_1
    ringInst?_1 commRingInst?_1 orderedRingInst?_1 fieldInst?_1 : Option Lean.Expr)
  (charInst?_1 : Option (Lean.Expr × ℕ)) (zero_1 ofNatZero_1 : Lean.Expr) (one?_1 leFn?_1 ltFn?_1 : Option Lean.Expr)
  (addFn_1 zsmulFn_1 nsmulFn_1 : Lean.Expr) (zsmulFn?_1 nsmulFn?_1 homomulFn?_1 : Option Lean.Expr)
  (subFn_1 negFn_1 : Lean.Expr) (vars_1 : Lean.PArray Lean.Expr)
  (varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.Linarith.Var)
  (lowers_1 uppers_1 : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Linear.IneqCnstr))
  (diseqs_1 : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Linear.DiseqCnstr)) (assignment_1 : Lean.PArray ℚ)
  (caseSplits_1 : Bool) (conflict?_1 : Option Lean.Meta.Grind.Arith.Linear.UnsatProof)
  (diseqSplits_1 : Lean.PHashMap Lean.Grind.Linarith.Poly Lean.FVarId)
  (elimEqs_1 : Lean.PArray (Option Lean.Meta.Grind.Arith.Linear.EqCnstr)) (elimStack_1 : List Lean.Grind.Linarith.Var)
  (occurs_1 : Lean.PArray Lean.Meta.Grind.Arith.Linear.VarSet) (ignored_1 : Lean.PArray Lean.Expr),
  ({ 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 } =
      { id := id_1, ringId? := ringId?_1, type := type_1, u := u_1, intModuleInst := intModuleInst_1,
        leInst? := leInst?_1, ltInst? := ltInst?_1, lawfulOrderLTInst? := lawfulOrderLTInst?_1,
        isPreorderInst? := isPreorderInst?_1, orderedAddInst? := orderedAddInst?_1, isLinearInst? := isLinearInst?_1,
        noNatDivInst? := noNatDivInst?_1, ringInst? := ringInst?_1, commRingInst? := commRingInst?_1,
        orderedRingInst? := orderedRingInst?_1, fieldInst? := fieldInst?_1, charInst? := charInst?_1, zero := zero_1,
        ofNatZero := ofNatZero_1, one? := one?_1, leFn? := leFn?_1, ltFn? := ltFn?_1, addFn := addFn_1,
        zsmulFn := zsmulFn_1, nsmulFn := nsmulFn_1, zsmulFn? := zsmulFn?_1, nsmulFn? := nsmulFn?_1,
        homomulFn? := homomulFn?_1, subFn := subFn_1, negFn := negFn_1, vars := vars_1, varMap := varMap_1,
        lowers := lowers_1, uppers := uppers_1, diseqs := diseqs_1, assignment := assignment_1,
        caseSplits := caseSplits_1, conflict? := conflict?_1, diseqSplits := diseqSplits_1, elimEqs := elimEqs_1,
        elimStack := elimStack_1, occurs := occurs_1, ignored := ignored_1 }) =
    (id = id_1 ∧ ringId? = ringId?_1 ∧ ⋯)