Update Defs.lea

leanprover-community · Jan 22, 2025 · 67f5043 · 67f5043
1 parent 455795a
commit 67f5043
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Group/Submonoid/Defs.lean b/Mathlib/Algebra/Group/Submonoid/Defs.lean
@@ -68,10 +68,6 @@ export ZeroMemClass (zero_mem)
 
 attribute [to_additive] OneMemClass
 
-/-
-Aesop attribute is for closing goals of the form `?x ∈ s`, allowing Aesop to show
-`[SetLike S M] [Zero/OneMemClass S M] (s : S) → ∃ x : M, x ∈ s`
--/
 attribute [simp, aesop safe apply (rule_sets := [SetLike])] one_mem zero_mem
 
 section