-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommRing.mk.inj : ∀ {toRing : Lean.Meta.Grind.Arith.CommRing.Ring} {invFn? : Option Lean.Expr} {semiringId? : Option ℕ}
  {commSemiringInst commRingInst : Lean.Expr} {noZeroDivInst? fieldInst? : Option Lean.Expr}
  {powIdentityInst? : Option (Lean.Expr × Lean.Expr × ℕ)}
  {denoteEntries : Lean.PArray (Lean.Expr × Lean.Meta.Grind.Arith.CommRing.RingExpr)} {nextId steps : ℕ}
  {queue : Lean.Meta.Grind.Arith.CommRing.Queue} {basis : List Lean.Meta.Grind.Arith.CommRing.EqCnstr}
  {diseqs : Lean.PArray Lean.Meta.Grind.Arith.CommRing.DiseqCnstr} {recheck : Bool} {invSet : Lean.PHashSet Lean.Expr}
  {powIdentityVarCount : ℕ} {numEq0? : Option Lean.Meta.Grind.Arith.CommRing.EqCnstr} {numEq0Updated : Bool}
  {toRing_1 : Lean.Meta.Grind.Arith.CommRing.Ring} {invFn?_1 : Option Lean.Expr} {semiringId?_1 : Option ℕ}
  {commSemiringInst_1 commRingInst_1 : Lean.Expr} {noZeroDivInst?_1 fieldInst?_1 : Option Lean.Expr}
  {powIdentityInst?_1 : Option (Lean.Expr × Lean.Expr × ℕ)}
  {denoteEntries_1 : Lean.PArray (Lean.Expr × Lean.Meta.Grind.Arith.CommRing.RingExpr)} {nextId_1 steps_1 : ℕ}
  {queue_1 : Lean.Meta.Grind.Arith.CommRing.Queue} {basis_1 : List Lean.Meta.Grind.Arith.CommRing.EqCnstr}
  {diseqs_1 : Lean.PArray Lean.Meta.Grind.Arith.CommRing.DiseqCnstr} {recheck_1 : Bool}
  {invSet_1 : Lean.PHashSet Lean.Expr} {powIdentityVarCount_1 : ℕ}
  {numEq0?_1 : Option Lean.Meta.Grind.Arith.CommRing.EqCnstr} {numEq0Updated_1 : Bool},
  { toRing := toRing, invFn? := invFn?, semiringId? := semiringId?, commSemiringInst := commSemiringInst,
        commRingInst := commRingInst, noZeroDivInst? := noZeroDivInst?, fieldInst? := fieldInst?,
        powIdentityInst? := powIdentityInst?, denoteEntries := denoteEntries, nextId := nextId, steps := steps,
        queue := queue, basis := basis, diseqs := diseqs, recheck := recheck, invSet := invSet,
        powIdentityVarCount := powIdentityVarCount, numEq0? := numEq0?, numEq0Updated := numEq0Updated } =
      { toRing := toRing_1, invFn? := invFn?_1, semiringId? := semiringId?_1, commSemiringInst := commSemiringInst_1,
        commRingInst := commRingInst_1, noZeroDivInst? := noZeroDivInst?_1, fieldInst? := fieldInst?_1,
        powIdentityInst? := powIdentityInst?_1, denoteEntries := denoteEntries_1, nextId := nextId_1, steps := steps_1,
        queue := queue_1, basis := basis_1, diseqs := diseqs_1, recheck := recheck_1, invSet := invSet_1,
        powIdentityVarCount := powIdentityVarCount_1, numEq0? := numEq0?_1, numEq0Updated := numEq0Updated_1 } →
    toRing = toRing_1 ∧
      invFn? = invFn?_1 ∧
        semiringId? = semiringId?_1 ∧
          commSemiringInst = commSemiringInst_1 ∧
            commRingInst = commRingInst_1 ∧
              noZeroDivInst? = noZeroDivInst?_1 ∧
                fieldInst? = fieldInst?_1 ∧
                  powIdentityInst? = powIdentityInst?_1 ∧
                    denoteEntries = denoteEntries_1 ∧
                      nextId = nextId_1 ∧
                        steps = steps_1 ∧
                          queue = queue_1 ∧
                            basis = basis_1 ∧
                              diseqs = diseqs_1 ∧
                                recheck = recheck_1 ∧
                                  invSet = invSet_1 ∧
                                    powIdentityVarCount = powIdentityVarCount_1 ∧
                                      numEq0? = numEq0?_1 ∧ numEq0Updated = numEq0Updated_1