-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommRing.mk.injEq : ∀ (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)