diff --git a/archive/imo1988_q6.lean b/archive/imo1988_q6.lean
index 441822b62f057..3391f8acbf902 100644
--- a/archive/imo1988_q6.lean
+++ b/archive/imo1988_q6.lean
@@ -114,18 +114,17 @@ begin
   -- So we assume that the exceptional locus is empty, and work towards dering a contradiction.
   assume exceptional_empty,
   -- Observe that S is nonempty.
-  have S_ne_empty : S ≠ ∅,
-  { rw set.ne_empty_iff_exists_mem,
-    -- It contains the image of p.
+  have S_nonempty : S.nonempty,
+  { -- It contains the image of p.
     use p.2,
     apply set.mem_image_of_mem,
     -- After all, we assumed that the exceptional locus is empty.
     rwa [exceptional_empty, set.diff_empty], },
   -- We are now set for an infinite descent argument.
   -- Let m be the smallest element of the nonempty set S.
-  let  m     : ℕ                := well_founded.min     nat.lt_wf S S_ne_empty,
-  have m_mem : m ∈ S            := well_founded.min_mem nat.lt_wf S S_ne_empty,
-  have m_min : ∀ k ∈ S, ¬ k < m := λ k hk, well_founded.not_lt_min nat.lt_wf S S_ne_empty hk,
+  let  m     : ℕ                := well_founded.min     nat.lt_wf S S_nonempty,
+  have m_mem : m ∈ S            := well_founded.min_mem nat.lt_wf S S_nonempty,
+  have m_min : ∀ k ∈ S, ¬ k < m := λ k hk, well_founded.not_lt_min nat.lt_wf S S_nonempty hk,
   -- It suffices to show that there is point (a,b) with b ∈ S and b < m.
   suffices hp' : ∃ p' : ℕ × ℕ, p'.2 ∈ S ∧ p'.2 < m,
   { rcases hp' with ⟨p', p'_mem, p'_small⟩, solve_by_elim },
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index c9e8c85656ea9..2c0b8d5ede290 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -6,8 +6,13 @@ Author: Jeremy Avigad, Leonardo de Moura
 import tactic.basic tactic.finish data.subtype logic.unique
 open function
 
+/-! # Basic properties of sets
 
-/- set coercion to a type -/
+This file provides some basic definitions related to sets and functions (e.g., `preimage`)
+not present in the core library, as well as extra lemmas.
+-/
+
+/-! ### Set coercion to a type -/
 namespace set
 instance {α : Type*} : has_coe_to_sort (set α) := ⟨_, λ s, {x // x ∈ s}⟩
 end set
@@ -56,7 +61,7 @@ theorem ext_iff (s t : set α) : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
 @[trans] theorem mem_of_mem_of_subset {α : Type u} {x : α} {s t : set α} (hx : x ∈ s) (h : s ⊆ t) : x ∈ t :=
 h hx
 
-/- mem and set_of -/
+/-! ### Lemmas about `mem` and `set_of` -/
 
 @[simp] theorem mem_set_of_eq {a : α} {p : α → Prop} : a ∈ {a | p a} = p a := rfl
 
@@ -79,7 +84,7 @@ rfl
 
 @[simp] lemma set_of_mem {α} {s : set α} : {a | a ∈ s} = s := rfl
 
-/- subset -/
+/-! #### Lemmas about subsets -/
 
 -- TODO(Jeremy): write a tactic to unfold specific instances of generic notation?
 theorem subset_def {s t : set α} : (s ⊆ t) = ∀ x, x ∈ s → x ∈ t := rfl
@@ -109,7 +114,7 @@ assume h₁ h₂, h₁ h₂
 theorem not_subset : (¬ s ⊆ t) ↔ ∃a, a ∈ s ∧ a ∉ t :=
 by simp [subset_def, classical.not_forall]
 
-/- strict subset -/
+/-! ### Definition of strict subsets `s ⊂ t` and basic properties. -/
 
 /-- `s ⊂ t` means that `s` is a strict subset of `t`, that is, `s ⊆ t` but `s ≠ t`. -/
 def strict_subset (s t : set α) := s ⊆ t ∧ s ≠ t
@@ -132,7 +137,47 @@ assume h : x ∈ ∅, h
 @[simp] theorem not_not_mem [decidable (a ∈ s)] : ¬ (a ∉ s) ↔ a ∈ s :=
 not_not
 
-/- empty set -/
+/-! ### Non-empty sets -/
+
+/-- The property `s.nonempty` expresses the fact that the set `s` is not empty. It should be used
+in theorem assumptions instead of `∃ x, x ∈ s` or `s ≠ ∅` as it gives access to a nice API thanks
+to the dot notation. -/
+protected def nonempty (s : set α) : Prop := ∃ x, x ∈ s
+
+lemma nonempty_of_mem {x} (h : x ∈ s) : s.nonempty := ⟨x, h⟩
+
+/-- Extract a witness from `s.nonempty`. This function might be used instead of case analysis
+on the argument. Note that it makes a proof depend on the `classical.choice` axiom. -/
+protected noncomputable def nonempty.some (h : s.nonempty) : α := classical.some h
+
+protected lemma nonempty.some_mem (h : s.nonempty) : h.some ∈ s := classical.some_spec h
+
+lemma nonempty.of_subset (ht : s ⊆ t) (hs : s.nonempty) : t.nonempty := hs.imp ht
+
+lemma nonempty_of_ssubset (ht : s ⊂ t) : (t \ s).nonempty :=
+let ⟨x, xt, xs⟩ := exists_of_ssubset ht in ⟨x, xt, xs⟩
+
+lemma nonempty.of_diff (h : (s \ t).nonempty) : s.nonempty := h.imp $ λ _, and.left
+
+lemma nonempty.of_ssubset' (ht : s ⊂ t) : t.nonempty := (nonempty_of_ssubset ht).of_diff
+
+lemma nonempty.inl (hs : s.nonempty) : (s ∪ t).nonempty := hs.imp $ λ _, or.inl
+
+lemma nonempty.inr (ht : t.nonempty) : (s ∪ t).nonempty := ht.imp $ λ _, or.inr
+
+@[simp] lemma union_nonempty : (s ∪ t).nonempty ↔ s.nonempty ∨ t.nonempty := exists_or_distrib
+
+lemma nonempty.left (h : (s ∩ t).nonempty) : s.nonempty := h.imp $ λ _, and.left
+
+lemma nonempty.right (h : (s ∩ t).nonempty) : t.nonempty := h.imp $ λ _, and.right
+
+lemma nonempty_iff_univ_nonempty : nonempty α ↔ (univ : set α).nonempty :=
+⟨λ ⟨x⟩, ⟨x, trivial⟩, λ ⟨x, _⟩, ⟨x⟩⟩
+
+lemma univ_nonempty : ∀ [h : nonempty α], (univ : set α).nonempty
+| ⟨x⟩ := ⟨x, trivial⟩
+
+/-! ### Lemmas about the empty set -/
 
 theorem empty_def : (∅ : set α) = {x | false} := rfl
 
@@ -143,9 +188,6 @@ theorem empty_def : (∅ : set α) = {x | false} := rfl
 theorem eq_empty_iff_forall_not_mem {s : set α} : s = ∅ ↔ ∀ x, x ∉ s :=
 by simp [ext_iff]
 
-theorem ne_empty_of_mem {s : set α} {x : α} (h : x ∈ s) : s ≠ ∅ :=
-by { intro hs, rw hs at h, apply not_mem_empty _ h }
-
 @[simp] theorem empty_subset (s : set α) : ∅ ⊆ s :=
 assume x, assume h, false.elim h
 
@@ -155,13 +197,18 @@ by simp [subset.antisymm_iff]
 theorem eq_empty_of_subset_empty {s : set α} : s ⊆ ∅ → s = ∅ :=
 subset_empty_iff.1
 
-theorem ne_empty_iff_exists_mem {s : set α} : s ≠ ∅ ↔ ∃ x, x ∈ s :=
+theorem ne_empty_iff_nonempty : s ≠ ∅ ↔ s.nonempty :=
 by haveI := classical.prop_decidable;
-   simp [eq_empty_iff_forall_not_mem]
+   simp [eq_empty_iff_forall_not_mem, set.nonempty]
+
+theorem ne_empty_iff_exists_mem {s : set α} : s ≠ ∅ ↔ ∃ x, x ∈ s := ne_empty_iff_nonempty
 
 theorem exists_mem_of_ne_empty {s : set α} : s ≠ ∅ → ∃ x, x ∈ s :=
 ne_empty_iff_exists_mem.1
 
+theorem ne_empty_of_mem {s : set α} {x : α} (h : x ∈ s) : s ≠ ∅ :=
+ne_empty_iff_nonempty.2 ⟨x, h⟩
+
 theorem coe_nonempty_iff_ne_empty {s : set α} : nonempty s ↔ s ≠ ∅ :=
 nonempty_subtype.trans ne_empty_iff_exists_mem.symm
 
@@ -179,7 +226,10 @@ theorem ball_empty_iff {p : α → Prop} :
   (∀ x ∈ (∅ : set α), p x) ↔ true :=
 by simp [iff_def]
 
-/- universal set -/
+/-! ### Universal set.
+
+In Lean `@univ α` (or `univ : set α`) is the set that contains all elements of type `α`.
+Mathematically it is the same as `α` but it has a different type. -/
 
 theorem univ_def : @univ α = {x | true} := rfl
 
@@ -216,7 +266,7 @@ lemma exists_mem_of_nonempty (α) : ∀ [nonempty α], ∃x:α, x ∈ (univ : se
 instance univ_decidable : decidable_pred (@set.univ α) :=
 λ x, is_true trivial
 
-/- union -/
+/-! ### Lemmas about union -/
 
 theorem union_def {s₁ s₂ : set α} : s₁ ∪ s₂ = {a | a ∈ s₁ ∨ a ∈ s₂} := rfl
 
@@ -295,7 +345,7 @@ subset.trans h (subset_union_right t u)
 @[simp] theorem union_empty_iff {s t : set α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅ :=
 ⟨by finish [ext_iff], by finish [ext_iff]⟩
 
-/- intersection -/
+/-! ### Lemmas about intersection -/
 
 theorem inter_def {s₁ s₂ : set α} : s₁ ∩ s₂ = {a | a ∈ s₁ ∧ a ∈ s₂} := rfl
 
@@ -384,7 +434,7 @@ by finish [ext_iff, iff_def]
 theorem nonempty_of_inter_nonempty_left {s t : set α} (h : s ∩ t ≠ ∅) : s ≠ ∅ :=
 by finish [ext_iff, iff_def]
 
-/- distributivity laws -/
+/-! ### Distributivity laws -/
 
 theorem inter_distrib_left (s t u : set α) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) :=
 ext (assume x, and_or_distrib_left)
@@ -398,7 +448,9 @@ ext (assume x, or_and_distrib_left)
 theorem union_distrib_right (s t u : set α) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) :=
 ext (assume x, and_or_distrib_right)
 
-/- insert -/
+/-! ### Lemmas about `insert`
+
+`insert α s` is the set `{α} ∪ s`. -/
 
 theorem insert_def (x : α) (s : set α) : insert x s = { y | y = x ∨ y ∈ s } := rfl
 
@@ -457,7 +509,7 @@ theorem ball_insert_iff {P : α → Prop} {a : α} {s : set α} :
   (∀ x ∈ insert a s, P x) ↔ P a ∧ (∀x ∈ s, P x) :=
 by finish [iff_def]
 
-/- singletons -/
+/-! ### Lemmas about singletons -/
 
 theorem singleton_def (a : α) : ({a} : set α) = insert a ∅ := rfl
 
@@ -517,7 +569,7 @@ instance unique_singleton {α : Type*} (a : α) : unique ↥({a} : set α) :=
     apply eq_of_mem_singleton (subtype.mem x),
   end}
 
-/- separation -/
+/-! ### Lemmas about sets defined as `{x ∈ s | p x}`. -/
 
 theorem mem_sep {s : set α} {p : α → Prop} {x : α} (xs : x ∈ s) (px : p x) : x ∈ {x ∈ s | p x} :=
 ⟨xs, px⟩
@@ -540,7 +592,7 @@ by finish [ext_iff]
 @[simp] lemma sep_univ {α} {p : α → Prop} : {a ∈ (univ : set α) | p a} = {a | p a} :=
 set.ext $ by simp
 
-/- complement -/
+/-! ### Lemmas about complement -/
 
 theorem mem_compl {s : set α} {x : α} (h : x ∉ s) : x ∈ -s := h
 
@@ -625,7 +677,7 @@ begin
   intros h x, rintro ⟨xa, xb⟩, cases h xa, contradiction, assumption
 end
 
-/- set difference -/
+/-! ### Lemmas about set difference -/
 
 theorem diff_eq (s t : set α) : s \ t = s ∩ -t := rfl
 
@@ -1053,6 +1105,7 @@ Hh.symm ▸ set.ext (λ ⟨a₁, a₂⟩, ⟨quotient.induction_on₂ a₁ a₂
   have h₃ : ⟦b₁⟧ = a₁ ∧ ⟦b₂⟧ = a₂ := prod.ext_iff.1 h₂,
     h₃.1 ▸ h₃.2 ▸ h₁⟩)
 
+/-- Restriction of `f` to `s` factors through `s.image_factorization f : s → f '' s`. -/
 def image_factorization (f : α → β) (s : set α) : s → f '' s :=
 λ p, ⟨f p.1, mem_image_of_mem f p.2⟩
 
@@ -1069,6 +1122,7 @@ end image
 theorem univ_eq_true_false : univ = ({true, false} : set Prop) :=
 eq.symm $ eq_univ_of_forall $ classical.cases (by simp) (by simp)
 
+/-! ### Lemmas about range of a function. -/
 section range
 variables {f : ι → α}
 open function
@@ -1165,6 +1219,7 @@ range_subset_iff.2 $ λ x, or.inl rfl
 | ⟨x⟩ c := subset.antisymm range_const_subset $
   assume y hy, (mem_singleton_iff.1 hy).symm ▸ mem_range_self x
 
+/-- Any map `f : ι → β` factors through a map `range_factorization f : ι → range f`. -/
 def range_factorization (f : ι → β) : ι → range f :=
 λ i, ⟨f i, mem_range_self i⟩
 
@@ -1213,7 +1268,7 @@ theorem pairwise_on.mono' {s : set α} {r r' : α → α → Prop}
 end set
 open set
 
-/- image and preimage on subtypes -/
+/-! ### Image and preimage on subtypes -/
 
 namespace subtype
 
@@ -1280,6 +1335,8 @@ subtype.val_range
 
 end range
 
+/-! ### Lemmas about cartesian product of sets -/
+
 section prod
 
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
@@ -1303,10 +1360,10 @@ lemma prod_subset_iff {P : set (α × β)} :
 ⟨λ h _ xin _ yin, h (mk_mem_prod xin yin),
  λ h _ pin, by { cases mem_prod.1 pin with hs ht, simpa using h _ hs _ ht }⟩
 
-@[simp] theorem prod_empty {s : set α} : set.prod s ∅ = (∅ : set (α × β)) :=
+@[simp] theorem prod_empty : set.prod s ∅ = (∅ : set (α × β)) :=
 ext $ by simp [set.prod]
 
-@[simp] theorem empty_prod {t : set β} : set.prod ∅ t = (∅ : set (α × β)) :=
+@[simp] theorem empty_prod : set.prod ∅ t = (∅ : set (α × β)) :=
 ext $ by simp [set.prod]
 
 theorem insert_prod {a : α} {s : set α} {t : set β} :
@@ -1359,14 +1416,25 @@ ext $ by simp [range]
   set.prod {a} {b} = ({(a, b)} : set (α×β)) :=
 ext $ by simp [set.prod]
 
-theorem prod_neq_empty_iff {s : set α} {t : set β} :
-  set.prod s t ≠ ∅ ↔ (s ≠ ∅ ∧ t ≠ ∅) :=
-by simp [not_eq_empty_iff_exists]
+theorem nonempty.prod : s.nonempty → t.nonempty → (s.prod t).nonempty
+| ⟨x, hx⟩ ⟨y, hy⟩ := ⟨(x, y), ⟨hx, hy⟩⟩
+
+theorem nonempty.fst : (s.prod t).nonempty → s.nonempty
+| ⟨p, hp⟩ := ⟨p.1, hp.1⟩
+
+theorem nonempty.snd : (s.prod t).nonempty → t.nonempty
+| ⟨p, hp⟩ := ⟨p.2, hp.2⟩
+
+theorem prod_nonempty_iff : (s.prod t).nonempty ↔ s.nonempty ∧ t.nonempty :=
+⟨λ h, ⟨h.fst, h.snd⟩, λ h, nonempty.prod h.1 h.2⟩
+
+theorem prod_ne_empty_iff : s.prod t ≠ ∅ ↔ (s ≠ ∅ ∧ t ≠ ∅) :=
+by simp only [ne_empty_iff_nonempty, prod_nonempty_iff]
 
 theorem prod_eq_empty_iff {s : set α} {t : set β} :
   set.prod s t = ∅ ↔ (s = ∅ ∨ t = ∅) :=
 suffices (¬ set.prod s t ≠ ∅) ↔ (¬ s ≠ ∅ ∨ ¬ t ≠ ∅), by simpa only [(≠), classical.not_not],
-by classical; rw [prod_neq_empty_iff, not_and_distrib]
+by classical; rw [prod_ne_empty_iff, not_and_distrib]
 
 @[simp] theorem prod_mk_mem_set_prod_eq {a : α} {b : β} {s : set α} {t : set β} :
   (a, b) ∈ set.prod s t = (a ∈ s ∧ b ∈ t) := rfl
@@ -1414,10 +1482,10 @@ begin
   classical,
   by_cases h : set.prod s t = ∅,
   { simp [h, prod_eq_empty_iff.1 h] },
-  { have st : s ≠ ∅ ∧ t ≠ ∅, by rwa [← ne.def, prod_neq_empty_iff] at h,
+  { have st : s ≠ ∅ ∧ t ≠ ∅, by rwa [← ne.def, prod_ne_empty_iff] at h,
     split,
     { assume H : set.prod s t ⊆ set.prod s₁ t₁,
-      have h' : s₁ ≠ ∅ ∧ t₁ ≠ ∅ := prod_neq_empty_iff.1 (subset_ne_empty H h),
+      have h' : s₁ ≠ ∅ ∧ t₁ ≠ ∅ := prod_ne_empty_iff.1 (subset_ne_empty H h),
       refine or.inl ⟨_, _⟩,
       show s ⊆ s₁,
       { have := image_subset (prod.fst : α × β → α) H,
diff --git a/src/field_theory/minimal_polynomial.lean b/src/field_theory/minimal_polynomial.lean
index ce5e12902cb35..3b17fc59d1b57 100644
--- a/src/field_theory/minimal_polynomial.lean
+++ b/src/field_theory/minimal_polynomial.lean
@@ -31,7 +31,7 @@ variables [comm_ring α] [comm_ring β] [algebra α β]
 /-- Let B be an A-algebra, and x an element of B that is integral over A.
 The minimal polynomial of x is a monic polynomial of smallest degree that has x as its root. -/
 noncomputable def minimal_polynomial {x : β} (hx : is_integral α x) : polynomial α :=
-well_founded.min polynomial.degree_lt_wf _ (ne_empty_iff_exists_mem.mpr hx)
+well_founded.min polynomial.degree_lt_wf _ hx
 
 end min_poly_def
 
@@ -43,17 +43,17 @@ variables {x : β} (hx : is_integral α x)
 
 /--A minimal polynomial is monic.-/
 lemma monic : monic (minimal_polynomial hx) :=
-(well_founded.min_mem degree_lt_wf _ (ne_empty_iff_exists_mem.mpr hx)).1
+(well_founded.min_mem degree_lt_wf _ hx).1
 
 /--An element is a root of its minimal polynomial.-/
 @[simp] lemma aeval : aeval α β x (minimal_polynomial hx) = 0 :=
-(well_founded.min_mem degree_lt_wf _ (ne_empty_iff_exists_mem.mpr hx)).2
+(well_founded.min_mem degree_lt_wf _ hx).2
 
 /--The defining property of the minimal polynomial of an element x:
 it is the monic polynomial with smallest degree that has x as its root.-/
 lemma min {p : polynomial α} (pmonic : p.monic) (hp : polynomial.aeval α β x p = 0) :
   degree (minimal_polynomial hx) ≤ degree p :=
-le_of_not_lt $ well_founded.not_lt_min degree_lt_wf _ (ne_empty_iff_exists_mem.mpr hx) ⟨pmonic, hp⟩
+le_of_not_lt $ well_founded.not_lt_min degree_lt_wf _ hx ⟨pmonic, hp⟩
 
 end ring
 
diff --git a/src/logic/basic.lean b/src/logic/basic.lean
index 508139866bf32..d4d33ef74af04 100644
--- a/src/logic/basic.lean
+++ b/src/logic/basic.lean
@@ -581,6 +581,8 @@ or_iff_not_imp_right
 
 protected lemma not_not {p : Prop} : ¬¬p ↔ p := not_not
 
+protected theorem not_imp_not {p q : Prop} : (¬ p → ¬ q) ↔ (q → p) := not_imp_not
+
 protected lemma not_and_distrib {p q : Prop}: ¬(p ∧ q) ↔ ¬p ∨ ¬q := not_and_distrib
 
 protected lemma imp_iff_not_or {a b : Prop} : a → b ↔ ¬a ∨ b := imp_iff_not_or
diff --git a/src/order/basic.lean b/src/order/basic.lean
index 707c1fe4e26d7..1cb670618f01b 100644
--- a/src/order/basic.lean
+++ b/src/order/basic.lean
@@ -484,39 +484,39 @@ end
 by { classical, rw [not_iff_comm, not_bounded_iff] }
 
 namespace well_founded
+/-- If `r` is a well founded relation, then any nonempty set has a minimum element
+with respect to `r`. -/
 theorem has_min {α} {r : α → α → Prop} (H : well_founded r)
-  (p : set α) : p ≠ ∅ → ∃ a ∈ p, ∀ x ∈ p, ¬ r x a :=
-by classical; exact
-not_imp_comm.1 (λ he, set.eq_empty_iff_forall_not_mem.2 $ λ a,
-acc.rec_on (H.apply a) $ λ a H IH h,
-he ⟨_, h, λ y, imp_not_comm.1 (IH y)⟩)
+  (s : set α) : s.nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬ r x a
+| ⟨a, ha⟩ := (acc.rec_on (H.apply a) $ λ x _ IH, classical.not_imp_not.1 $ λ hne hx, hne $
+  ⟨x, hx, λ y hy hyx, hne $ IH y hyx hy⟩) ha
 
 /-- The minimum element of a nonempty set in a well-founded order -/
 noncomputable def min {α} {r : α → α → Prop} (H : well_founded r)
-  (p : set α) (h : p ≠ ∅) : α :=
+  (p : set α) (h : p.nonempty) : α :=
 classical.some (H.has_min p h)
 
 theorem min_mem {α} {r : α → α → Prop} (H : well_founded r)
-  (p : set α) (h : p ≠ ∅) : H.min p h ∈ p :=
+  (p : set α) (h : p.nonempty) : H.min p h ∈ p :=
 let ⟨h, _⟩ := classical.some_spec (H.has_min p h) in h
 
 theorem not_lt_min {α} {r : α → α → Prop} (H : well_founded r)
-  (p : set α) (h : p ≠ ∅) {x} (xp : x ∈ p) : ¬ r x (H.min p h) :=
+  (p : set α) (h : p.nonempty) {x} (xp : x ∈ p) : ¬ r x (H.min p h) :=
 let ⟨_, h'⟩ := classical.some_spec (H.has_min p h) in h' _ xp
 
 open set
 protected noncomputable def sup {α} {r : α → α → Prop} (wf : well_founded r) (s : set α)
   (h : bounded r s) : α :=
-wf.min { x | ∀a ∈ s, r a x } (ne_empty_iff_exists_mem.mpr h)
+wf.min { x | ∀a ∈ s, r a x } h
 
 protected lemma lt_sup {α} {r : α → α → Prop} (wf : well_founded r) {s : set α} (h : bounded r s)
   {x} (hx : x ∈ s) : r x (wf.sup s h) :=
-min_mem wf { x | ∀a ∈ s, r a x } (ne_empty_iff_exists_mem.mpr h) x hx
+min_mem wf { x | ∀a ∈ s, r a x } h x hx
 
 section
 open_locale classical
 protected noncomputable def succ {α} {r : α → α → Prop} (wf : well_founded r) (x : α) : α :=
-if h : ∃y, r x y then wf.min { y | r x y } (ne_empty_iff_exists_mem.mpr h) else x
+if h : ∃y, r x y then wf.min { y | r x y } h else x
 
 protected lemma lt_succ {α} {r : α → α → Prop} (wf : well_founded r) {x : α} (h : ∃y, r x y) :
   r x (wf.succ x) :=
@@ -529,7 +529,7 @@ begin
   split,
   { intro h', have : ¬r x y,
     { intro hy, rw [well_founded.succ, dif_pos] at h',
-      exact wo.wf.not_lt_min _ (ne_empty_iff_exists_mem.mpr h) hy h' },
+      exact wo.wf.not_lt_min _ h hy h' },
     rcases trichotomous_of r x y with hy | hy | hy,
     exfalso, exact this hy,
     right, exact hy.symm,
diff --git a/src/order/pilex.lean b/src/order/pilex.lean
index a99e2f2dc0524..90244be72264c 100644
--- a/src/order/pilex.lean
+++ b/src/order/pilex.lean
@@ -67,8 +67,7 @@ instance [linear_order ι] (wf : well_founded ((<) : ι → ι → Prop)) [∀ a
 { le_total := λ x y, by classical; exact
     or_iff_not_imp_left.2 (λ hxy, begin
       have := not_or_distrib.1 hxy,
-      let i : ι := well_founded.min wf _
-        (set.ne_empty_iff_exists_mem.2 (classical.not_forall.1 (this.2 ∘ funext))),
+      let i : ι := well_founded.min wf _ (classical.not_forall.1 (this.2 ∘ funext)),
       have hjiyx : ∀ j < i, y j = x j,
       { assume j,
         rw [eq_comm, ← not_imp_not],
diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean
index ff6dee20a3119..cda2988b05215 100644
--- a/src/ring_theory/integral_closure.lean
+++ b/src/ring_theory/integral_closure.lean
@@ -90,7 +90,7 @@ begin
   let leval : @linear_map R (polynomial R) A _ _ _ _ _ := (aeval R A x).to_linear_map,
   let D : ℕ → submodule R A := λ n, (degree_le R n).map leval,
   let M := well_founded.min (is_noetherian_iff_well_founded.1 H)
-    (set.range D) (set.ne_empty_of_mem ⟨0, rfl⟩),
+    (set.range D) ⟨_, ⟨0, rfl⟩⟩,
   have HM : M ∈ set.range D := well_founded.min_mem _ _ _,
   cases HM with N HN,
   have HM : ¬M < D (N+1) := well_founded.not_lt_min
diff --git a/src/ring_theory/polynomial.lean b/src/ring_theory/polynomial.lean
index 4fc2f5e426970..b486c6ed84ccb 100644
--- a/src/ring_theory/polynomial.lean
+++ b/src/ring_theory/polynomial.lean
@@ -230,7 +230,7 @@ theorem is_noetherian_ring_polynomial [is_noetherian_ring R] : is_noetherian_rin
 ⟨assume I : ideal (polynomial R),
 let L := I.leading_coeff in
 let M := well_founded.min (is_noetherian_iff_well_founded.1 (by apply_instance))
-  (set.range I.leading_coeff_nth) (set.ne_empty_of_mem ⟨0, rfl⟩) in
+  (set.range I.leading_coeff_nth) ⟨_, ⟨0, rfl⟩⟩ in
 have hm : M ∈ set.range I.leading_coeff_nth := well_founded.min_mem _ _ _,
 let ⟨N, HN⟩ := hm, ⟨s, hs⟩ := I.is_fg_degree_le N in
 have hm2 : ∀ k, I.leading_coeff_nth k ≤ M := λ k, or.cases_on (le_or_lt k N)
diff --git a/src/ring_theory/principal_ideal_domain.lean b/src/ring_theory/principal_ideal_domain.lean
index c300291acc2f4..765a4df8007ed 100644
--- a/src/ring_theory/principal_ideal_domain.lean
+++ b/src/ring_theory/principal_ideal_domain.lean
@@ -75,11 +75,8 @@ lemma mod_mem_iff {S : ideal α} {x y : α} (hy : y ∈ S) : x % y ∈ S ↔ x 
 @[priority 100] -- see Note [lower instance priority]
 instance euclidean_domain.to_principal_ideal_domain : principal_ideal_domain α :=
 { principal := λ S, by exactI
-    ⟨if h : {x : α | x ∈ S ∧ x ≠ 0} = ∅
-    then ⟨0, submodule.ext $ λ a, by rw [← @submodule.bot_coe α α _ _ ring.to_module, span_eq, submodule.mem_bot]; exact
-      ⟨λ haS, by_contradiction $ λ ha0, eq_empty_iff_forall_not_mem.1 h a ⟨haS, ha0⟩,
-      λ h₁, h₁.symm ▸ S.zero_mem⟩⟩
-    else
+    ⟨if h : {x : α | x ∈ S ∧ x ≠ 0}.nonempty
+    then
     have wf : well_founded euclidean_domain.r := euclidean_domain.r_well_founded α,
     have hmin : well_founded.min wf {x : α | x ∈ S ∧ x ≠ 0} h ∈ S ∧
         well_founded.min wf {x : α | x ∈ S ∧ x ≠ 0} h ≠ 0,
@@ -92,7 +89,10 @@ instance euclidean_domain.to_principal_ideal_domain : principal_ideal_domain α
           from λ h₁, well_founded.not_lt_min wf _ h h₁ (mod_lt x hmin.2),
         have x % well_founded.min wf {x : α | x ∈ S ∧ x ≠ 0} h = 0, by finish [(mod_mem_iff hmin.1).2 hx],
         by simp *),
-      λ hx, let ⟨y, hy⟩ := mem_span_singleton.1 hx in hy.symm ▸ ideal.mul_mem_right _ hmin.1⟩⟩⟩ }
+      λ hx, let ⟨y, hy⟩ := mem_span_singleton.1 hx in hy.symm ▸ ideal.mul_mem_right _ hmin.1⟩⟩
+    else ⟨0, submodule.ext $ λ a, by rw [← @submodule.bot_coe α α _ _ ring.to_module, span_eq, submodule.mem_bot]; exact
+      ⟨λ haS, by_contradiction $ λ ha0, h ⟨a, ⟨haS, ha0⟩⟩,
+      λ h₁, h₁.symm ▸ S.zero_mem⟩⟩⟩ }
 
 end
 
diff --git a/src/set_theory/cofinality.lean b/src/set_theory/cofinality.lean
index 212988724542c..31265ba54b267 100644
--- a/src/set_theory/cofinality.lean
+++ b/src/set_theory/cofinality.lean
@@ -114,8 +114,7 @@ begin
     { intro e, injection e with e, subst b,
       exact irrefl _ h } },
   { intro a,
-    have : {b : S | ¬ r b a} ≠ ∅ := let ⟨b, bS, ba⟩ := hS a in
-      @set.ne_empty_of_mem S {b | ¬ r b a} ⟨b, bS⟩ ba,
+    have : {b : S | ¬ r b a}.nonempty := let ⟨b, bS, ba⟩ := hS a in ⟨⟨b, bS⟩, ba⟩,
     let b := (is_well_order.wf s).min _ this,
     have ba : ¬r b a := (is_well_order.wf s).min_mem _ this,
     refine ⟨b, ⟨b.2, λ c, not_imp_not.1 $ λ h, _⟩, ba⟩,
diff --git a/src/set_theory/ordinal.lean b/src/set_theory/ordinal.lean
index 611f34b4c6d5c..5e60cd3b5fca2 100644
--- a/src/set_theory/ordinal.lean
+++ b/src/set_theory/ordinal.lean
@@ -294,7 +294,7 @@ def collapse_F [is_well_order β s] (f : r ≼o s) : Π a, {b // ¬ s (f a) b} :
   have : f a ∈ S, from λ a' h, ((trichotomous _ _)
     .resolve_left $ λ h', (IH a' h).2 $ trans (f.ord'.1 h) h')
     .resolve_left $ λ h', (IH a' h).2 $ h' ▸ f.ord'.1 h,
-  exact ⟨(is_well_order.wf s).min S (set.ne_empty_of_mem this),
+  exact ⟨(is_well_order.wf s).min S ⟨_, this⟩,
    (is_well_order.wf s).not_lt_min _ _ this⟩
 end
 
@@ -320,7 +320,7 @@ by haveI := order_embedding.is_well_order f; exact
   (λ a, (collapse_F f a).1) (λ a b, collapse_F.lt f),
 λ a b, acc.rec_on ((is_well_order.wf s).apply b) (λ b H IH a h, begin
   let S := {a | ¬ s (collapse_F f a).1 b},
-  have : S ≠ ∅ := set.ne_empty_of_mem (asymm h),
+  have : S.nonempty := ⟨_, asymm h⟩,
   existsi (is_well_order.wf r).min S this,
   refine ((@trichotomous _ s _ _ _).resolve_left _).resolve_right _,
   { exact (is_well_order.wf r).min_mem S this },
@@ -1244,7 +1244,7 @@ def typein.principal_seg {α : Type u} (r : α → α → Prop) [is_well_order 
 
 /-- The minimal element of a nonempty family of ordinals -/
 def min {ι} (I : nonempty ι) (f : ι → ordinal) : ordinal :=
-wf.min (set.range f) (let ⟨i⟩ := I in set.ne_empty_of_mem (set.mem_range_self i))
+wf.min (set.range f) (let ⟨i⟩ := I in ⟨_, set.mem_range_self i⟩)
 
 theorem min_eq {ι} (I) (f : ι → ordinal) : ∃ i, min I f = f i :=
 let ⟨i, e⟩ := wf.min_mem (set.range f) _ in ⟨i, e.symm⟩
diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
index cc7fae57ebf43..bb369d2e07bb9 100644
--- a/src/topology/constructions.lean
+++ b/src/topology/constructions.lean
@@ -246,7 +246,7 @@ lemma is_open_prod_iff' {s : set α} {t : set β} :
 begin
   by_cases h : set.prod s t = ∅,
   { simp [h, prod_eq_empty_iff.1 h] },
-  { have st : s ≠ ∅ ∧ t ≠ ∅, by rwa [← ne.def, prod_neq_empty_iff] at h,
+  { have st : s ≠ ∅ ∧ t ≠ ∅, by rwa [← ne.def, prod_ne_empty_iff] at h,
     split,
     { assume H : is_open (set.prod s t),
       refine or.inl ⟨_, _⟩,