{u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {a : Q(«$α»)} →
        (rα : Q(CommRing «$α»)) →
          Mathlib.Tactic.Ring.ExProd sα a →
            Lean.MetaM (Mathlib.Tactic.Ring.Result (Mathlib.Tactic.Ring.ExProd sα) q(-«$a»))