-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.mk.inj : ∀ {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 ∧ ⋯