replace messy simps with clean Aesop API

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -566,7 +566,7 @@ variable {R}
 
 /-- The `NonUnitalStarSubalgebra` obtained from `S : NonUnitalSubalgebra R A` by taking the
 smallest non-unital subalgebra containing both `S` and `star S`. -/
-@[simps!]
+@[simps toNonUnitalSubalgebra]
 def starClosure (S : NonUnitalSubalgebra R A) : NonUnitalStarSubalgebra R A where
   toNonUnitalSubalgebra := S ⊔ star S
   star_mem' := @fun a (ha : a ∈ S ⊔ star S) => show star a ∈ S ⊔ star S by
@@ -575,6 +575,32 @@ def starClosure (S : NonUnitalSubalgebra R A) : NonUnitalStarSubalgebra R A wher
     simp only [Set.sup_eq_union, star_adjoin_comm, Set.union_star, coe_star, star_star,
       Set.union_comm]
 
+theorem le_starClosure_toNonUnitalSubalgebra (S : NonUnitalSubalgebra R A) :
+    S ≤ S.starClosure.toNonUnitalSubalgebra := by
+  rw [starClosure_toNonUnitalSubalgebra]; simp
+
+theorem star_le_starClosure_toNonUnitalSubalgebra (S : NonUnitalSubalgebra R A) :
+    star S ≤ S.starClosure.toNonUnitalSubalgebra := by
+  rw [starClosure_toNonUnitalSubalgebra]; simp
+
+@[aesop safe 20 apply (rule_sets := [SetLike])]
+theorem subset_starClosure (S : NonUnitalSubalgebra R A) :
+    (S : Set A) ⊆ S.starClosure.toNonUnitalSubalgebra :=
+  le_starClosure_toNonUnitalSubalgebra _
+
+@[aesop safe 20 apply (rule_sets := [SetLike])]
+theorem star_subset_starClosure (S : NonUnitalSubalgebra R A) :
+    (star S : Set A) ⊆ S.starClosure.toNonUnitalSubalgebra :=
+  star_le_starClosure_toNonUnitalSubalgebra _
+
+@[aesop unsafe 50% apply (rule_sets := [SetLike])]
+theorem mem_starClosure_of_mem {S : NonUnitalSubalgebra R A} {x : A} (hx : x ∈ S) :
+    x ∈ S.starClosure := le_starClosure_toNonUnitalSubalgebra _ hx
+
+@[aesop unsafe 49% apply (rule_sets := [SetLike])]
+theorem mem_starClosure_of_star_mem {S : NonUnitalSubalgebra R A} {x : A} (hx : star x ∈ S) :
+    x ∈ S.starClosure := star_le_starClosure_toNonUnitalSubalgebra _ hx
+
 theorem starClosure_le {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A}
     (h : S₁ ≤ S₂.toNonUnitalSubalgebra) : S₁.starClosure ≤ S₂ :=
   NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff.1 <|
@@ -585,10 +611,8 @@ theorem starClosure_le_iff {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalSta
     S₁.starClosure ≤ S₂ ↔ S₁ ≤ S₂.toNonUnitalSubalgebra :=
   ⟨fun h => le_sup_left.trans h, starClosure_le⟩
 
-@[simp]
-theorem starClosure_toNonunitalSubalgebra {S : NonUnitalSubalgebra R A} :
-    S.starClosure.toNonUnitalSubalgebra = S ⊔ star S :=
-  rfl
+@[deprecated (since := "05-01-2025")] alias
+  starClosure_toNonunitalSubalgebra := starClosure_toNonUnitalSubalgebra
 
 @[mono]
 theorem starClosure_mono : Monotone (starClosure (R := R) (A := A)) :=
@@ -614,6 +638,7 @@ open NonUnitalStarSubalgebra
 variable (R)
 
 /-- The minimal non-unital subalgebra that includes `s`. -/
+@[simps! toNonUnitalSubalgebra]
 def adjoin (s : Set A) : NonUnitalStarSubalgebra R A where
   toNonUnitalSubalgebra := NonUnitalAlgebra.adjoin R (s ∪ star s)
   star_mem' _ := by
@@ -628,17 +653,21 @@ theorem adjoin_eq_starClosure_adjoin (s : Set A) :
     from
       (NonUnitalSubalgebra.star_adjoin_comm R s).symm ▸ NonUnitalAlgebra.adjoin_union s (star s)
 
-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.trans <| NonUnitalAlgebra.subset_adjoin R
 
+@[aesop safe 20 apply (rule_sets := [SetLike])]
 theorem star_subset_adjoin (s : Set A) : star s ⊆ adjoin R s :=
   Set.subset_union_right.trans <| NonUnitalAlgebra.subset_adjoin R
 
+@[aesop unsafe 50% apply (rule_sets := [SetLike])]
+theorem mem_adjoin_of_mem {s : Set A} {x : A} (hx : x ∈ s) : x ∈ adjoin R s := subset_adjoin R s hx
+
+@[aesop unsafe 49% apply (rule_sets := [SetLike])]
+theorem mem_adjoin_of_star_mem {s : Set A} {x : A} (hx : star x ∈ s) : x ∈ adjoin R s :=
+  star_subset_adjoin R s hx
+
 theorem self_mem_adjoin_singleton (x : A) : x ∈ adjoin R ({x} : Set A) :=
   NonUnitalAlgebra.subset_adjoin R <| Set.mem_union_left _ (Set.mem_singleton x)
 

Mathlib/Algebra/Star/Subalgebra.lean

@@ -341,16 +341,36 @@ variable {R}
 
 /-- The `StarSubalgebra` obtained from `S : Subalgebra R A` by taking the smallest subalgebra
 containing both `S` and `star S`. -/
-@[simps!]
+@[simps toSubalgebra]
 def starClosure (S : Subalgebra R A) : StarSubalgebra R A where
   toSubalgebra := S ⊔ star S
   star_mem' := fun {a} ha => by
     simp only [Subalgebra.mem_carrier, ← (@Algebra.gi R A _ _ _).l_sup_u _ _] at *
     rw [← mem_star_iff _ a, star_adjoin_comm, sup_comm]
     simpa using ha
 
-theorem starClosure_toSubalgebra (S : Subalgebra R A) : S.starClosure.toSubalgebra = S ⊔ star S :=
-  rfl
+theorem le_starClosure_toSubalgebra (S : Subalgebra R A) : S ≤ S.starClosure.toSubalgebra := by
+  rw [starClosure_toSubalgebra]; simp
+
+theorem star_le_starClosure_toSubalgebra (S : Subalgebra R A) :
+    star S ≤ S.starClosure.toSubalgebra := by
+  rw [starClosure_toSubalgebra]; simp
+
+@[aesop safe 20 apply (rule_sets := [SetLike])]
+theorem subset_starClosure (S : Subalgebra R A) : (S : Set A) ⊆ S.starClosure.toSubalgebra :=
+  le_starClosure_toSubalgebra _
+
+@[aesop safe 20 apply (rule_sets := [SetLike])]
+theorem star_subset_starClosure (S : Subalgebra R A) :
+    (star S : Set A) ⊆ S.starClosure.toSubalgebra := star_le_starClosure_toSubalgebra _
+
+@[aesop unsafe 50% apply (rule_sets := [SetLike])]
+theorem mem_starClosure_of_mem {S : Subalgebra R A} {x : A} (hx : x ∈ S) : x ∈ S.starClosure :=
+  le_starClosure_toSubalgebra _ hx
+
+@[aesop unsafe 49% apply (rule_sets := [SetLike])]
+theorem mem_starClosure_of_star_mem {S : Subalgebra R A} {x : A} (hx : star x ∈ S) :
+    x ∈ S.starClosure := star_le_starClosure_toSubalgebra _ hx
 
 theorem starClosure_le {S₁ : Subalgebra R A} {S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂.toSubalgebra) :
     S₁.starClosure ≤ S₂ :=
@@ -374,10 +394,11 @@ open StarSubalgebra
 variable {F R A B : Type*} [CommSemiring R] [StarRing R]
 variable [Semiring A] [Algebra R A] [StarRing A] [StarModule R A]
 variable [Semiring B] [Algebra R B] [StarRing B] [StarModule R B]
+
 variable (R)
 
 /-- The minimal star subalgebra that contains `s`. -/
-@[simps!]
+@[simps! toSubalgebra]
 def adjoin (s : Set A) : StarSubalgebra R A :=
   { Algebra.adjoin R (s ∪ star s) with
     star_mem' := fun hx => by
@@ -389,17 +410,21 @@ theorem adjoin_eq_starClosure_adjoin (s : Set A) : adjoin R s = (Algebra.adjoin
     show Algebra.adjoin R (s ∪ star s) = Algebra.adjoin R s ⊔ star (Algebra.adjoin R s) from
       (Subalgebra.star_adjoin_comm R s).symm ▸ Algebra.adjoin_union s (star s)
 
-theorem adjoin_toSubalgebra (s : Set A) :
-    (adjoin R s).toSubalgebra = Algebra.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.trans Algebra.subset_adjoin
 
+@[aesop safe 20 apply (rule_sets := [SetLike])]
 theorem star_subset_adjoin (s : Set A) : star s ⊆ adjoin R s :=
   Set.subset_union_right.trans Algebra.subset_adjoin
 
+@[aesop unsafe 50% apply (rule_sets := [SetLike])]
+theorem mem_adjoin_of_mem {s : Set A} {x : A} (hx : x ∈ s) : x ∈ adjoin R s := subset_adjoin R s hx
+
+@[aesop unsafe 49% apply (rule_sets := [SetLike])]
+theorem mem_adjoin_of_star_mem {s : Set A} {x : A} (hx : star x ∈ s) : x ∈ adjoin R s :=
+  star_subset_adjoin R s hx
+
 theorem self_mem_adjoin_singleton (x : A) : x ∈ adjoin R ({x} : Set A) :=
   Algebra.subset_adjoin <| Set.mem_union_left _ (Set.mem_singleton x)