refactor(frontends/lean): remove unnecessary files
refactor(frontends/lean): remove dead code
refactor(library/tactic): remove unnecessary hack

It is not needed anymore.
We had to use this hack when we had tactic_macro_definition_cell.