Printing multiple commands using Try this

Stream: metaprogramming / tactics

[Paul Lezeau]

I'm trying to write a command that prints out a "try this" suggestion with multiple commands. Is there a clean way of doing this?
E.g. my first attempt was something along the lines of the following:

import Mathlib
open Lean Elab Tactic Meta Tactic.TryThis Command

elab "#testing " : command => Command.liftTermElabM do
  let command1 : Command ← `( #check Nat.add)
  let command2 : Command ← `( #check Nat.div)
  let command : Command ← `($command1:command $command2:command)
  let suggestion : SuggestionText := .tsyntax command
  let suggestion : Suggestion := { suggestion := suggestion }
  addSuggestion (← getRef) suggestion

but this doesn't work.

[Paul Lezeau]

The idea would be to get both commands simultaneously when clicking on the try this, rather than getting multiple try this suggestions by using addSuggestions