∀ {toRing : Lean.Meta.Grind.Arith.CommRing.Ring} {invFn? : Option Lean.Expr} {semiringId? : Option ℕ}
  {commSemiringInst commRingInst : Lean.Expr} {noZeroDivInst? fieldInst? : Option 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}
  {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}
  {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} {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?,
        denoteEntries := denoteEntries, nextId := nextId, steps := steps, queue := queue, basis := basis,
        diseqs := diseqs, recheck := recheck, invSet := invSet, 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,
        denoteEntries := denoteEntries_1, nextId := nextId_1, steps := steps_1, queue := queue_1, basis := basis_1,
        diseqs := diseqs_1, recheck := recheck_1, invSet := invSet_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 ∧
                  denoteEntries = denoteEntries_1 ∧
                    nextId = nextId_1 ∧
                      steps = steps_1 ∧
                        queue = queue_1 ∧
                          basis = basis_1 ∧
                            diseqs = diseqs_1 ∧
                              recheck = recheck_1 ∧
                                invSet = invSet_1 ∧ numEq0? = numEq0?_1 ∧ numEq0Updated = numEq0Updated_1