{motive : Lean.Meta.Grind.Arith.CommRing.CommSemiring → Sort u} →
  (t : Lean.Meta.Grind.Arith.CommRing.CommSemiring) →
    ((toSemiring : Lean.Meta.Grind.Arith.CommRing.Semiring) →
        (ringId : ℕ) →
          (commSemiringInst : Lean.Expr) →
            (addRightCancelInst? : Option (Option Lean.Expr)) →
              (toQFn? : Option Lean.Expr) →
                motive
                  { toSemiring := toSemiring, ringId := ringId, commSemiringInst := commSemiringInst,
                    addRightCancelInst? := addRightCancelInst?, toQFn? := toQFn? }) →
      motive t