feat(frontends/lean): remove tactic hints for specific classes

The idea is to separate class-instance resolution and tactic framework
as two independent engines.
refactor(frontends/lean/tactic_hint): simplify tactic_hints