mathlib3

79abf670 - fix(tactic/apply_rules): separate single rules and attribute names in syntax (#13227)

fix(tactic/apply_rules): separate single rules and attribute names in syntax (#13227) @hrmacbeth reported an issue with `apply_rules` [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/monotonicity.2Eattr.20with.20apply_rules). It boiled down to `apply_rules` not properly distinguishing between attribute names, the names of `user_attribute` declarations, and the names of normal declarations. There's an example of using `apply_rules` with attributes in the docs: ```lean @[user_attribute] meta def mono_rules : user_attribute := { name := `mono_rules, descr := "lemmas usable to prove monotonicity" } local attribute [mono_rules] add_le_add example (a b c d : α) : a + b ≤ c + d := begin apply_rules mono_rules, -- takes action end ``` but this only worked by coincidence because the attribute name and the name of the `user_attribute` declaration were the same. With this change, expressions and names of attributes are now separated: the latter are specified after `with`. The call above becomes `apply_rules with mono_rules`. This mirrors the syntax of `simp`. Note that this feature was only used in meta code in mathlib. The example from Zulip (modified for proper syntax) still doesn't work with my change: ```lean import tactic.monotonicity variables {α : Type*} [linear_ordered_add_comm_group α] example (a b c d : α) : a + b ≤ c + d := begin apply_rules with mono, end ``` but it seems to fail because the `mono` rules cause `apply_rules` to loop -- that is, the rule set is getting applied correctly. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>