feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>