feat(*): add not_mem_of_not_mem_closure for anything with subset_clos…

…ure (#9595)

This is a goal I would expect library search to finish if I have something not in a closure and I want it not in the base set.

src/field_theory/subfield.lean

@@ -429,6 +429,9 @@ lemma subring_closure_le (s : set K) : subring.closure s ≤ (closure s).to_subr
 @[simp] lemma subset_closure {s : set K} : s ⊆ closure s :=
 set.subset.trans subring.subset_closure (subring_closure_le s)
 
+lemma not_mem_of_not_mem_closure {s : set K} {P : K} (hP : P ∉ closure s) : P ∉ s :=
+λ h, hP (subset_closure h)
+
 lemma mem_closure {x : K} {s : set K} : x ∈ closure s ↔ ∀ S : subfield K, s ⊆ S → x ∈ S :=
 ⟨λ ⟨y, hy, z, hz, x_eq⟩ t le, x_eq ▸
   t.div_mem

src/group_theory/subgroup/basic.lean

@@ -578,6 +578,9 @@ mem_Inf
 @[simp, to_additive "The `add_subgroup` generated by a set includes the set."]
 lemma subset_closure : k ⊆ closure k := λ x hx, mem_closure.2 $ λ K hK, hK hx
 
+@[to_additive]
+lemma not_mem_of_not_mem_closure {P : G} (hP : P ∉ closure k) : P ∉ k := λ h, hP (subset_closure h)
+
 open set
 
 /-- A subgroup `K` includes `closure k` if and only if it includes `k`. -/

src/group_theory/submonoid/basic.lean

@@ -247,6 +247,9 @@ mem_Inf
 @[simp, to_additive "The `add_submonoid` generated by a set includes the set."]
 lemma subset_closure : s ⊆ closure s := λ x hx, mem_closure.2 $ λ S hS, hS hx
 
+@[to_additive]
+lemma not_mem_of_not_mem_closure {P : M} (hP : P ∉ closure s) : P ∉ s := λ h, hP (subset_closure h)
+
 variable {S}
 open set
 

src/model_theory/basic.lean

@@ -500,6 +500,9 @@ mem_Inf
 @[simp]
 lemma subset_closure : s ⊆ closure L s := (closure L).le_closure s
 
+lemma not_mem_of_not_mem_closure {P : M} (hP : P ∉ closure L s) : P ∉ s :=
+λ h, hP (subset_closure h)
+
 @[simp]
 lemma closed (S : L.substructure M) : (closure L).closed (S : set M) :=
 congr rfl ((closure L).eq_of_le set.subset.rfl (λ x xS, mem_closure.2 (λ T hT, hT xS)))

src/order/closure.lean

@@ -380,6 +380,9 @@ variables [set_like α β] (l : lower_adjoint (coe : α → set β))
 lemma subset_closure (s : set β) : s ⊆ l s :=
 l.le_closure s
 
+lemma not_mem_of_not_mem_closure {s : set β} {P : β} (hP : P ∉ l s) : P ∉ s :=
+λ h, hP (subset_closure _ s h)
+
 lemma le_iff_subset (s : set β) (S : α) : l s ≤ S ↔ s ⊆ S :=
 l.gc s S
 

src/ring_theory/subring.lean

@@ -556,6 +556,9 @@ mem_Inf
 /-- The subring generated by a set includes the set. -/
 @[simp] lemma subset_closure {s : set R} : s ⊆ closure s := λ x hx, mem_closure.2 $ λ S hS, hS hx
 
+lemma not_mem_of_not_mem_closure {s : set R} {P : R} (hP : P ∉ closure s) : P ∉ s :=
+λ h, hP (subset_closure h)
+
 /-- A subring `t` includes `closure s` if and only if it includes `s`. -/
 @[simp]
 lemma closure_le {s : set R} {t : subring R} : closure s ≤ t ↔ s ⊆ t :=

src/ring_theory/subsemiring.lean

@@ -414,6 +414,9 @@ mem_Inf
 /-- The subsemiring generated by a set includes the set. -/
 @[simp] lemma subset_closure {s : set R} : s ⊆ closure s := λ x hx, mem_closure.2 $ λ S hS, hS hx
 
+lemma not_mem_of_not_mem_closure {s : set R} {P : R} (hP : P ∉ closure s) : P ∉ s :=
+λ h, hP (subset_closure h)
+
 /-- A subsemiring `S` includes `closure s` if and only if it includes `s`. -/
 @[simp]
 lemma closure_le {s : set R} {t : subsemiring R} : closure s ≤ t ↔ s ⊆ t :=

src/topology/basic.lean

@@ -316,6 +316,9 @@ is_closed_sInter $ assume t ⟨h₁, h₂⟩, h₁
 lemma subset_closure {s : set α} : s ⊆ closure s :=
 subset_sInter $ assume t ⟨h₁, h₂⟩, h₂
 
+lemma not_mem_of_not_mem_closure {s : set α} {P : α} (hP : P ∉ closure s) : P ∉ s :=
+λ h, hP (subset_closure h)
+
 lemma closure_minimal {s t : set α} (h₁ : s ⊆ t) (h₂ : is_closed t) : closure s ⊆ t :=
 sInter_subset_of_mem ⟨h₂, h₁⟩