diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean
index 7646e4832fa79..2604cce938ccb 100644
--- a/src/field_theory/subfield.lean
+++ b/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
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 3670a75c70028..121f87aaa41e1 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/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`. -/
diff --git a/src/group_theory/submonoid/basic.lean b/src/group_theory/submonoid/basic.lean
index a4bf838fff9e7..e9e5469fdf70a 100644
--- a/src/group_theory/submonoid/basic.lean
+++ b/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
 
diff --git a/src/model_theory/basic.lean b/src/model_theory/basic.lean
index 4b1d0765fc66f..bb077d1533e9d 100644
--- a/src/model_theory/basic.lean
+++ b/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)))
diff --git a/src/order/closure.lean b/src/order/closure.lean
index 7feb1e9200377..f32b6490beb08 100644
--- a/src/order/closure.lean
+++ b/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
 
diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean
index 83d2bae1345a0..d8662c2a285eb 100644
--- a/src/ring_theory/subring.lean
+++ b/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 :=
diff --git a/src/ring_theory/subsemiring.lean b/src/ring_theory/subsemiring.lean
index f1eb39177a76b..cc60269f9da9a 100644
--- a/src/ring_theory/subsemiring.lean
+++ b/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 :=
diff --git a/src/topology/basic.lean b/src/topology/basic.lean
index 11b22bd38d97a..3e07510827b93 100644
--- a/src/topology/basic.lean
+++ b/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₁⟩