From 631cd406967325d1fd41a6f1d41784c93a97eb55 Mon Sep 17 00:00:00 2001 From: artie2000 Date: Wed, 22 Jan 2025 00:36:51 +0000 Subject: [PATCH] docs --- Mathlib/Tactic/SetLike.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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: