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