diff --git a/Mathlib/Tactic/SetLike.lean b/Mathlib/Tactic/SetLike.lean index 02aacdaa79c2a..9c8aa3e5d5e27 100644 --- a/Mathlib/Tactic/SetLike.lean +++ b/Mathlib/Tactic/SetLike.lean @@ -18,7 +18,7 @@ so we must put this declaration into its own file. declare_aesop_rule_sets [SetLike] (default := true) declare_aesop_rule_sets [SetLike!] (default := false) -library_note "SetLike Aesop lemmas"/-- +library_note "SetLike Aesop ruleset"/-- The Aesop tactic (`aesop`) can automatically prove obvious facts about membership in structures such as subgroups and subrings. Certain lemmas regarding membership in algebraic substructures are given the `aesop` attribute according to the following principles: