mathlib

abcd601c - fix(src/tactic/alias): Teach `get_alias_target` about `alias f ↔ a b` (#13742)

fix(src/tactic/alias): Teach `get_alias_target` about `alias f ↔ a b` (#13742) the `get_alias_target` function in `alias.lean` is used by the `to_additive` command to add the “Alias of …” docstring when creating an additive version of an existing alias (this was #13330). But `get_alias_target` did not work for `alias f ↔ a b`. This fixes it by extending the `alias_attr` map to not just store whether a defintion is an alias, but also what it is an alias of. Much more principled than trying to reconstruct the alias target from the RHS of the alias definition. Note that `alias` currently says “Alias of `foo_iff`” even though it’s really an alias of `foo_iff.mp`. This is an existing bug, not fixed in this PR – the effect is just that this “bug” will uniformly apply to additive lemmas as well. Hopefully will get rid of plenty of nolint.txt entries, and create better docs. Also improve the test file for the linter significantly.