fix(frontends/lean/builtin_cmds): allow 'check' command to unfold the current module opaque definitions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean/run): add another class-instance example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean/run): add another class-instance example