feat(frontends/lean): avoid warning message

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/parser): bug in add_rewrite

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(builtin/num): prove basic theorems using simplifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker

We should not rely on this feature. It can be quite expensive.
We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as

   is_convertible(num, Nat)

If is_convertible starts unfolding opaque definitions, we would keep expanding num.

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