feat(tactic/ext): don't remove attr (#15502)
In #8785 the ext attribute was changed to try to remove itself after it is applied, unfortunately this is not possible however.
The command `unset_attribute` is not persistent, as seen in https://github.com/leanprover-community/lean/blob/bf12a6c9b74846b532a248617eae692d2c13f18b/src/library/tactic/user_attribute.cpp#L365.
This means that even though it appears that a declaration doesn't have the `ext` attribute when `#print`ed immediately after, the attribute reappears after the namespace is closed
This leads to weird discrepancies like the following:
https://leanprover-community.github.io/mathlib_docs/topology/algebra/open_subgroup.html#open_subgroup.ext
where the `to_additive` version of the lemma doesn't have the `ext` attribute in doc-gen (as it is copied immediately, so before the end of the current scope), but the original does have the attribute, as it only temporarily didn't.
To resolve this we simply give up on removing the `ext` attribute.
