-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.State.mk.inj : ∀ {rings : Array Lean.Meta.Grind.Arith.CommRing.CommRing} {typeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {exprToRingId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ} {semirings : Array Lean.Meta.Grind.Arith.CommRing.CommSemiring}
  {stypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {exprToSemiringId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ} {ncRings : Array Lean.Meta.Grind.Arith.CommRing.Ring}
  {exprToNCRingId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ} {nctypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {ncSemirings : Array Lean.Meta.Grind.Arith.CommRing.Semiring}
  {exprToNCSemiringId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ}
  {ncstypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)} {steps : ℕ} {reportedMaxDegreeIssue : Bool}
  {rings_1 : Array Lean.Meta.Grind.Arith.CommRing.CommRing}
  {typeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)} {exprToRingId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ}
  {semirings_1 : Array Lean.Meta.Grind.Arith.CommRing.CommSemiring}
  {stypeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {exprToSemiringId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ} {ncRings_1 : Array Lean.Meta.Grind.Arith.CommRing.Ring}
  {exprToNCRingId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ}
  {nctypeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {ncSemirings_1 : Array Lean.Meta.Grind.Arith.CommRing.Semiring}
  {exprToNCSemiringId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ}
  {ncstypeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)} {steps_1 : ℕ} {reportedMaxDegreeIssue_1 : Bool},
  { rings := rings, typeIdOf := typeIdOf, exprToRingId := exprToRingId, semirings := semirings, stypeIdOf := stypeIdOf,
        exprToSemiringId := exprToSemiringId, ncRings := ncRings, exprToNCRingId := exprToNCRingId,
        nctypeIdOf := nctypeIdOf, ncSemirings := ncSemirings, exprToNCSemiringId := exprToNCSemiringId,
        ncstypeIdOf := ncstypeIdOf, steps := steps, reportedMaxDegreeIssue := reportedMaxDegreeIssue } =
      { rings := rings_1, typeIdOf := typeIdOf_1, exprToRingId := exprToRingId_1, semirings := semirings_1,
        stypeIdOf := stypeIdOf_1, exprToSemiringId := exprToSemiringId_1, ncRings := ncRings_1,
        exprToNCRingId := exprToNCRingId_1, nctypeIdOf := nctypeIdOf_1, ncSemirings := ncSemirings_1,
        exprToNCSemiringId := exprToNCSemiringId_1, ncstypeIdOf := ncstypeIdOf_1, steps := steps_1,
        reportedMaxDegreeIssue := reportedMaxDegreeIssue_1 } →
    rings = rings_1 ∧
      typeIdOf = typeIdOf_1 ∧
        exprToRingId = exprToRingId_1 ∧
          semirings = semirings_1 ∧
            stypeIdOf = stypeIdOf_1 ∧
              exprToSemiringId = exprToSemiringId_1 ∧
                ncRings = ncRings_1 ∧
                  exprToNCRingId = exprToNCRingId_1 ∧
                    nctypeIdOf = nctypeIdOf_1 ∧
                      ncSemirings = ncSemirings_1 ∧
                        exprToNCSemiringId = exprToNCSemiringId_1 ∧
                          ncstypeIdOf = ncstypeIdOf_1 ∧
                            steps = steps_1 ∧ reportedMaxDegreeIssue = reportedMaxDegreeIssue_1