feat: add closure_insert_one etc (#23159)

Author: urkud

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -525,17 +525,49 @@ theorem adjoin_union (s t : Set A) : adjoin R (s ∪ t) = adjoin R s ⊔ adjoin
 variable (R A)
 
 @[simp]
-theorem adjoin_empty : adjoin R (∅ : Set A) = ⊥ :=
-  show adjoin R ⊥ = ⊥ by
-    apply GaloisConnection.l_bot
-    exact Algebra.gc
+theorem adjoin_empty : adjoin R (∅ : Set A) = ⊥ := Algebra.gc.l_bot
 
 @[simp]
-theorem adjoin_univ : adjoin R (Set.univ : Set A) = ⊤ :=
-  eq_top_iff.2 fun _x => subset_adjoin <| Set.mem_univ _
+theorem adjoin_univ : adjoin R (Set.univ : Set A) = ⊤ := Algebra.gi.l_top
+
+variable {R} in
+@[simp]
+theorem adjoin_singleton_algebraMap (x : R) : adjoin R {algebraMap R A x} = ⊥ :=
+  bot_unique <| adjoin_le <| Set.singleton_subset_iff.mpr <| Subalgebra.algebraMap_mem _ _
+
+@[simp]
+theorem adjoin_singleton_natCast (n : ℕ) : adjoin R {(n : A)} = ⊥ := by
+  simpa using adjoin_singleton_algebraMap A (n : R)
+
+@[simp]
+theorem adjoin_singleton_zero : adjoin R ({0} : Set A) = ⊥ :=
+  mod_cast adjoin_singleton_natCast R A 0
+
+@[simp]
+theorem adjoin_singleton_one : adjoin R ({1} : Set A) = ⊥ :=
+  mod_cast adjoin_singleton_natCast R A 1
 
 variable {A} (s)
 
+variable {R} in
+@[simp]
+theorem adjoin_insert_algebraMap (x : R) (s : Set A) :
+    adjoin R (insert (algebraMap R A x) s) = adjoin R s := by
+  rw [Set.insert_eq, adjoin_union]
+  simp
+
+@[simp]
+theorem adjoin_insert_natCast (n : ℕ) (s : Set A) : adjoin R (insert (n : A) s) = adjoin R s :=
+  mod_cast adjoin_insert_algebraMap (n : R) s
+
+@[simp]
+theorem adjoin_insert_zero (s : Set A) : adjoin R (insert 0 s) = adjoin R s :=
+  mod_cast adjoin_insert_natCast R 0 s
+
+@[simp]
+theorem adjoin_insert_one (s : Set A) : adjoin R (insert 1 s) = adjoin R s :=
+  mod_cast adjoin_insert_natCast R 1 s
+
 theorem adjoin_eq_span : Subalgebra.toSubmodule (adjoin R s) = span R (Submonoid.closure s) := by
   apply le_antisymm
   · intro r hr
@@ -645,9 +677,6 @@ lemma commute_of_mem_adjoin_self {a b : A} (hb : b ∈ adjoin R {a}) :
 
 variable (R)
 
-theorem adjoin_singleton_one : adjoin R ({1} : Set A) = ⊥ :=
-  eq_bot_iff.2 <| adjoin_le <| Set.singleton_subset_iff.2 <| SetLike.mem_coe.2 <| one_mem _
-
 theorem self_mem_adjoin_singleton (x : A) : x ∈ adjoin R ({x} : Set A) :=
   Algebra.subset_adjoin (Set.mem_singleton_iff.mpr rfl)
 
@@ -672,6 +701,14 @@ section Ring
 variable [CommRing R] [Ring A]
 variable [Algebra R A] {s t : Set A}
 
+@[simp]
+theorem adjoin_singleton_intCast (n : ℤ) : adjoin R {(n : A)} = ⊥ := by
+  simpa using adjoin_singleton_algebraMap A (n : R)
+
+@[simp]
+theorem adjoin_insert_intCast (n : ℤ) (s : Set A) : adjoin R (insert (n : A) s) = adjoin R s := by
+  simpa using adjoin_insert_algebraMap (n : R) s
+
 theorem mem_adjoin_iff {s : Set A} {x : A} :
     x ∈ adjoin R s ↔ x ∈ Subring.closure (Set.range (algebraMap R A) ∪ s) :=
   ⟨fun hx =>

Mathlib/Algebra/Group/Subgroup/Lattice.lean

@@ -470,6 +470,11 @@ theorem closure_eq_top_of_mclosure_eq_top {S : Set G} (h : Submonoid.closure S =
     closure S = ⊤ :=
   (eq_top_iff' _).2 fun _ => le_closure_toSubmonoid _ <| h.symm ▸ trivial
 
+@[to_additive (attr := simp)]
+theorem closure_insert_one (s : Set G) : closure (insert 1 s) = closure s := by
+  rw [insert_eq, closure_union]
+  simp [one_mem]
+
 theorem toAddSubgroup_closure (S : Set G) :
     (Subgroup.closure S).toAddSubgroup = AddSubgroup.closure (Additive.toMul ⁻¹' S) :=
   le_antisymm (toAddSubgroup.le_symm_apply.mp <|

Mathlib/Algebra/Group/Submonoid/Basic.lean

@@ -268,6 +268,11 @@ theorem closure_iUnion {ι} (s : ι → Set M) : closure (⋃ i, s i) = ⨆ i, c
 theorem closure_singleton_le_iff_mem (m : M) (p : Submonoid M) : closure {m} ≤ p ↔ m ∈ p := by
   rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
 
+@[to_additive (attr := simp)]
+theorem closure_insert_one (s : Set M) : closure (insert 1 s) = closure s := by
+  rw [insert_eq, closure_union, sup_eq_right, closure_singleton_le_iff_mem]
+  apply one_mem
+
 @[to_additive]
 theorem mem_iSup {ι : Sort*} (p : ι → Submonoid M) {m : M} :
     (m ∈ ⨆ i, p i) ↔ ∀ N, (∀ i, p i ≤ N) → m ∈ N := by

Mathlib/Algebra/Ring/Subring/Basic.lean

@@ -634,6 +634,37 @@ theorem closure_iUnion {ι} (s : ι → Set R) : closure (⋃ i, s i) = ⨆ i, c
 theorem closure_sUnion (s : Set (Set R)) : closure (⋃₀ s) = ⨆ t ∈ s, closure t :=
   (Subring.gi R).gc.l_sSup
 
+@[simp]
+theorem closure_singleton_intCast (n : ℤ) : closure {(n : R)} = ⊥ :=
+  bot_unique <| closure_le.2 <| Set.singleton_subset_iff.mpr <| intCast_mem _ _
+
+@[simp]
+theorem closure_singleton_natCast (n : ℕ) : closure {(n : R)} = ⊥ :=
+  mod_cast closure_singleton_intCast n
+
+@[simp]
+theorem closure_singleton_zero : closure {(0 : R)} = ⊥ := mod_cast closure_singleton_natCast 0
+
+@[simp]
+theorem closure_singleton_one : closure {(1 : R)} = ⊥ := mod_cast closure_singleton_natCast 1
+
+@[simp]
+theorem closure_insert_intCast (n : ℤ) (s : Set R) : closure (insert (n : R) s) = closure s := by
+  rw [Set.insert_eq, closure_union]
+  simp
+
+@[simp]
+theorem closure_insert_natCast (n : ℕ) (s : Set R) : closure (insert (n : R) s) = closure s :=
+  mod_cast closure_insert_intCast n s
+
+@[simp]
+theorem closure_insert_zero (s : Set R) : closure (insert 0 s) = closure s :=
+  mod_cast closure_insert_natCast 0 s
+
+@[simp]
+theorem closure_insert_one (s : Set R) : closure (insert 1 s) = closure s :=
+  mod_cast closure_insert_natCast 1 s
+
 theorem map_sup (s t : Subring R) (f : R →+* S) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
   (gc_map_comap f).l_sup
 

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

@@ -563,6 +563,29 @@ theorem closure_iUnion {ι} (s : ι → Set R) : closure (⋃ i, s i) = ⨆ i, c
 theorem closure_sUnion (s : Set (Set R)) : closure (⋃₀ s) = ⨆ t ∈ s, closure t :=
   (Subsemiring.gi R).gc.l_sSup
 
+@[simp]
+theorem closure_singleton_natCast (n : ℕ) : closure {(n : R)} = ⊥ :=
+  bot_unique <| closure_le.2 <| Set.singleton_subset_iff.mpr <| natCast_mem _ _
+
+@[simp]
+theorem closure_singleton_zero : closure {(0 : R)} = ⊥ := mod_cast closure_singleton_natCast 0
+
+@[simp]
+theorem closure_singleton_one : closure {(1 : R)} = ⊥ := mod_cast closure_singleton_natCast 1
+
+@[simp]
+theorem closure_insert_natCast (n : ℕ) (s : Set R) : closure (insert (n : R) s) = closure s := by
+  rw [Set.insert_eq, closure_union]
+  simp
+
+@[simp]
+theorem closure_insert_zero (s : Set R) : closure (insert 0 s) = closure s :=
+  mod_cast closure_insert_natCast 0 s
+
+@[simp]
+theorem closure_insert_one (s : Set R) : closure (insert 1 s) = closure s :=
+  mod_cast closure_insert_natCast 1 s
+
 theorem map_sup (s t : Subsemiring R) (f : R →+* S) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
   (gc_map_comap f).l_sup