feat: add a SetLike default rule set for aesop (#7111)

This creates a new `aesop` rule set called `SetLike` to house lemmas about membership in subobjects.

Lemmas like `pow_mem` should be included in the rule set:
```lean
@[to_additive (attr := aesop safe apply (rule_sets [SetLike]))]
theorem pow_mem {M A} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x : M}
(hx : x ∈ S) : ∀ n : ℕ, x ^ n ∈ S
```

Lemmas about closures, like `AddSubmonoid.closure` should be included in the rule set, but they should be assigned a penalty (here we choose `20` throughout) so that they are not attempted before the general purpose ones like `pow_mem`.
```lean
@[to_additive (attr := simp, aesop safe 20 apply (rule_sets [SetLike]))
  "The `AddSubmonoid` generated by a set includes the set."]
theorem subset_closure : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx
```

In order for `aesop` to make effective use of `AddSubmonoid.closure` it needs the following new lemma.
```lean
@[aesop 5% apply (rule_sets [SetLike])]
lemma mem_of_subset {s : Set B} (hp : s ⊆ p) {x : B} (hx : x ∈ s) : x ∈ p := hp hx
```
Note: this lemma is marked as very unsafe (`5%`) because it will apply *whenever* the goal is of the form `x ∈ p` where `p` is any term of a `SetLike` instance; and moreover, it will create `s` as a metavariable, which is in general a terrible idea, but necessary for the reason mentioned above.

Mathlib.lean

@@ -3223,6 +3223,7 @@ import Mathlib.Tactic.Sat.FromLRAT
 import Mathlib.Tactic.Says
 import Mathlib.Tactic.ScopedNS
 import Mathlib.Tactic.Set
+import Mathlib.Tactic.SetLike
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.Simps.Basic

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -514,6 +514,7 @@ theorem adjoin_toSubmodule (s : Set A) :
     (adjoin R s).toSubmodule = Submodule.span R (NonUnitalSubsemiring.closure s : Set A) :=
   rfl
 
+@[aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_adjoin {s : Set A} : s ⊆ adjoin R s :=
   NonUnitalSubsemiring.subset_closure.trans Submodule.subset_span
 

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -104,6 +104,7 @@ variable (S : Subalgebra R A)
 instance instSMulMemClass : SMulMemClass (Subalgebra R A) R A where
   smul_mem {S} r x hx := (Algebra.smul_def r x).symm ▸ mul_mem (S.algebraMap_mem' r) hx
 
+@[aesop safe apply (rule_sets [SetLike])]
 theorem _root_.algebraMap_mem {S R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
     [SetLike S A] [OneMemClass S A] [SMulMemClass S R A] (s : S) (r : R) :
     algebraMap R A r ∈ s :=

Mathlib/Algebra/Star/Basic.lean

@@ -62,6 +62,8 @@ class StarMemClass (S R : Type*) [Star R] [SetLike S R] : Prop where
 
 export StarMemClass (star_mem)
 
+attribute [aesop safe apply (rule_sets [SetLike])] star_mem
+
 namespace StarMemClass
 
 variable {S : Type w} [Star R] [SetLike S R] [hS : StarMemClass S R] (s : S)

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -633,6 +633,7 @@ theorem adjoin_toNonUnitalSubalgebra (s : Set A) :
     (adjoin R s).toNonUnitalSubalgebra = NonUnitalAlgebra.adjoin R (s ∪ star s) :=
   rfl
 
+@[aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_adjoin (s : Set A) : s ⊆ adjoin R s :=
   (Set.subset_union_left s (star s)).trans <| NonUnitalAlgebra.subset_adjoin R
 

Mathlib/Algebra/Star/SelfAdjoint.lean

@@ -528,6 +528,7 @@ section SMul
 
 variable [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A]
 
+@[aesop safe apply (rule_sets [SetLike])]
 theorem smul_mem [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) {x : A}
     (h : x ∈ skewAdjoint A) : r • x ∈ skewAdjoint A := by
   rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]

Mathlib/Algebra/Star/Subalgebra.lean

@@ -445,6 +445,7 @@ theorem adjoin_toSubalgebra (s : Set A) :
   rfl
 #align star_subalgebra.adjoin_to_subalgebra StarSubalgebra.adjoin_toSubalgebra
 
+@[aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_adjoin (s : Set A) : s ⊆ adjoin R s :=
   (Set.subset_union_left s (star s)).trans Algebra.subset_adjoin
 #align star_subalgebra.subset_adjoin StarSubalgebra.subset_adjoin

Mathlib/Analysis/Convex/Cone/Basic.lean

@@ -114,6 +114,7 @@ theorem ext {S T : ConvexCone 𝕜 E} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T :
   SetLike.ext h
 #align convex_cone.ext ConvexCone.ext
 
+@[aesop safe apply (rule_sets [SetLike])]
 theorem smul_mem {c : 𝕜} {x : E} (hc : 0 < c) (hx : x ∈ S) : c • x ∈ S :=
   S.smul_mem' hc hx
 #align convex_cone.smul_mem ConvexCone.smul_mem

Mathlib/Data/SetLike/Basic.lean

@@ -5,6 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Data.Set.Basic
 import Mathlib.Tactic.Monotonicity.Attr
+import Mathlib.Tactic.SetLike
 
 #align_import data.set_like.basic from "leanprover-community/mathlib"@"feb99064803fd3108e37c18b0f77d0a8344677a3"
 
@@ -174,6 +175,9 @@ theorem coe_mem (x : p) : (x : B) ∈ p :=
   x.2
 #align set_like.coe_mem SetLike.coe_mem
 
+@[aesop 5% apply (rule_sets [SetLike])]
+lemma mem_of_subset {s : Set B} (hp : s ⊆ p) {x : B} (hx : x ∈ s) : x ∈ p := hp hx
+
 -- porting note: removed `@[simp]` because `simpNF` linter complained
 protected theorem eta (x : p) (hx : (x : B) ∈ p) : (⟨x, hx⟩ : p) = x := rfl
 #align set_like.eta SetLike.eta

Mathlib/FieldTheory/Subfield.lean

@@ -88,6 +88,7 @@ instance (priority := 100) toSubgroupClass : SubgroupClass S K :=
 
 variable {S}
 
+@[aesop safe apply (rule_sets [SetLike])]
 theorem coe_rat_mem (s : S) (x : ℚ) : (x : K) ∈ s := by
   simpa only [Rat.cast_def] using div_mem (coe_int_mem s x.num) (coe_nat_mem s x.den)
 #align subfield_class.coe_rat_mem SubfieldClass.coe_rat_mem
@@ -101,10 +102,16 @@ theorem coe_rat_cast (s : S) (x : ℚ) : ((x : s) : K) = x :=
 #align subfield_class.coe_rat_cast SubfieldClass.coe_rat_cast
 
 -- Porting note: Mistranslated: used to be (a • x : K) ∈ s
+@[aesop safe apply (rule_sets [SetLike])]
 theorem rat_smul_mem (s : S) (a : ℚ) (x : s) : a • (x : K) ∈ s := by
   simpa only [Rat.smul_def] using mul_mem (coe_rat_mem s a) x.prop
 #align subfield_class.rat_smul_mem SubfieldClass.rat_smul_mem
 
+@[aesop safe apply (rule_sets [SetLike])]
+lemma ofScientific_mem (s : S) {b : Bool} {n m : ℕ} :
+    (OfScientific.ofScientific n b m : K) ∈ s :=
+  SubfieldClass.coe_rat_mem ..
+
 instance (s : S) : SMul ℚ s :=
   ⟨fun a x => ⟨a • (x : K), rat_smul_mem s a x⟩⟩
 
@@ -694,7 +701,7 @@ theorem subring_closure_le (s : Set K) : Subring.closure s ≤ (closure s).toSub
 #align subfield.subring_closure_le Subfield.subring_closure_le
 
 /-- The subfield generated by a set includes the set. -/
-@[simp]
+@[simp, aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_closure {s : Set K} : s ⊆ closure s :=
   Set.Subset.trans Subring.subset_closure (subring_closure_le s)
 #align subfield.subset_closure Subfield.subset_closure

Mathlib/GroupTheory/GroupAction/SubMulAction.lean

@@ -63,6 +63,8 @@ class VAddMemClass (S : Type*) (R : outParam <| Type*) (M : Type*) [VAdd R M] [S
 
 attribute [to_additive] SMulMemClass
 
+attribute [aesop safe 10 apply (rule_sets [SetLike])] SMulMemClass.smul_mem VAddMemClass.vadd_mem
+
 /-- Not registered as an instance because `R` is an `outParam` in `SMulMemClass S R M`. -/
 lemma AddSubmonoidClass.nsmulMemClass {S M : Type*} [AddMonoid M] [SetLike S M]
     [AddSubmonoidClass S M] : SMulMemClass S ℕ M where

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -124,6 +124,8 @@ class AddSubgroupClass (S G : Type*) [SubNegMonoid G] [SetLike S G] extends AddS
 
 attribute [to_additive] InvMemClass SubgroupClass
 
+attribute [aesop safe apply (rule_sets [SetLike])] inv_mem neg_mem
+
 @[to_additive (attr := simp)]
 theorem inv_mem_iff {S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G] {H : S}
     {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
@@ -138,13 +140,14 @@ theorem inv_mem_iff {S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G]
 variable {M S : Type*} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {H K : S}
 
 /-- A subgroup is closed under division. -/
-@[to_additive "An additive subgroup is closed under subtraction."]
+@[to_additive (attr := aesop safe apply (rule_sets [SetLike]))
+  "An additive subgroup is closed under subtraction."]
 theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H := by
   rw [div_eq_mul_inv]; exact mul_mem hx (inv_mem hy)
 #align div_mem div_mem
 #align sub_mem sub_mem
 
-@[to_additive]
+@[to_additive (attr := aesop safe apply (rule_sets [SetLike]))]
 theorem zpow_mem {x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
   | (n : ℕ) => by
     rw [zpow_ofNat]
@@ -1108,7 +1111,8 @@ theorem mem_closure {x : G} : x ∈ closure k ↔ ∀ K : Subgroup G, k ⊆ K 
 #align add_subgroup.mem_closure AddSubgroup.mem_closure
 
 /-- The subgroup generated by a set includes the set. -/
-@[to_additive (attr := simp) "The `AddSubgroup` generated by a set includes the set."]
+@[to_additive (attr := simp, aesop safe 20 apply (rule_sets [SetLike]))
+  "The `AddSubgroup` generated by a set includes the set."]
 theorem subset_closure : k ⊆ closure k := fun _ hx => mem_closure.2 fun _ hK => hK hx
 #align subgroup.subset_closure Subgroup.subset_closure
 #align add_subgroup.subset_closure AddSubgroup.subset_closure

Mathlib/GroupTheory/Submonoid/Basic.lean

@@ -85,6 +85,8 @@ export ZeroMemClass (zero_mem)
 
 attribute [to_additive] OneMemClass
 
+attribute [aesop safe apply (rule_sets [SetLike])] one_mem zero_mem
+
 section
 
 /-- A submonoid of a monoid `M` is a subset containing 1 and closed under multiplication. -/
@@ -129,7 +131,7 @@ class AddSubmonoidClass (S : Type*) (M : Type*) [AddZeroClass M] [SetLike S M] e
 
 attribute [to_additive] Submonoid SubmonoidClass
 
-@[to_additive]
+@[to_additive (attr := aesop safe apply (rule_sets [SetLike]))]
 theorem pow_mem {M A} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x : M}
     (hx : x ∈ S) : ∀ n : ℕ, x ^ n ∈ S
   | 0 => by
@@ -393,7 +395,8 @@ theorem mem_closure {x : M} : x ∈ closure s ↔ ∀ S : Submonoid M, s ⊆ S 
 #align add_submonoid.mem_closure AddSubmonoid.mem_closure
 
 /-- The submonoid generated by a set includes the set. -/
-@[to_additive (attr := simp) "The `AddSubmonoid` generated by a set includes the set."]
+@[to_additive (attr := simp, aesop safe 20 apply (rule_sets [SetLike]))
+  "The `AddSubmonoid` generated by a set includes the set."]
 theorem subset_closure : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx
 #align submonoid.subset_closure Submonoid.subset_closure
 #align add_submonoid.subset_closure AddSubmonoid.subset_closure

Mathlib/GroupTheory/Subsemigroup/Basic.lean

@@ -76,6 +76,8 @@ export AddMemClass (add_mem)
 
 attribute [to_additive] MulMemClass
 
+attribute [aesop safe apply (rule_sets [SetLike])] mul_mem add_mem
+
 /-- A subsemigroup of a magma `M` is a subset closed under multiplication. -/
 structure Subsemigroup (M : Type*) [Mul M] where
   /-- The carrier of a subsemigroup. -/
@@ -306,7 +308,8 @@ theorem mem_closure {x : M} : x ∈ closure s ↔ ∀ S : Subsemigroup M, s ⊆
 #align add_subsemigroup.mem_closure AddSubsemigroup.mem_closure
 
 /-- The subsemigroup generated by a set includes the set. -/
-@[to_additive (attr := simp) "The `AddSubsemigroup` generated by a set includes the set."]
+@[to_additive (attr := simp, aesop safe 20 apply (rule_sets [SetLike]))
+  "The `AddSubsemigroup` generated by a set includes the set."]
 theorem subset_closure : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx
 #align subsemigroup.subset_closure Subsemigroup.subset_closure
 #align add_subsemigroup.subset_closure AddSubsemigroup.subset_closure

Mathlib/LinearAlgebra/Span.lean

@@ -58,6 +58,7 @@ theorem mem_span : x ∈ span R s ↔ ∀ p : Submodule R M, s ⊆ p → x ∈ p
   mem_iInter₂
 #align submodule.mem_span Submodule.mem_span
 
+@[aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_span : s ⊆ span R s := fun _ h => mem_span.2 fun _ hp => hp h
 #align submodule.subset_span Submodule.subset_span
 

Mathlib/RingTheory/Adjoin/Basic.lean

@@ -40,6 +40,7 @@ variable [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B]
 variable [Algebra R S] [Algebra R A] [Algebra S A] [Algebra R B] [IsScalarTower R S A]
 variable {s t : Set A}
 
+@[aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_adjoin : s ⊆ adjoin R s :=
   Algebra.gc.le_u_l s
 #align algebra.subset_adjoin Algebra.subset_adjoin

Mathlib/RingTheory/NonUnitalSubring/Basic.lean

@@ -646,7 +646,7 @@ theorem mem_closure {x : R} {s : Set R} : x ∈ closure s ↔ ∀ S : NonUnitalS
   mem_sInf
 
 /-- The `NonUnitalSubring` generated by a set includes the set. -/
-@[simp]
+@[simp, aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_closure {s : Set R} : s ⊆ closure s := fun _x hx => mem_closure.2 fun _S hS => hS hx
 
 theorem not_mem_of_not_mem_closure {s : Set R} {P : R} (hP : P ∉ closure s) : P ∉ s := fun h =>

Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

@@ -567,7 +567,7 @@ theorem mem_closure {x : R} {s : Set R} :
 #align non_unital_subsemiring.mem_closure NonUnitalSubsemiring.mem_closure
 
 /-- The non-unital subsemiring generated by a set includes the set. -/
-@[simp]
+@[simp, aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_closure {s : Set R} : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx
 #align non_unital_subsemiring.subset_closure NonUnitalSubsemiring.subset_closure
 

Mathlib/RingTheory/Subring/Basic.lean

@@ -86,6 +86,7 @@ instance (priority := 100) SubringClass.addSubgroupClass (S : Type*) (R : Type u
 
 variable [SetLike S R] [hSR : SubringClass S R] (s : S)
 
+@[aesop safe apply (rule_sets [SetLike])]
 theorem coe_int_mem (n : ℤ) : (n : R) ∈ s := by simp only [← zsmul_one, zsmul_mem, one_mem]
 #align coe_int_mem coe_int_mem
 
@@ -896,7 +897,7 @@ theorem mem_closure {x : R} {s : Set R} : x ∈ closure s ↔ ∀ S : Subring R,
 #align subring.mem_closure Subring.mem_closure
 
 /-- The subring generated by a set includes the set. -/
-@[simp]
+@[simp, aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_closure {s : Set R} : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx
 #align subring.subset_closure Subring.subset_closure
 

Mathlib/RingTheory/Subsemiring/Basic.lean

@@ -37,10 +37,16 @@ class AddSubmonoidWithOneClass (S R : Type*) [AddMonoidWithOne R]
 
 variable {S R : Type*} [AddMonoidWithOne R] [SetLike S R] (s : S)
 
+@[aesop safe apply (rule_sets [SetLike])]
 theorem natCast_mem [AddSubmonoidWithOneClass S R] (n : ℕ) : (n : R) ∈ s := by
   induction n <;> simp [zero_mem, add_mem, one_mem, *]
 #align nat_cast_mem natCast_mem
 
+@[aesop safe apply (rule_sets [SetLike])]
+lemma ofNat_mem [AddSubmonoidWithOneClass S R] (s : S) (n : ℕ) [n.AtLeastTwo] :
+    no_index (OfNat.ofNat n) ∈ s := by
+  rw [←Nat.cast_eq_ofNat]; exact natCast_mem s n
+
 instance (priority := 74) AddSubmonoidWithOneClass.toAddMonoidWithOne
     [AddSubmonoidWithOneClass S R] : AddMonoidWithOne s :=
   { AddSubmonoidClass.toAddMonoid s with
@@ -803,7 +809,7 @@ theorem mem_closure {x : R} {s : Set R} : x ∈ closure s ↔ ∀ S : Subsemirin
 #align subsemiring.mem_closure Subsemiring.mem_closure
 
 /-- The subsemiring generated by a set includes the set. -/
-@[simp]
+@[simp, aesop safe 20 apply (rule_sets [SetLike])]
 theorem subset_closure {s : Set R} : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx
 #align subsemiring.subset_closure Subsemiring.subset_closure
 

Mathlib/Tactic.lean

@@ -143,6 +143,7 @@ import Mathlib.Tactic.Sat.FromLRAT
 import Mathlib.Tactic.Says
 import Mathlib.Tactic.ScopedNS
 import Mathlib.Tactic.Set
+import Mathlib.Tactic.SetLike
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.Simps.Basic

Mathlib/Tactic/SetLike.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2023 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+
+import Aesop
+
+/-!
+# SetLike Rule Set
+
+This module defines the `SetLike` Aesop rule set which is used by the
+`set_like` tactic. Aesop rule sets only become visible once the file in which
+they're declared is imported, so we must put this declaration into its own file.
+-/
+
+declare_aesop_rule_sets [SetLike] (default := true)

Mathlib/Topology/Algebra/Algebra.lean

@@ -171,6 +171,7 @@ def Algebra.elementalAlgebra (x : A) : Subalgebra R A :=
   (Algebra.adjoin R ({x} : Set A)).topologicalClosure
 #align algebra.elemental_algebra Algebra.elementalAlgebra
 
+@[aesop safe apply (rule_sets [SetLike])]
 theorem Algebra.self_mem_elementalAlgebra (x : A) : x ∈ Algebra.elementalAlgebra R x :=
   SetLike.le_def.mp (Subalgebra.le_topologicalClosure (Algebra.adjoin R ({x} : Set A))) <|
     Algebra.self_mem_adjoin_singleton R x

Mathlib/Topology/Algebra/StarSubalgebra.lean

@@ -205,6 +205,7 @@ def elementalStarAlgebra (x : A) : StarSubalgebra R A :=
 
 namespace elementalStarAlgebra
 
+@[aesop safe apply (rule_sets [SetLike])]
 theorem self_mem (x : A) : x ∈ elementalStarAlgebra R x :=
   SetLike.le_def.mp (le_topologicalClosure _) (self_mem_adjoin_singleton R x)
 #align elemental_star_algebra.self_mem elementalStarAlgebra.self_mem

test/set_like.lean

@@ -0,0 +1,51 @@
+import Mathlib.Algebra.Star.Subalgebra
+import Mathlib.Algebra.Star.SelfAdjoint
+import Mathlib.Algebra.Star.NonUnitalSubalgebra
+import Mathlib.FieldTheory.Subfield
+
+set_option autoImplicit true
+
+example [Ring R] (S : Subring R) (hx : x ∈ S) (hy : y ∈ S) (hz : z ∈ S) (n m : ℕ) :
+    n • x ^ 3 - 2 • y + z ^ m ∈ S := by
+  aesop
+
+example [Ring R] (S : Set R) (hx : x ∈ S) (hy : y ∈ S) (hz : z ∈ S) (n m : ℕ) :
+    n • x ^ 3 - y + z ^ m ∈ Subring.closure S := by
+  aesop
+
+example [CommRing R] [Ring A] [Algebra R A] [StarRing R] [StarRing A] [StarModule R A]
+    (r : R) (a b c : A) (n : ℕ) :
+    -b + star (algebraMap R A r) + a ^ n * c ∈ StarSubalgebra.adjoin R {a, b, c} := by
+  aesop
+
+example [Monoid M] (x : M) (n : ℕ) : x ^ n ∈ Submonoid.closure {x} := by
+  aesop
+
+example [Monoid M] (x y z w : M) (n : ℕ) : (x * y) ^ n * w ∈ Submonoid.closure {x, y, z, w} := by
+  aesop
+
+example [Group M] (x : M) (n : ℤ) : x ^ n ∈ Subgroup.closure {x} := by
+  aesop
+
+example [Monoid M] (x y z : M) (S₁ S₂ : Submonoid M) (h : S₁ ≤ S₂) (hx : x ∈ S₁)
+    (hy : y ∈ S₁) (hz : z ∈ S₂) :
+    x * y * z ∈ S₂ := by
+  aesop
+
+example [Monoid M] (x y z : M) (S₁ S₂ : Submonoid M) (h : S₁ ≤ S₂) (hx : x ∈ S₁)
+    (hy : y ∈ S₁) (hz : z ∈ S₂) :
+    x * y * z ∈ S₁ ⊔ S₂ := by
+  aesop
+
+example [Monoid M] (x y z : M) (S : Submonoid M) (hxy : x * y ∈ S)  (hz : z ∈ S) :
+    z * (x * y) ∈ S := by
+  aesop
+
+example [Field F] (S : Subfield F) (q : ℚ) : (q : F) ∈ S := by
+  aesop
+
+example [Field F] (S : Subfield F) : (1.2 : F) ∈ S := by
+  aesop
+
+example [Field F] (S : Subfield F) (x : F) (hx : x ∈ S) : ((12e-100 : F) • x⁻¹) ∈ S := by
+  aesop