diff --git a/src/algebra/associated.lean b/src/algebra/associated.lean
index f4dfe733ca848..455b423578205 100644
--- a/src/algebra/associated.lean
+++ b/src/algebra/associated.lean
@@ -223,7 +223,7 @@ iff.intro
   (assume h, let ⟨c, h⟩ := h.symm in h ▸ ⟨c, (one_mul _).symm⟩)
   (assume ⟨c, h⟩, associated.symm ⟨c, by simp [h]⟩)
 
-theorem associated_zero_iff_eq_zero [comm_semiring α] (a : α) : a ~ᵤ 0 ↔ a = 0 :=
+theorem associated_zero_iff_eq_zero [monoid_with_zero α] (a : α) : a ~ᵤ 0 ↔ a = 0 :=
 iff.intro
   (assume h, let ⟨u, h⟩ := h.symm in by simpa using h.symm)
   (assume h, h ▸ associated.refl a)
@@ -457,17 +457,30 @@ end comm_monoid
 instance [has_zero α] [monoid α] : has_zero (associates α) := ⟨⟦ 0 ⟧⟩
 instance [has_zero α] [monoid α] : has_top (associates α) := ⟨0⟩
 
-section comm_semiring
-variables [comm_semiring α]
+section comm_monoid_with_zero
+
+variables [comm_monoid_with_zero α]
 
 @[simp] theorem mk_eq_zero {a : α} : associates.mk a = 0 ↔ a = 0 :=
 ⟨assume h, (associated_zero_iff_eq_zero a).1 $ quotient.exact h, assume h, h.symm ▸ rfl⟩
 
-instance : mul_zero_class (associates α) :=
-{ mul := (*),
-  zero := 0,
-  zero_mul := by { rintro ⟨a⟩, show associates.mk (0 * a) = associates.mk 0, rw [zero_mul] },
-  mul_zero := by { rintro ⟨a⟩, show associates.mk (a * 0) = associates.mk 0, rw [mul_zero] } }
+instance : comm_monoid_with_zero (associates α) :=
+{ zero_mul := by { rintro ⟨a⟩, show associates.mk (0 * a) = associates.mk 0, rw [zero_mul] },
+  mul_zero := by { rintro ⟨a⟩, show associates.mk (a * 0) = associates.mk 0, rw [mul_zero] },
+  .. associates.comm_monoid, .. associates.has_zero }
+
+instance [nontrivial α] : nontrivial (associates α) :=
+⟨⟨0, 1,
+assume h,
+have (0 : α) ~ᵤ 1, from quotient.exact h,
+have (0 : α) = 1, from ((associated_zero_iff_eq_zero 1).1 this.symm).symm,
+zero_ne_one this⟩⟩
+
+end comm_monoid_with_zero
+
+section comm_semiring
+
+variables [comm_semiring α]
 
 theorem dvd_of_mk_le_mk {a b : α} : associates.mk a ≤ associates.mk b → a ∣ b
 | ⟨c', hc'⟩ := (quotient.induction_on c' $ assume c hc,
@@ -547,12 +560,6 @@ instance : order_top (associates α) :=
   le_top := assume a, ⟨0, mul_zero a⟩,
   .. associates.partial_order }
 
-instance : nonzero (associates α) :=
-⟨ assume h,
-  have (0 : α) ~ᵤ 1, from quotient.exact h,
-  have (0 : α) = 1, from ((associated_zero_iff_eq_zero 1).1 this.symm).symm,
-  zero_ne_one this ⟩
-
 instance : no_zero_divisors (associates α) :=
 ⟨λ x y,
   (quotient.induction_on₂ x y $ assume a b h,
@@ -562,7 +569,7 @@ instance : no_zero_divisors (associates α) :=
 
 theorem prod_eq_zero_iff {s : multiset (associates α)} :
   s.prod = 0 ↔ (0 : associates α) ∈ s :=
-multiset.induction_on s (by simp; exact zero_ne_one.symm) $
+multiset.induction_on s (by simp) $
   assume a s, by simp [mul_eq_zero, @eq_comm _ 0 a] {contextual := tt}
 
 theorem irreducible_mk_iff (a : α) : irreducible (associates.mk a) ↔ irreducible a :=
diff --git a/src/algebra/category/CommRing/basic.lean b/src/algebra/category/CommRing/basic.lean
index f4e8a28e71115..afc7e1f4e3a2b 100644
--- a/src/algebra/category/CommRing/basic.lean
+++ b/src/algebra/category/CommRing/basic.lean
@@ -49,7 +49,10 @@ instance : category SemiRing := infer_instance -- short-circuit type class infer
 instance : concrete_category SemiRing := infer_instance -- short-circuit type class inference
 
 instance has_forget_to_Mon : has_forget₂ SemiRing Mon :=
-bundled_hom.mk_has_forget₂ @semiring.to_monoid (λ R₁ R₂, ring_hom.to_monoid_hom) (λ _ _ _, rfl)
+bundled_hom.mk_has_forget₂
+  (λ R hR, @monoid_with_zero.to_monoid R (@semiring.to_monoid_with_zero R hR))
+  (λ R₁ R₂, ring_hom.to_monoid_hom) (λ _ _ _, rfl)
+
 instance has_forget_to_AddCommMon : has_forget₂ SemiRing AddCommMon :=
 -- can't use bundled_hom.mk_has_forget₂, since AddCommMon is an induced category
 { forget₂ :=
diff --git a/src/algebra/char_p.lean b/src/algebra/char_p.lean
index 118d112627806..0e0cabb53cdb1 100644
--- a/src/algebra/char_p.lean
+++ b/src/algebra/char_p.lean
@@ -258,10 +258,10 @@ calc r = 1 * r       : by rw one_mul
 
 end prio
 
-lemma false_of_nonzero_of_char_one [semiring R] [nonzero R] [char_p R 1] : false :=
+lemma false_of_nonzero_of_char_one [semiring R] [nontrivial R] [char_p R 1] : false :=
 zero_ne_one $ show (0:R) = 1, from subsingleton.elim 0 1
 
-lemma ring_char_ne_one [semiring R] [nonzero R] : ring_char R ≠ 1 :=
+lemma ring_char_ne_one [semiring R] [nontrivial R] : ring_char R ≠ 1 :=
 by { intros h, apply @zero_ne_one R, symmetry, rw [←nat.cast_one, ring_char.spec, h], }
 
 end char_one
diff --git a/src/algebra/classical_lie_algebras.lean b/src/algebra/classical_lie_algebras.lean
index 5428f62e78368..8309380a6df66 100644
--- a/src/algebra/classical_lie_algebras.lean
+++ b/src/algebra/classical_lie_algebras.lean
@@ -77,9 +77,9 @@ def Eb (h : j ≠ i) : sl n R :=
 
 end elementary_basis
 
-lemma sl_non_abelian [nonzero R] (h : 1 < fintype.card n) : ¬lie_algebra.is_abelian ↥(sl n R) :=
+lemma sl_non_abelian [nontrivial R] (h : 1 < fintype.card n) : ¬lie_algebra.is_abelian ↥(sl n R) :=
 begin
-  rcases fintype.exists_pair_of_one_lt_card h with ⟨i, j, hij⟩,
+  rcases fintype.exists_pair_of_one_lt_card h with ⟨j, i, hij⟩,
   let A := Eb R i j hij,
   let B := Eb R j i hij.symm,
   intros c,
diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean
index 1cff3faa6059c..7ade971ce2a4a 100644
--- a/src/algebra/direct_limit.lean
+++ b/src/algebra/direct_limit.lean
@@ -497,14 +497,14 @@ variables [directed_system G f]
 
 namespace direct_limit
 
-instance nonzero : nonzero (ring.direct_limit G f) :=
-{ zero_ne_one := nonempty.elim (by apply_instance) $ assume i : ι, begin
-    change (0 : ring.direct_limit G f) ≠ 1,
-    rw ← ring.direct_limit.of_one,
-    intros H, rcases ring.direct_limit.of.zero_exact H.symm with ⟨j, hij, hf⟩,
-    rw is_ring_hom.map_one (f i j hij) at hf,
-    exact one_ne_zero hf
-  end }
+instance nontrivial : nontrivial (ring.direct_limit G f) :=
+⟨⟨0, 1, nonempty.elim (by apply_instance) $ assume i : ι, begin
+  change (0 : ring.direct_limit G f) ≠ 1,
+  rw ← ring.direct_limit.of_one,
+  intros H, rcases ring.direct_limit.of.zero_exact H.symm with ⟨j, hij, hf⟩,
+  rw is_ring_hom.map_one (f i j hij) at hf,
+  exact one_ne_zero hf
+end ⟩⟩
 
 theorem exists_inv {p : ring.direct_limit G f} : p ≠ 0 → ∃ y, p * y = 1 :=
 ring.direct_limit.induction_on p $ λ i x H,
@@ -529,7 +529,7 @@ protected noncomputable def field : field (ring.direct_limit G f) :=
   mul_inv_cancel := λ p, direct_limit.mul_inv_cancel G f,
   inv_zero := dif_pos rfl,
   .. ring.direct_limit.comm_ring G f,
-  .. direct_limit.nonzero G f }
+  .. direct_limit.nontrivial G f }
 
 end
 
diff --git a/src/algebra/euclidean_domain.lean b/src/algebra/euclidean_domain.lean
index 28e086c116c85..797434c08965e 100644
--- a/src/algebra/euclidean_domain.lean
+++ b/src/algebra/euclidean_domain.lean
@@ -14,7 +14,7 @@ section prio
 set_option default_priority 100 -- see Note [default priority]
 set_option old_structure_cmd true
 @[protect_proj without mul_left_not_lt r_well_founded]
-class euclidean_domain (α : Type u) extends comm_ring α :=
+class euclidean_domain (α : Type u) extends comm_ring α, nontrivial α :=
 (quotient : α → α → α)
 (quotient_zero : ∀ a, quotient a 0 = 0)
 (remainder : α → α → α)
@@ -32,7 +32,6 @@ class euclidean_domain (α : Type u) extends comm_ring α :=
   function from weak to strong. I've currently divided the lemmas into
   strong and weak depending on whether they require `val_le_mul_left` or not. -/
 (mul_left_not_lt : ∀ a {b}, b ≠ 0 → ¬r (a * b) a)
-(zero_ne_one : (0 : α) ≠ 1)
 end prio
 
 namespace euclidean_domain
@@ -41,9 +40,6 @@ variables [euclidean_domain α]
 
 local infix ` ≺ `:50 := euclidean_domain.r
 
-@[priority 70] -- see Note [lower instance priority]
-instance : nonzero α := ⟨euclidean_domain.zero_ne_one⟩
-
 @[priority 70] -- see Note [lower instance priority]
 instance : has_div α := ⟨euclidean_domain.quotient⟩
 
@@ -351,7 +347,7 @@ instance int.euclidean_domain : euclidean_domain ℤ :=
     by rw [← mul_one a.nat_abs, int.nat_abs_mul];
     exact mul_le_mul_of_nonneg_left (int.nat_abs_pos_of_ne_zero b0) (nat.zero_le _),
   .. int.comm_ring,
-  .. int.nonzero }
+  .. int.nontrivial }
 
 @[priority 100] -- see Note [lower instance priority]
 instance field.to_euclidean_domain {K : Type u} [field K] : euclidean_domain K :=
diff --git a/src/algebra/field.lean b/src/algebra/field.lean
index be5139497cdea..f72ba4e3ef9e9 100644
--- a/src/algebra/field.lean
+++ b/src/algebra/field.lean
@@ -14,18 +14,14 @@ universe u
 variables {α : Type u}
 
 @[protect_proj, ancestor ring has_inv]
-class division_ring (α : Type u) extends ring α, has_inv α :=
+class division_ring (α : Type u) extends ring α, has_inv α, nontrivial α :=
 (mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1)
 (inv_mul_cancel : ∀ {a : α}, a ≠ 0 → a⁻¹ * a = 1)
 (inv_zero : (0 : α)⁻¹ = 0)
-(zero_ne_one : (0 : α) ≠ 1)
 
 section division_ring
 variables [division_ring α] {a b : α}
 
-instance division_ring.to_nonzero : nonzero α :=
-⟨division_ring.zero_ne_one⟩
-
 instance division_ring_has_div : has_div α :=
 ⟨λ a b, a * b⁻¹⟩
 
@@ -115,10 +111,9 @@ instance division_ring.to_domain : domain α :=
 end division_ring
 
 @[protect_proj, ancestor division_ring comm_ring]
-class field (α : Type u) extends comm_ring α, has_inv α :=
+class field (α : Type u) extends comm_ring α, has_inv α, nontrivial α :=
 (mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1)
 (inv_zero : (0 : α)⁻¹ = 0)
-(zero_ne_one : (0 : α) ≠ 1)
 
 section field
 
diff --git a/src/algebra/group/prod.lean b/src/algebra/group/prod.lean
index 6a843fc9efa5a..3f51ede624513 100644
--- a/src/algebra/group/prod.lean
+++ b/src/algebra/group/prod.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
 -/
 import algebra.group.hom
+import algebra.group_with_zero
 import data.prod
 
 /-!
diff --git a/src/algebra/group/with_one.lean b/src/algebra/group/with_one.lean
index bafd7417b5036..c865c3b7aeb64 100644
--- a/src/algebra/group/with_one.lean
+++ b/src/algebra/group/with_one.lean
@@ -23,6 +23,9 @@ instance : has_one (with_one α) := ⟨none⟩
 @[to_additive]
 instance : inhabited (with_one α) := ⟨1⟩
 
+@[to_additive]
+instance [nonempty α] : nontrivial (with_one α) := option.nontrivial
+
 @[to_additive]
 instance : has_coe_t α (with_one α) := ⟨some⟩
 
@@ -117,9 +120,6 @@ namespace with_zero
 instance [one : has_one α] : has_one (with_zero α) :=
 { ..one }
 
-instance [has_one α] : nonzero (with_zero α) :=
-{ zero_ne_one := λ h, option.no_confusion h }
-
 lemma coe_one [has_one α] : ((1 : α) : with_zero α) = 1 := rfl
 
 instance [has_mul α] : mul_zero_class (with_zero α) :=
@@ -148,7 +148,7 @@ instance [comm_semigroup α] : comm_semigroup (with_zero α) :=
     end,
   ..with_zero.semigroup }
 
-instance [monoid α] : monoid (with_zero α) :=
+instance [monoid α] : monoid_with_zero (with_zero α) :=
 { one_mul := λ a, match a with
     | none   := rfl
     | some a := congr_arg some $ one_mul _
@@ -157,12 +157,12 @@ instance [monoid α] : monoid (with_zero α) :=
     | none   := rfl
     | some a := congr_arg some $ mul_one _
     end,
+  ..with_zero.mul_zero_class,
   ..with_zero.has_one,
-  ..with_zero.nonzero,
   ..with_zero.semigroup }
 
-instance [comm_monoid α] : comm_monoid (with_zero α) :=
-{ ..with_zero.monoid, ..with_zero.comm_semigroup }
+instance [comm_monoid α] : comm_monoid_with_zero (with_zero α) :=
+{ ..with_zero.monoid_with_zero, ..with_zero.comm_semigroup }
 
 definition inv [has_inv α] (x : with_zero α) : with_zero α :=
 do a ← x, return a⁻¹
@@ -260,7 +260,7 @@ instance [semiring α] : semiring (with_zero α) :=
   end,
   ..with_zero.add_comm_monoid,
   ..with_zero.mul_zero_class,
-  ..with_zero.monoid }
+  ..with_zero.monoid_with_zero }
 
 end semiring
 
diff --git a/src/algebra/group_with_zero.lean b/src/algebra/group_with_zero.lean
index 13d3d120d06a9..0cf39cae69df4 100644
--- a/src/algebra/group_with_zero.lean
+++ b/src/algebra/group_with_zero.lean
@@ -9,6 +9,7 @@ import tactic.localized
 import logic.unique
 import algebra.group.commute
 import algebra.group.units_hom
+import logic.nontrivial
 import algebra.group.inj_surj
 
 /-!
@@ -47,6 +48,8 @@ reduce an expression in a field to an expression of the form `n / d` where `n` a
 division-free."
 
 section
+
+section prio
 set_option default_priority 100 -- see Note [default priority]
 
 /-- Typeclass for expressing that a type `M₀` with multiplication and a zero satisfies
@@ -56,6 +59,8 @@ class mul_zero_class (M₀ : Type*) extends has_mul M₀, has_zero M₀ :=
 (zero_mul : ∀ a : M₀, 0 * a = 0)
 (mul_zero : ∀ a : M₀, a * 0 = 0)
 
+end prio
+
 section mul_zero_class
 
 variables [mul_zero_class M₀] {a b : M₀}
@@ -97,49 +102,6 @@ lemma ne_zero_and_ne_zero_of_mul (h : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
 
 end mul_zero_class
 
-/-- Predicate typeclass for expressing that a (semi)ring or similar algebraic structure
-is nonzero. -/
-@[protect_proj] class nonzero (M₀ : Type*) [has_zero M₀] [has_one M₀] : Prop :=
-(zero_ne_one : 0 ≠ (1:M₀))
-
-section
-
-variables [has_zero M₀] [has_one M₀] [nonzero M₀]
-
-@[simp] lemma zero_ne_one : 0 ≠ (1:M₀) := nonzero.zero_ne_one
-
-@[simp] lemma one_ne_zero : (1:M₀) ≠ 0 := zero_ne_one.symm
-
-lemma ne_zero_of_eq_one {a : M₀} (h : a = 1) : a ≠ 0 :=
-calc a = 1 : h
-   ... ≠ 0 : one_ne_zero
-
-/-- Pushforward a `nonzero` instance along an injective function. -/
-protected lemma function.injective.nonzero [has_zero M₀'] [has_one M₀']
-  (f : M₀ → M₀') (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1) :
-  nonzero M₀' :=
-⟨zero ▸ (hf.ne_iff' one).2 zero_ne_one⟩
-
-/-- Pullback a `nonzero` instance along a function sending `0` to `0` and `1` to `1`. -/
-protected lemma pullback_nonzero [has_zero M₀'] [has_one M₀']
-  (f : M₀' → M₀) (zero : f 0 = 0) (one : f 1 = 1) :
-  nonzero M₀' :=
-⟨mt (congr_arg f) $ by { rw [zero, one], exact zero_ne_one }⟩
-
-end
-
-section
-
-variables [mul_zero_class M₀] [has_one M₀] [nonzero M₀] {a b : M₀}
-
-lemma left_ne_zero_of_mul_eq_one (h : a * b = 1) : a ≠ 0 :=
-left_ne_zero_of_mul $ ne_zero_of_eq_one h
-
-lemma right_ne_zero_of_mul_eq_one (h : a * b = 1) : b ≠ 0 :=
-right_ne_zero_of_mul $ ne_zero_of_eq_one h
-
-end
-
 /-- Predicate typeclass for expressing that `a * b = 0` implies `a = 0` or `b = 0`
 for all `a` and `b` of type `G₀`. -/
 class no_zero_divisors (M₀ : Type*) [has_mul M₀] [has_zero M₀] : Prop :=
@@ -214,6 +176,42 @@ and right absorbing, and left/right multiplication by a non-zero element is inje
 (mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c)
 (mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c)
 
+section
+
+variables [monoid_with_zero M₀] [nontrivial M₀] {a b : M₀}
+
+/-- In a nontrivial monoid with zero, zero and one are different. -/
+@[simp] lemma zero_ne_one : 0 ≠ (1:M₀) :=
+begin
+  assume h,
+  rcases exists_pair_ne M₀ with ⟨x, y, hx⟩,
+  apply hx,
+  calc x = 1 * x : by rw [one_mul]
+  ... = 0 : by rw [← h, zero_mul]
+  ... = 1 * y : by rw [← h, zero_mul]
+  ... = y : by rw [one_mul]
+end
+
+@[simp] lemma one_ne_zero : (1:M₀) ≠ 0 :=
+zero_ne_one.symm
+
+lemma ne_zero_of_eq_one {a : M₀} (h : a = 1) : a ≠ 0 :=
+calc a = 1 : h
+   ... ≠ 0 : one_ne_zero
+
+lemma left_ne_zero_of_mul_eq_one (h : a * b = 1) : a ≠ 0 :=
+left_ne_zero_of_mul $ ne_zero_of_eq_one h
+
+lemma right_ne_zero_of_mul_eq_one (h : a * b = 1) : b ≠ 0 :=
+right_ne_zero_of_mul $ ne_zero_of_eq_one h
+
+/-- Pullback a `nontrivial` instance along a function sending `0` to `0` and `1` to `1`. -/
+protected lemma pullback_nonzero [has_zero M₀'] [has_one M₀']
+  (f : M₀' → M₀) (zero : f 0 = 0) (one : f 1 = 1) : nontrivial M₀' :=
+⟨⟨0, 1, mt (congr_arg f) $ by { rw [zero, one], exact zero_ne_one }⟩⟩
+
+end
+
 /-- A type `M` is a commutative “monoid with zero” if it is a commutative monoid with zero
 element, and `0` is left and right absorbing. -/
 @[protect_proj]
@@ -225,13 +223,9 @@ The type is required to come with an “inverse” function, and the inverse of
 
 Examples include division rings and the ordered monoids that are the
 target of valuations in general valuation theory.-/
-class group_with_zero (G₀ : Type*) extends monoid_with_zero G₀, has_inv G₀ :=
+class group_with_zero (G₀ : Type*) extends monoid_with_zero G₀, has_inv G₀, nontrivial G₀ :=
 (inv_zero : (0 : G₀)⁻¹ = 0)
 (mul_inv_cancel : ∀ a:G₀, a ≠ 0 → a * a⁻¹ = 1)
-(zero_ne_one : (0 : G₀) ≠ 1)
-
-instance group_with_zero.to_nonzero (G₀ : Type*) [group_with_zero G₀] : nonzero G₀ :=
-⟨group_with_zero.zero_ne_one⟩
 
 /-- A type `G₀` is a commutative “group with zero”
 if it is a commutative monoid with zero element (distinct from `1`)
@@ -283,7 +277,7 @@ variables [monoid_with_zero M₀]
 
 namespace units
 
-@[simp] lemma ne_zero [nonzero M₀] (u : units M₀) :
+@[simp] lemma ne_zero [nontrivial M₀] (u : units M₀) :
   (u : M₀) ≠ 0 :=
 left_ne_zero_of_mul_eq_one u.mul_inv
 
@@ -300,7 +294,7 @@ end units
 
 namespace is_unit
 
-lemma ne_zero [nonzero M₀] {a : M₀} (ha : is_unit a) : a ≠ 0 := let ⟨u, hu⟩ := ha in hu ▸ u.ne_zero
+lemma ne_zero [nontrivial M₀] {a : M₀} (ha : is_unit a) : a ≠ 0 := let ⟨u, hu⟩ := ha in hu ▸ u.ne_zero
 
 lemma mul_right_eq_zero {a b : M₀} (ha : is_unit a) : a * b = 0 ↔ b = 0 :=
 let ⟨u, hu⟩ := ha in hu ▸ u.mul_right_eq_zero
@@ -332,24 +326,11 @@ lemma eq_of_zero_eq_one (h : (0 : M₀) = 1) (a b : M₀) : a = b :=
 ⟨λ ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩, by rwa zero_mul at a0,
  λ h, ⟨⟨0, 0, eq_of_zero_eq_one h _ _, eq_of_zero_eq_one h _ _⟩, rfl⟩⟩
 
-@[simp] theorem not_is_unit_zero [nonzero M₀] : ¬ is_unit (0 : M₀) :=
+@[simp] theorem not_is_unit_zero [nontrivial M₀] : ¬ is_unit (0 : M₀) :=
 mt is_unit_zero_iff.1 zero_ne_one
 
 variable (M₀)
 
-/-- A monoid with zero is either nonzero, or has a unique element. -/
-noncomputable def nonzero_psum_unique : psum (nonzero M₀) (unique M₀) :=
-if h : (0:M₀) = 1 then psum.inr (unique_of_zero_eq_one h) else psum.inl ⟨h⟩
-
-/-- A monoid with zero is either a subsingleton or nonzero. -/
-lemma subsingleton_or_nonzero :  subsingleton M₀ ∨ nonzero M₀ :=
-begin
-  classical,
-  by_cases h : (0 : M₀) = 1,
-  { left, exact subsingleton_of_zero_eq_one h },
-  { right, exact ⟨h⟩ }
-end
-
 /-- In a monoid with zero, either zero and one are nonequal, or zero is the only element. -/
 lemma zero_ne_one_or_forall_eq_0 : (0 : M₀) ≠ 1 ∨ (∀a:M₀, a = 0) :=
 not_or_of_imp eq_zero_of_zero_eq_one
@@ -428,7 +409,7 @@ protected def function.surjective.group_with_zero [has_zero G₀'] [has_mul G₀
   mul_inv_cancel := hf.forall.2 $ λ x hx,
     by erw [← inv, ← mul, mul_inv_cancel (mt (congr_arg f) $ trans_rel_left ne hx zero.symm)];
       exact one,
-  zero_ne_one := h01,
+  exists_pair_ne := ⟨0, 1, h01⟩,
   .. hf.monoid_with_zero f zero one mul }
 
 @[simp] lemma mul_inv_cancel_right' {b : G₀} (h : b ≠ 0) (a : G₀) :
diff --git a/src/algebra/opposites.lean b/src/algebra/opposites.lean
index 140045d7bfe71..2c033b9a2f057 100644
--- a/src/algebra/opposites.lean
+++ b/src/algebra/opposites.lean
@@ -35,6 +35,9 @@ instance [add_comm_semigroup α] : add_comm_semigroup (opposite α) :=
 instance [has_zero α] : has_zero (opposite α) :=
 { zero := op 0 }
 
+instance [nontrivial α] : nontrivial (opposite α) :=
+let ⟨x, y, h⟩ := exists_pair_ne α in nontrivial_of_ne (op x) (op y) (op_injective.ne h)
+
 section
 local attribute [reducible] opposite
 @[simp] lemma unop_eq_zero_iff [has_zero α] (a : αᵒᵖ) : a.unop = (0 : α) ↔ a = (0 : αᵒᵖ) :=
@@ -127,19 +130,16 @@ instance [ring α] : ring (opposite α) :=
 instance [comm_ring α] : comm_ring (opposite α) :=
 { .. opposite.ring α, .. opposite.comm_semigroup α }
 
-instance [has_zero α] [has_one α] [nonzero α] : nonzero (opposite α) :=
-{ zero_ne_one := λ h : op (0 : α) = op 1, zero_ne_one (op_injective h) }
-
 instance [integral_domain α] : integral_domain (opposite α) :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ x y (H : op (_ * _) = op (0:α)),
     or.cases_on (eq_zero_or_eq_zero_of_mul_eq_zero $ op_injective H)
       (λ hy, or.inr $ unop_injective $ hy) (λ hx, or.inl $ unop_injective $ hx),
-  .. opposite.comm_ring α, .. opposite.nonzero α }
+  .. opposite.comm_ring α, .. opposite.nontrivial α }
 
 instance [field α] : field (opposite α) :=
 { mul_inv_cancel := λ x hx, unop_injective $ inv_mul_cancel $ λ hx', hx $ unop_injective hx',
   inv_zero := unop_injective inv_zero,
-  .. opposite.comm_ring α, .. opposite.nonzero α, .. opposite.has_inv α }
+  .. opposite.comm_ring α, .. opposite.has_inv α, .. opposite.nontrivial α }
 
 @[simp] lemma op_zero [has_zero α] : op (0 : α) = 0 := rfl
 @[simp] lemma unop_zero [has_zero α] : unop (0 : αᵒᵖ) = 0 := rfl
diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean
index 6357cc2cd7647..1dfb6b87c5c1f 100644
--- a/src/algebra/ordered_group.lean
+++ b/src/algebra/ordered_group.lean
@@ -333,13 +333,14 @@ instance [add_comm_semigroup α] : add_comm_semigroup (with_top α) :=
 instance [add_monoid α] : add_monoid (with_top α) :=
 { zero := some 0,
   add := (+),
-  ..@additive.add_monoid _ $ @with_zero.monoid (multiplicative α) _ }
+  ..@additive.add_monoid _ $ @monoid_with_zero.to_monoid _ $
+    @with_zero.monoid_with_zero (multiplicative α) _ }
 
 instance [add_comm_monoid α] : add_comm_monoid (with_top α) :=
 { zero := 0,
   add := (+),
-  ..@additive.add_comm_monoid _ $
-    @with_zero.comm_monoid (multiplicative α) _ }
+  ..@additive.add_comm_monoid _ $ @comm_monoid_with_zero.to_comm_monoid _ $
+    @with_zero.comm_monoid_with_zero (multiplicative α) _ }
 
 instance [ordered_add_comm_monoid α] : ordered_add_comm_monoid (with_top α) :=
 begin
diff --git a/src/algebra/ordered_ring.lean b/src/algebra/ordered_ring.lean
index 86d8b8049f65e..bb9dca450f706 100644
--- a/src/algebra/ordered_ring.lean
+++ b/src/algebra/ordered_ring.lean
@@ -430,16 +430,12 @@ end decidable_linear_ordered_semiring
 /-- An `ordered_ring α` is a ring `α` with a partial order such that
 multiplication with a positive number and addition are monotone. -/
 @[protect_proj]
-class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
+class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α, nontrivial α :=
 (mul_pos     : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)
-(zero_ne_one : (0 : α) ≠ 1)
 
 section ordered_ring
 variables [ordered_ring α] {a b c : α}
 
-instance ordered_ring.to_nonzero : nonzero α :=
-⟨ordered_ring.zero_ne_one⟩
-
 lemma ordered_ring.mul_nonneg (a b : α) (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) : 0 ≤ a * b :=
 begin
   cases classical.em (a ≤ 0), { simp [le_antisymm h h₁] },
@@ -815,10 +811,9 @@ end decidable_linear_ordered_comm_ring
 
 /-- Extend `nonneg_add_comm_group` to support ordered rings
   specified by their nonnegative elements -/
-class nonneg_ring (α : Type*) extends ring α, nonneg_add_comm_group α :=
+class nonneg_ring (α : Type*) extends ring α, nonneg_add_comm_group α, nontrivial α :=
 (mul_nonneg : ∀ {a b}, nonneg a → nonneg b → nonneg (a * b))
 (mul_pos : ∀ {a b}, pos a → pos b → pos (a * b))
-(zero_ne_one : (0 : α) ≠ 1)
 
 /-- Extend `nonneg_add_comm_group` to support linearly ordered rings
   specified by their nonnegative elements -/
@@ -927,18 +922,14 @@ end linear_nonneg_ring
 in which `a ≤ b` iff there exists `c` with `b = a + c`. This is satisfied by the
 natural numbers, for example, but not the integers or other ordered groups. -/
 class canonically_ordered_comm_semiring (α : Type*) extends
-  canonically_ordered_add_monoid α, comm_semiring α :=
+  canonically_ordered_add_monoid α, comm_semiring α, nontrivial α :=
 (eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0)
-(zero_ne_one : (0 : α) ≠ 1)
 
 namespace canonically_ordered_semiring
 variables [canonically_ordered_comm_semiring α] {a b : α}
 
 open canonically_ordered_add_monoid (le_iff_exists_add)
 
-instance canonically_ordered_comm_semiring.to_nonzero : nonzero α :=
-⟨canonically_ordered_comm_semiring.zero_ne_one⟩
-
 instance canonically_ordered_comm_semiring.to_no_zero_divisors :
   no_zero_divisors α :=
 ⟨canonically_ordered_comm_semiring.eq_zero_or_eq_zero_of_mul_eq_zero⟩
@@ -962,8 +953,8 @@ end canonically_ordered_semiring
 
 namespace with_top
 
-instance [has_zero α] [has_one α] [nonzero α] : nonzero (with_top α) :=
-⟨mt coe_eq_coe.1 zero_ne_one⟩
+instance [nonempty α] : nontrivial (with_top α) :=
+option.nontrivial
 
 variable [decidable_eq α]
 
@@ -1075,6 +1066,6 @@ instance : canonically_ordered_comm_semiring (with_top α) :=
   one_mul         := one_mul',
   mul_one         := assume a, by rw [comm, one_mul'],
   .. with_top.add_comm_monoid, .. with_top.mul_zero_class, .. with_top.canonically_ordered_add_monoid,
-  .. with_top.no_zero_divisors, .. with_top.nonzero }
+  .. with_top.no_zero_divisors, .. with_top.nontrivial }
 
 end with_top
diff --git a/src/algebra/ring.lean b/src/algebra/ring.lean
index 7c83e33ed2270..cce36e1a87710 100644
--- a/src/algebra/ring.lean
+++ b/src/algebra/ring.lean
@@ -101,14 +101,12 @@ protected def function.surjective.distrib {S} [distrib R] [has_add S] [has_mul S
 ### Semirings
 -/
 
-@[protect_proj, ancestor add_comm_monoid monoid distrib mul_zero_class]
-class semiring (α : Type u) extends add_comm_monoid α, monoid α, distrib α, mul_zero_class α
+@[protect_proj, ancestor add_comm_monoid monoid_with_zero distrib]
+class semiring (α : Type u) extends add_comm_monoid α, monoid_with_zero α, distrib α
 
 section semiring
 variables [semiring α]
 
-instance semiring.to_monoid_with_zero : monoid_with_zero α := { .. (‹_› : semiring α) }
-
 /-- Pullback a `semiring` instance along an injective function. -/
 protected def function.injective.semiring [has_zero β] [has_one β] [has_add β] [has_mul β]
   (f : β → α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
@@ -334,6 +332,9 @@ end ring_hom
 @[protect_proj, ancestor semiring comm_monoid]
 class comm_semiring (α : Type u) extends semiring α, comm_monoid α
 
+instance comm_semiring.to_comm_monoid_with_zero [comm_semiring α] : comm_monoid_with_zero α :=
+{ .. comm_semiring.to_comm_monoid α, .. comm_semiring.to_semiring α }
+
 section comm_semiring
 variables [comm_semiring α] [comm_semiring β] {a b c : α}
 
@@ -735,27 +736,22 @@ end
 
 end comm_ring
 
-lemma succ_ne_self [ring α] [nonzero α] (a : α) : a + 1 ≠ a :=
+lemma succ_ne_self [ring α] [nontrivial α] (a : α) : a + 1 ≠ a :=
 λ h, one_ne_zero ((add_right_inj a).mp (by simp [h]))
 
-lemma pred_ne_self [ring α] [nonzero α] (a : α) : a - 1 ≠ a :=
+lemma pred_ne_self [ring α] [nontrivial α] (a : α) : a - 1 ≠ a :=
 λ h, one_ne_zero (neg_injective ((add_right_inj a).mp (by { convert h, simp })))
 
 /-- An element of the unit group of a nonzero semiring represented as an element
     of the semiring is nonzero. -/
-lemma units.coe_ne_zero [semiring α] [nonzero α] (u : units α) : (u : α) ≠ 0 :=
+lemma units.coe_ne_zero [semiring α] [nontrivial α] (u : units α) : (u : α) ≠ 0 :=
 λ h : u.1 = 0, by simpa [h, zero_ne_one] using u.3
 
-/-- Proves that a semiring that contains at least two distinct elements is nonzero. -/
-theorem nonzero.of_ne [semiring α] {x y : α} (h : x ≠ y) : nonzero α :=
-{ zero_ne_one := λ h01, h $ by rw [← one_mul x, ← one_mul y, ← h01, zero_mul, zero_mul] }
-
 /-- A domain is a ring with no zero divisors, i.e. satisfying
   the condition `a * b = 0 ↔ a = 0 ∨ b = 0`. Alternatively, a domain
   is an integral domain without assuming commutativity of multiplication. -/
-@[protect_proj] class domain (α : Type u) extends ring α :=
+@[protect_proj] class domain (α : Type u) extends ring α, nontrivial α :=
 (eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0)
-(zero_ne_one : (0 : α) ≠ 1)
 
 section domain
 variable [domain α]
@@ -763,9 +759,6 @@ variable [domain α]
 instance domain.to_no_zero_divisors : no_zero_divisors α :=
 ⟨domain.eq_zero_or_eq_zero_of_mul_eq_zero⟩
 
-instance domain.to_nonzero : nonzero α :=
-⟨domain.zero_ne_one⟩
-
 instance domain.to_cancel_monoid_with_zero : cancel_monoid_with_zero α :=
 { mul_left_cancel_of_ne_zero := λ a b c ha,
     by { rw [← sub_eq_zero, ← mul_sub], simp [ha, sub_eq_zero] },
@@ -890,10 +883,13 @@ end is_unit
 
 This is mainly useful because such a predicate does not contain data,
 and can therefore be easily transported along ring isomorphisms. -/
-structure is_integral_domain (R : Type u) [ring R] : Prop :=
+structure is_integral_domain (R : Type u) [ring R] extends nontrivial R : Prop :=
 (mul_comm : ∀ (x y : R), x * y = y * x)
 (eq_zero_or_eq_zero_of_mul_eq_zero : ∀ x y : R, x * y = 0 → x = 0 ∨ y = 0)
-(zero_ne_one : (0 : R) ≠ 1)
+
+-- The linter does not recognize that is_integral_domain.to_nontrivial is a structure
+-- projection, disable it
+attribute [nolint def_lemma doc_blame] is_integral_domain.to_nontrivial
 
 /-- Every integral domain satisfies the predicate for integral domains. -/
 lemma integral_domain.to_is_integral_domain (R : Type u) [integral_domain R] :
diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 9ceae53b6c0f2..d9146d10e6584 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -455,7 +455,7 @@ begin
   exact norm_pow_le a (nat.succ_le_iff.mp h),
 end
 
-lemma units.norm_pos {α : Type*} [normed_ring α] [nonzero α] (x : units α) : 0 < ∥(x:α)∥ :=
+lemma units.norm_pos {α : Type*} [normed_ring α] [nontrivial α] (x : units α) : 0 < ∥(x:α)∥ :=
 norm_pos_iff.mpr (units.coe_ne_zero x)
 
 /-- In a normed ring, the left-multiplication `add_monoid_hom` is bounded. -/
@@ -855,7 +855,7 @@ begin
   simpa [f, dist_eq_norm, norm_smul] using hc
 end
 
-theorem interior_closed_ball' [normed_space ℝ E] (x : E) (r : ℝ) (hE : ∃ z : E, z ≠ 0) :
+theorem interior_closed_ball' [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :
   interior (closed_ball x r) = ball x r :=
 begin
   rcases lt_trichotomy r 0 with hr|rfl|hr,
@@ -866,7 +866,7 @@ begin
       obtain rfl : y = x := set.mem_singleton_iff.1 (interior_subset hy),
       exact this hy },
     rw [← set.mem_compl_iff, ← closure_compl],
-    rcases hE with ⟨z, hz⟩,
+    rcases exists_ne (0 : E) with ⟨z, hz⟩,
     suffices : (λ c : ℝ, x + c • z) 0 ∈ closure ({x}ᶜ : set E),
       by simpa only [zero_smul, add_zero] using this,
     have : (0:ℝ) ∈ closure (set.Ioi (0:ℝ)), by simp [closure_Ioi],
@@ -882,10 +882,9 @@ theorem frontier_closed_ball [normed_space ℝ E] (x : E) {r : ℝ} (hr : 0 < r)
 by rw [frontier, closure_closed_ball, interior_closed_ball x hr,
   closed_ball_diff_ball]
 
-theorem frontier_closed_ball' [normed_space ℝ E] (x : E) (r : ℝ) (hE : ∃ z : E, z ≠ 0) :
+theorem frontier_closed_ball' [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :
   frontier (closed_ball x r) = sphere x r :=
-by rw [frontier, closure_closed_ball, interior_closed_ball' x r hE,
-  closed_ball_diff_ball]
+by rw [frontier, closure_closed_ball, interior_closed_ball' x r, closed_ball_diff_ball]
 
 open normed_field
 
@@ -982,8 +981,8 @@ begin
   rw @normed_algebra.norm_one 𝕜, norm_num,
 end
 
-lemma normed_algebra.to_nonzero : nonzero 𝕜' :=
-{ zero_ne_one := normed_algebra.zero_ne_one 𝕜 }
+lemma normed_algebra.to_nonzero : nontrivial 𝕜' :=
+⟨⟨0, 1, normed_algebra.zero_ne_one 𝕜⟩⟩
 
 end normed_algebra
 
diff --git a/src/analysis/normed_space/hahn_banach.lean b/src/analysis/normed_space/hahn_banach.lean
index 7c55577adbe4a..d8bd90feeedb4 100644
--- a/src/analysis/normed_space/hahn_banach.lean
+++ b/src/analysis/normed_space/hahn_banach.lean
@@ -75,11 +75,11 @@ end
 
 /-- Variant of the above theorem, eliminating the hypothesis that `x` be nonzero, and choosing
     the dual element arbitrarily when `x = 0`. -/
-theorem exists_dual_vector' (h : 0 < vector_space.dim ℝ E) (x : E) : ∃ g : E →L[ℝ] ℝ,
+theorem exists_dual_vector' [nontrivial E] (x : E) : ∃ g : E →L[ℝ] ℝ,
   ∥g∥ = 1 ∧ g x = ∥x∥ :=
 begin
   by_cases hx : x = 0,
-  { cases dim_pos_iff_exists_ne_zero.mp h with y hy,
+  { rcases exists_ne (0 : E) with ⟨y, hy⟩,
     cases exists_dual_vector y hy with g hg,
     use g, refine ⟨hg.left, _⟩, simp [hx] },
   { exact exists_dual_vector x hx }
diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean
index c6db394f511b6..d14eb1f130b31 100644
--- a/src/analysis/normed_space/operator_norm.lean
+++ b/src/analysis/normed_space/operator_norm.lean
@@ -302,13 +302,13 @@ lemma norm_id_le : ∥id 𝕜 E∥ ≤ 1 :=
 op_norm_le_bound _ zero_le_one (λx, by simp)
 
 /-- If a space is non-trivial, then the norm of the identity equals `1`. -/
-lemma norm_id (h : ∃ x : E, x ≠ 0) : ∥id 𝕜 E∥ = 1 :=
-le_antisymm norm_id_le $ let ⟨x, hx⟩ := h in
+lemma norm_id [nontrivial E] : ∥id 𝕜 E∥ = 1 :=
+le_antisymm norm_id_le $ let ⟨x, hx⟩ := exists_ne (0 : E) in
 have _ := (id 𝕜 E).ratio_le_op_norm x,
 by rwa [id_apply, div_self (ne_of_gt $ norm_pos_iff.2 hx)] at this
 
 @[simp] lemma norm_id_field : ∥id 𝕜 𝕜∥ = 1 :=
-norm_id ⟨1, one_ne_zero⟩
+norm_id
 
 @[simp] lemma norm_id_field' : ∥(1 : 𝕜 →L[𝕜] 𝕜)∥ = 1 :=
 norm_id_field
@@ -684,22 +684,26 @@ e.is_O_comp_rev _ _
 lemma uniform_embedding : uniform_embedding e :=
 e.antilipschitz.uniform_embedding e.lipschitz.uniform_continuous
 
-lemma one_le_norm_mul_norm_symm (h : ∃ x : E, x ≠ 0) :
+lemma one_le_norm_mul_norm_symm [nontrivial E] :
   1 ≤ ∥(e : E →L[𝕜] F)∥ * ∥(e.symm : F →L[𝕜] E)∥ :=
 begin
   rw [mul_comm],
   convert (e.symm : F →L[𝕜] E).op_norm_comp_le (e : E →L[𝕜] F),
-  rw [e.coe_symm_comp_coe, continuous_linear_map.norm_id h]
+  rw [e.coe_symm_comp_coe, continuous_linear_map.norm_id]
 end
 
-lemma norm_pos (h : ∃ x : E, x ≠ 0) : 0 < ∥(e : E →L[𝕜] F)∥ :=
-pos_of_mul_pos_right (lt_of_lt_of_le zero_lt_one (e.one_le_norm_mul_norm_symm h)) (norm_nonneg _)
+lemma norm_pos [nontrivial E] : 0 < ∥(e : E →L[𝕜] F)∥ :=
+pos_of_mul_pos_right (lt_of_lt_of_le zero_lt_one e.one_le_norm_mul_norm_symm) (norm_nonneg _)
 
-lemma norm_symm_pos (h : ∃ x : E, x ≠ 0) : 0 < ∥(e.symm : F →L[𝕜] E)∥ :=
-pos_of_mul_pos_left (lt_of_lt_of_le zero_lt_one (e.one_le_norm_mul_norm_symm h)) (norm_nonneg _)
+lemma norm_symm_pos [nontrivial E] : 0 < ∥(e.symm : F →L[𝕜] E)∥ :=
+pos_of_mul_pos_left (lt_of_lt_of_le zero_lt_one e.one_le_norm_mul_norm_symm) (norm_nonneg _)
 
 lemma subsingleton_or_norm_symm_pos : subsingleton E ∨ 0 < ∥(e.symm : F →L[𝕜] E)∥ :=
-(subsingleton_or_exists_ne (0 : E)).imp id (λ hE, e.norm_symm_pos hE)
+begin
+  rcases subsingleton_or_nontrivial E with _i|_i; resetI,
+  { left, apply_instance },
+  { right, exact e.norm_symm_pos }
+end
 
 lemma subsingleton_or_nnnorm_symm_pos : subsingleton E ∨ 0 < (nnnorm $ (e.symm : F →L[𝕜] E)) :=
 subsingleton_or_norm_symm_pos e
diff --git a/src/analysis/normed_space/units.lean b/src/analysis/normed_space/units.lean
index 876d05137391a..a74dd44616bfa 100644
--- a/src/analysis/normed_space/units.lean
+++ b/src/analysis/normed_space/units.lean
@@ -42,7 +42,7 @@ def one_sub (t : R) (h : ∥t∥ < 1) : units R :=
 def add (x : units R) (t : R) (h : ∥t∥ < ∥((x⁻¹:units R):R)∥⁻¹) : units R :=
 x * (units.one_sub (- (((x⁻¹:units R):R) * t))
 begin
-  rcases subsingleton_or_nonzero R with _i|_i; resetI,
+  rcases subsingleton_or_nontrivial R with _i|_i; resetI,
   { rw subsingleton.elim ((x⁻¹:units R):R) 0,
     have : (0:ℝ) < 1 := by norm_num,
     simpa, },
@@ -68,7 +68,7 @@ x.add ((y:R) - x) h
 /-- The group of units of a complete normed ring is an open subset of the ring. -/
 lemma is_open : is_open {x : R | is_unit x} :=
 begin
-  rcases subsingleton_or_nonzero R with _i|_i; resetI,
+  rcases subsingleton_or_nontrivial R with _i|_i; resetI,
   { exact is_open_discrete is_unit },
   { apply metric.is_open_iff.mpr,
     rintros x' ⟨x, h⟩,
diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean
index dcc5bb996194e..326144eafd06f 100644
--- a/src/data/complex/basic.lean
+++ b/src/data/complex/basic.lean
@@ -269,7 +269,7 @@ by rw [inv_def, ← mul_assoc, mul_conj, ← of_real_mul,
 
 noncomputable instance : field ℂ :=
 { inv := has_inv.inv,
-  zero_ne_one := mt (congr_arg re) zero_ne_one,
+  exists_pair_ne := ⟨0, 1, mt (congr_arg re) zero_ne_one⟩,
   mul_inv_cancel := @complex.mul_inv_cancel,
   inv_zero := complex.inv_zero,
   ..complex.comm_ring }
diff --git a/src/data/equiv/ring.lean b/src/data/equiv/ring.lean
index 395855db068b7..d19f6b4785407 100644
--- a/src/data/equiv/ring.lean
+++ b/src/data/equiv/ring.lean
@@ -239,7 +239,8 @@ protected lemma is_integral_domain {A : Type*} (B : Type*) [ring A] [ring B]
     have e x * e y = 0, by rw [← e.map_mul, hxy, e.map_zero],
     (hB.eq_zero_or_eq_zero_of_mul_eq_zero _ _ this).imp (λ hx, by simpa using congr_arg e.symm hx)
       (λ hy, by simpa using congr_arg e.symm hy),
-  zero_ne_one := λ H, hB.zero_ne_one $ by rw [← e.map_zero, ← e.map_one, H] }
+  exists_pair_ne := ⟨e.symm 0, e.symm 1,
+    by { haveI : nontrivial B := hB.to_nontrivial, exact e.symm.injective.ne zero_ne_one }⟩ }
 
 /-- If two rings are isomorphic, and the second is an integral domain, then so is the first. -/
 protected def integral_domain {A : Type*} (B : Type*) [ring A] [integral_domain B]
diff --git a/src/data/equiv/transfer_instance.lean b/src/data/equiv/transfer_instance.lean
index 3dc49f6664d80..b080a18a990ae 100644
--- a/src/data/equiv/transfer_instance.lean
+++ b/src/data/equiv/transfer_instance.lean
@@ -141,14 +141,14 @@ protected def comm_ring [comm_ring β] : comm_ring α :=
   ..equiv.ring e }
 
 /-- Transfer `nonzero` across an `equiv` -/
-protected theorem nonzero [has_zero β] [has_one β] [nonzero β] : @nonzero α e.has_zero e.has_one :=
-{ zero_ne_one := by simp [zero_def, one_def] }
+protected theorem nontrivial [nontrivial β] : nontrivial α :=
+let ⟨x, y, h⟩ := exists_pair_ne β in ⟨⟨e.symm x, e.symm y, e.symm.injective.ne h⟩⟩
 
 /-- Transfer `domain` across an `equiv` -/
 protected def domain [domain β] : domain α :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := by simp [mul_def, zero_def, equiv.eq_symm_apply],
-  zero_ne_one := by simp [zero_def, one_def],
-  ..equiv.ring e }
+  ..equiv.ring e,
+  ..equiv.nontrivial e }
 
 /-- Transfer `integral_domain` across an `equiv` -/
 protected def integral_domain [integral_domain β] : integral_domain α :=
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
index ebd61af3757b5..2e7941a1350a6 100644
--- a/src/data/fintype/basic.lean
+++ b/src/data/fintype/basic.lean
@@ -461,19 +461,26 @@ match n, hn with
     (λ _ _ _, h _ _))⟩
 end
 
+lemma fintype.card_le_one_iff_subsingleton [fintype α] :
+  fintype.card α ≤ 1 ↔ subsingleton α :=
+iff.trans fintype.card_le_one_iff subsingleton_iff.symm
+
+lemma fintype.one_lt_card_iff_nontrivial [fintype α] :
+  1 < fintype.card α ↔ nontrivial α :=
+begin
+  classical,
+  rw ← not_iff_not,
+  push_neg,
+  rw [not_nontrivial_iff_subsingleton, fintype.card_le_one_iff_subsingleton]
+end
+
 lemma fintype.exists_ne_of_one_lt_card [fintype α] (h : 1 < fintype.card α) (a : α) :
   ∃ b : α, b ≠ a :=
-let ⟨b, hb⟩ := classical.not_forall.1 (mt fintype.card_le_one_iff.2 (not_le_of_gt h)) in
-let ⟨c, hc⟩ := classical.not_forall.1 hb in
-by haveI := classical.dec_eq α; exact
-if hba : b = a then ⟨c, by cc⟩ else ⟨b, hba⟩
+by { haveI : nontrivial α := fintype.one_lt_card_iff_nontrivial.1 h, exact exists_ne a }
 
 lemma fintype.exists_pair_of_one_lt_card [fintype α] (h : 1 < fintype.card α) :
-  ∃ (a b : α), b ≠ a :=
-begin
-  rcases fintype.card_pos_iff.1 (nat.lt_of_succ_lt h) with a,
-  exact ⟨a, fintype.exists_ne_of_one_lt_card h a⟩,
-end
+  ∃ (a b : α), a ≠ b :=
+by { haveI : nontrivial α := fintype.one_lt_card_iff_nontrivial.1 h, exact exists_pair_ne α }
 
 lemma fintype.injective_iff_surjective [fintype α] {f : α → α} : injective f ↔ surjective f :=
 by haveI := classical.prop_decidable; exact
diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean
index 29afe70678663..356ac83b654fe 100644
--- a/src/data/int/basic.lean
+++ b/src/data/int/basic.lean
@@ -14,6 +14,11 @@ open nat
 
 namespace int
 
+instance : inhabited ℤ := ⟨int.zero⟩
+
+instance : nontrivial ℤ :=
+⟨⟨0, 1, int.zero_ne_one⟩⟩
+
 instance : comm_ring int :=
 { add            := int.add,
   add_assoc      := int.add_assoc,
@@ -47,17 +52,11 @@ instance : semiring int           := by apply_instance
 instance : ring int               := by apply_instance
 instance : distrib int            := by apply_instance
 
-instance : nonzero ℤ :=
-{ zero_ne_one := int.zero_ne_one }
-
-instance : inhabited ℤ := ⟨int.zero⟩
-
 instance : decidable_linear_ordered_comm_ring int :=
 { add_le_add_left := @int.add_le_add_left,
-  zero_ne_one     := int.zero_ne_one,
   mul_pos         := @int.mul_pos,
   zero_lt_one     := int.zero_lt_one,
-  ..int.comm_ring, ..int.decidable_linear_order }
+  .. int.comm_ring, .. int.decidable_linear_order, .. int.nontrivial }
 
 instance : decidable_linear_ordered_add_comm_group int :=
 by apply_instance
@@ -215,7 +214,8 @@ theorem nat_abs_neg_of_nat (n : ℕ) : nat_abs (neg_of_nat n) = n :=
 by cases n; refl
 
 theorem nat_abs_mul (a b : ℤ) : nat_abs (a * b) = (nat_abs a) * (nat_abs b) :=
-by cases a; cases b; simp only [(*), int.mul, nat_abs_neg_of_nat, eq_self_iff_true, int.nat_abs]
+by cases a; cases b;
+  simp only [← int.mul_def, int.mul, nat_abs_neg_of_nat, eq_self_iff_true, int.nat_abs]
 
 @[simp] lemma nat_abs_mul_self' (a : ℤ) : (nat_abs a * nat_abs a : ℤ) = a * a :=
 by rw [← int.coe_nat_mul, nat_abs_mul_self]
@@ -942,8 +942,8 @@ by cases m with m m; cases n with n n; unfold has_add.add;
   simp [int.add, -of_nat_eq_coe, bool.bxor_comm]
 
 @[simp] lemma bodd_mul (m n : ℤ) : bodd (m * n) = bodd m && bodd n :=
-by cases m with m m; cases n with n n; unfold has_mul.mul;
-  simp [int.mul, -of_nat_eq_coe, bool.bxor_comm]
+by cases m with m m; cases n with n n;
+  simp [← int.mul_def, int.mul, -of_nat_eq_coe, bool.bxor_comm]
 
 theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
 | (n : ℕ) :=
diff --git a/src/data/matrix/pequiv.lean b/src/data/matrix/pequiv.lean
index ccce1873d15d6..ef3c844971787 100644
--- a/src/data/matrix/pequiv.lean
+++ b/src/data/matrix/pequiv.lean
@@ -94,7 +94,7 @@ end
 @[simp] lemma to_matrix_bot [decidable_eq n] [has_zero α] [has_one α] :
   ((⊥ : pequiv m n).to_matrix : matrix m n α) = 0 := rfl
 
-lemma to_matrix_injective [decidable_eq n] [has_zero α] [has_one α] [nonzero α] :
+lemma to_matrix_injective [decidable_eq n] [monoid_with_zero α] [nontrivial α] :
   function.injective (@to_matrix m n _ _ α _ _ _) :=
 begin
   classical,
@@ -108,7 +108,7 @@ begin
   { cases hg : g i with gi,
     { cc },
     { use gi,
-      simp } },
+      simp, } },
   { use fi,
     simp [hf.symm, ne.symm hi] }
 end
diff --git a/src/data/mv_polynomial.lean b/src/data/mv_polynomial.lean
index 2ec2d19f41289..980c95946d830 100644
--- a/src/data/mv_polynomial.lean
+++ b/src/data/mv_polynomial.lean
@@ -845,7 +845,7 @@ by rw [← C_0]; exact total_degree_C (0 : α)
 @[simp] lemma total_degree_one : (1 : mv_polynomial σ α).total_degree = 0 :=
 total_degree_C (1 : α)
 
-@[simp] lemma total_degree_X {α} [comm_semiring α] [nonzero α] (s : σ) :
+@[simp] lemma total_degree_X {α} [comm_semiring α] [nontrivial α] (s : σ) :
   (X s : mv_polynomial σ α).total_degree = 1 :=
 begin
   rw [total_degree, X, monomial, finsupp.support_single_ne_zero (one_ne_zero : (1 : α) ≠ 0)],
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
index a8fc81c5d32e4..6c91c6982fe9d 100644
--- a/src/data/nat/basic.lean
+++ b/src/data/nat/basic.lean
@@ -21,8 +21,8 @@ universes u v
 
 attribute [protected] nat.pow_zero nat.pow_succ
 
-instance : nonzero ℕ :=
-{ zero_ne_one := nat.zero_ne_one }
+instance : nontrivial ℕ :=
+⟨⟨0, 1, nat.zero_ne_one⟩⟩
 
 instance : comm_semiring nat :=
 { add            := nat.add,
@@ -76,10 +76,10 @@ instance : canonically_ordered_comm_semiring ℕ :=
 { le_iff_exists_add := assume a b,
   ⟨assume h, let ⟨c, hc⟩ := nat.le.dest h in ⟨c, hc.symm⟩,
     assume ⟨c, hc⟩, hc.symm ▸ nat.le_add_right _ _⟩,
-  zero_ne_one       := ne_of_lt zero_lt_one,
   eq_zero_or_eq_zero_of_mul_eq_zero   := assume a b, nat.eq_zero_of_mul_eq_zero,
   bot               := 0,
   bot_le            := nat.zero_le,
+  .. nat.nontrivial,
   .. (infer_instance : ordered_add_comm_monoid ℕ),
   .. (infer_instance : linear_ordered_semiring ℕ),
   .. (infer_instance : comm_semiring ℕ) }
diff --git a/src/data/num/lemmas.lean b/src/data/num/lemmas.lean
index 8b9b6961a75ee..63d786ded8c4d 100644
--- a/src/data/num/lemmas.lean
+++ b/src/data/num/lemmas.lean
@@ -1027,7 +1027,7 @@ instance : decidable_linear_ordered_comm_ring znum :=
   left_distrib     := by {transfer, simp [mul_add]},
   right_distrib    := by {transfer, simp [mul_add, mul_comm]},
   mul_comm         := by transfer,
-  zero_ne_one      := dec_trivial,
+  exists_pair_ne   := ⟨0, 1, dec_trivial⟩,
   add_le_add_left  := by {intros a b h c, revert h, transfer_rw, exact λ h, add_le_add_left h c},
   mul_pos          := λ a b, show 0 < a → 0 < b → 0 < a * b, by {transfer_rw, apply mul_pos},
   zero_lt_one      := dec_trivial,
diff --git a/src/data/padics/padic_integers.lean b/src/data/padics/padic_integers.lean
index 6bd2c4debc09e..732dbeebd41b5 100644
--- a/src/data/padics/padic_integers.lean
+++ b/src/data/padics/padic_integers.lean
@@ -165,7 +165,7 @@ have a * b = 0, from subtype.ext_iff_val.1 h,
 
 instance : integral_domain ℤ_[p] :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := padic_int.eq_zero_or_eq_zero_of_mul_eq_zero,
-  zero_ne_one := padic_int.zero_ne_one,
+  exists_pair_ne := ⟨0, 1, padic_int.zero_ne_one⟩,
   ..padic_int.comm_ring }
 
 end instances
@@ -232,7 +232,7 @@ local attribute [reducible] padic_int
 lemma mul_inv : ∀ {z : ℤ_[p]}, ∥z∥ = 1 → z * z.inv = 1
 | ⟨k, _⟩ h :=
   begin
-    have hk : k ≠ 0, from λ h', @zero_ne_one ℚ_[p] _ _ _ (by simpa [h'] using h),
+    have hk : k ≠ 0, from λ h', @zero_ne_one ℚ_[p] _ _ (by simpa [h'] using h),
     unfold padic_int.inv, split_ifs,
     { change (⟨k * (1/k), _⟩ : ℤ_[p]) = 1,
       simp [hk], refl },
diff --git a/src/data/polynomial.lean b/src/data/polynomial.lean
index a574675ee1ce0..6310898b112da 100644
--- a/src/data/polynomial.lean
+++ b/src/data/polynomial.lean
@@ -1016,7 +1016,7 @@ lemma monic.ne_zero_of_zero_ne_one (h : (0:R) ≠ 1) {p : polynomial R} (hp : p.
   p ≠ 0 :=
 by { contrapose! h, rwa [h] at hp }
 
-lemma monic.ne_zero {R : Type*} [semiring R] [nonzero R] {p : polynomial R} (hp : p.monic) :
+lemma monic.ne_zero {R : Type*} [semiring R] [nontrivial R] {p : polynomial R} (hp : p.monic) :
   p ≠ 0 :=
 hp.ne_zero_of_zero_ne_one zero_ne_one
 
@@ -1501,13 +1501,13 @@ have zn0 : (0 : R) ≠ 1, from λ h, by haveI := subsingleton_of_zero_eq_one h;
 end comm_semiring
 
 section nonzero_semiring
-variables [semiring R] [nonzero R] {p q : polynomial R}
+variables [semiring R] [nontrivial R] {p q : polynomial R}
 
-instance : nonzero (polynomial R) :=
-{ zero_ne_one := λ (h : (0 : polynomial R) = 1), zero_ne_one $
+instance : nontrivial (polynomial R) :=
+⟨⟨0, 1, λ (h : (0 : polynomial R) = 1), zero_ne_one $
     calc (0 : R) = eval 0 0 : eval_zero.symm
       ... = eval 0 1 : congr_arg _ h
-      ... = 1 : eval_C }
+      ... = 1 : eval_C⟩⟩
 
 @[simp] lemma degree_one : degree (1 : polynomial R) = (0 : with_bot ℕ) :=
 degree_C (show (1 : R) ≠ 0, from zero_ne_one.symm)
@@ -1540,7 +1540,7 @@ lemma ne_zero_of_monic (h : monic p) : p ≠ 0 :=
 λ h₁, @not_monic_zero R _ _ (h₁ ▸ h)
 
 theorem not_is_unit_X : ¬ is_unit (X : polynomial R) :=
-λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ _ $ by erw [← coeff_one_zero, ← hgf, coeff_mul_X_zero]
+λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $ by erw [← coeff_one_zero, ← hgf, coeff_mul_X_zero]
 
 end nonzero_semiring
 
@@ -1582,9 +1582,9 @@ lemma div_X_eq_zero_iff : div_X p = 0 ↔ p = C (p.coeff 0) :=
 lemma div_X_add : div_X (p + q) = div_X p + div_X q :=
 ext $ by simp [div_X]
 
-theorem nonzero.of_polynomial_ne (h : p ≠ q) : nonzero R :=
-{ zero_ne_one := λ h01 : 0 = 1, h $
-    by rw [← mul_one p, ← mul_one q, ← C_1, ← h01, C_0, mul_zero, mul_zero] }
+theorem nonzero.of_polynomial_ne (h : p ≠ q) : nontrivial R :=
+⟨⟨0, 1, λ h01 : 0 = 1, h $
+    by rw [← mul_one p, ← mul_one q, ← C_1, ← h01, C_0, mul_zero, mul_zero] ⟩⟩
 
 lemma degree_lt_degree_mul_X (hp : p ≠ 0) : p.degree < (p * X).degree :=
 by haveI := nonzero.of_polynomial_ne hp; exact
@@ -2121,7 +2121,7 @@ begin
   { haveI := subsingleton_of_zero_eq_one h01,
     rw [subsingleton.elim (f /ₘ g) 0, subsingleton.elim f 0, subsingleton.elim g 0,
         nat_degree_zero] },
-  haveI : nonzero R := ⟨h01⟩,
+  haveI : nontrivial R := ⟨⟨0, 1, h01⟩⟩,
   by_cases hfg : f /ₘ g = 0,
   { rw [hfg, nat_degree_zero], rw div_by_monic_eq_zero_iff hg hg.ne_zero at hfg,
     rw nat.sub_eq_zero_of_le (nat_degree_le_nat_degree $ le_of_lt hfg) },
@@ -2230,7 +2230,7 @@ by rw [is_root.def, eval_sub, eval_X, eval_C, sub_eq_zero_iff_eq, eq_comm]
 end comm_ring
 
 section nonzero_ring
-variables [ring R] [nonzero R] {p q : polynomial R}
+variables [ring R] [nontrivial R] {p q : polynomial R}
 
 @[simp] lemma degree_X_sub_C (a : R) : degree (X - C a) = 1 :=
 begin
@@ -2305,10 +2305,10 @@ end
 end ring
 
 section nonzero_ring
-variables [ring R] [nonzero R]
+variables [ring R] [nontrivial R]
 
 theorem not_is_unit_X_sub_C {r : R} : ¬ is_unit (X - C r) :=
-λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ _ $ by erw [← eval_mul_X_sub_C, hgf, eval_one]
+λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $ by erw [← eval_mul_X_sub_C, hgf, eval_one]
 
 end nonzero_ring
 
@@ -2320,7 +2320,7 @@ variables [comm_ring R] {p q : polynomial R}
   p %ₘ (X - C a) = C (p.eval a) :=
 if h0 : (0 : R) = 1 then by letI := subsingleton_of_zero_eq_one h0; exact subsingleton.elim _ _
 else
-by letI : nonzero R := nonzero.of_ne h0; exact
+by haveI : nontrivial R := nontrivial_of_ne 0 1 h0; exact
 have h : (p %ₘ (X - C a)).eval a = p.eval a :=
   by rw [mod_by_monic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul,
     eval_sub, eval_X, eval_C, sub_self, zero_mul, sub_zero],
@@ -2364,7 +2364,7 @@ lemma multiplicity_X_sub_C_finite (a : R) (h0 : p ≠ 0) :
 multiplicity_finite_of_degree_pos_of_monic
   (have (0 : R) ≠ 1, from (λ h, by haveI := subsingleton_of_zero_eq_one h;
       exact h0 (subsingleton.elim _ _)),
-    by haveI : nonzero R := ⟨this⟩; rw degree_X_sub_C; exact dec_trivial)
+    by haveI : nontrivial R := ⟨⟨0, 1, this⟩⟩; rw degree_X_sub_C; exact dec_trivial)
     (monic_X_sub_C _) h0
 
 def root_multiplicity (a : R) (p : polynomial R) : ℕ :=
@@ -2399,7 +2399,7 @@ lemma eval_div_by_monic_pow_root_multiplicity_ne_zero
   {p : polynomial R} (a : R) (hp : p ≠ 0) :
   (p /ₘ ((X - C a) ^ root_multiplicity a p)).eval a ≠ 0 :=
 begin
-  haveI : nonzero R := nonzero.of_polynomial_ne hp,
+  haveI : nontrivial R := nonzero.of_polynomial_ne hp,
   rw [ne.def, ← is_root.def, ← dvd_iff_is_root],
   rintros ⟨q, hq⟩,
   have := div_by_monic_mul_pow_root_multiplicity_eq p a,
@@ -2453,7 +2453,7 @@ instance : integral_domain (polynomial R) :=
     erw [← leading_coeff_eq_zero, ← leading_coeff_eq_zero],
     exact eq_zero_or_eq_zero_of_mul_eq_zero this
   end,
-  ..polynomial.nonzero,
+  ..polynomial.nontrivial,
   ..polynomial.comm_ring }
 
 lemma nat_degree_mul_eq (hp : p ≠ 0) (hq : q ≠ 0) : nat_degree (p * q) =
@@ -2794,7 +2794,7 @@ instance : euclidean_domain (polynomial R) :=
   remainder_lt := λ p q hq, remainder_lt_aux _ hq,
   mul_left_not_lt := λ p q hq, not_lt_of_ge (degree_le_mul_left _ hq),
   .. polynomial.comm_ring,
-  .. polynomial.nonzero }
+  .. polynomial.nontrivial }
 
 lemma mod_eq_self_iff (hq0 : q ≠ 0) : p % q = p ↔ degree p < degree q :=
 ⟨λ h, h ▸ euclidean_domain.mod_lt _ hq0,
diff --git a/src/data/rat/basic.lean b/src/data/rat/basic.lean
index 09f300e32212e..56dee36228966 100644
--- a/src/data/rat/basic.lean
+++ b/src/data/rat/basic.lean
@@ -427,7 +427,7 @@ instance : field ℚ :=
   mul_assoc        := rat.mul_assoc,
   left_distrib     := rat.mul_add,
   right_distrib    := rat.add_mul,
-  zero_ne_one      := rat.zero_ne_one,
+  exists_pair_ne   := ⟨0, 1, rat.zero_ne_one⟩,
   mul_inv_cancel   := rat.mul_inv_cancel,
   inv_zero         := rfl }
 
@@ -436,7 +436,7 @@ instance : division_ring ℚ      := by apply_instance
 instance : integral_domain ℚ    := by apply_instance
 -- TODO(Mario): this instance slows down data.real.basic
 --instance : domain ℚ           := by apply_instance
-instance : nonzero ℚ            := by apply_instance
+instance : nontrivial ℚ         := by apply_instance
 instance : comm_ring ℚ          := by apply_instance
 --instance : ring ℚ             := by apply_instance
 instance : comm_semiring ℚ      := by apply_instance
diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
index 1d7d5ea697ef4..4bdbab4cea005 100644
--- a/src/data/real/basic.lean
+++ b/src/data/real/basic.lean
@@ -104,10 +104,10 @@ quotient.induction_on₂ a b $ λ f g,
 instance : linear_ordered_comm_ring ℝ :=
 { add_le_add_left := λ a b h c,
     (le_iff_le_iff_lt_iff_lt.2 $ real.add_lt_add_iff_left c).2 h,
-  zero_ne_one := ne_of_lt real.zero_lt_one,
-  mul_pos := @real.mul_pos,
+  exists_pair_ne  := ⟨0, 1, ne_of_lt real.zero_lt_one⟩,
+  mul_pos     := @real.mul_pos,
   zero_lt_one := real.zero_lt_one,
-  ..real.comm_ring, ..real.linear_order, ..real.semiring }
+  .. real.comm_ring, .. real.linear_order, .. real.semiring }
 
 /- Extra instances to short-circuit type class resolution -/
 instance : linear_ordered_ring ℝ        := by apply_instance
@@ -141,7 +141,7 @@ noncomputable instance : decidable_linear_ordered_add_comm_group ℝ := by apply
 noncomputable instance field : field ℝ := by apply_instance
 noncomputable instance : division_ring ℝ           := by apply_instance
 noncomputable instance : integral_domain ℝ         := by apply_instance
-instance : nonzero ℝ                               := by apply_instance
+instance : nontrivial ℝ                            := by apply_instance
 noncomputable instance : decidable_linear_order ℝ  := by apply_instance
 noncomputable instance : distrib_lattice ℝ := by apply_instance
 noncomputable instance : lattice ℝ         := by apply_instance
diff --git a/src/data/real/cau_seq_completion.lean b/src/data/real/cau_seq_completion.lean
index 261878e6567bc..4165fb9e24ce7 100644
--- a/src/data/real/cau_seq_completion.lean
+++ b/src/data/real/cau_seq_completion.lean
@@ -129,7 +129,7 @@ end
 noncomputable def field : field Cauchy :=
 { inv              := has_inv.inv,
   mul_inv_cancel   := λ x x0, by rw [mul_comm, cau_seq.completion.inv_mul_cancel x0],
-  zero_ne_one      := zero_ne_one,
+  exists_pair_ne   := ⟨0, 1, zero_ne_one⟩,
   inv_zero         := inv_zero,
   ..cau_seq.completion.comm_ring }
 
diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
index d1af104f652b4..90da56c94e561 100644
--- a/src/data/real/nnreal.lean
+++ b/src/data/real/nnreal.lean
@@ -93,7 +93,7 @@ def to_real_hom : ℝ≥0 →+* ℝ :=
 @[simp] lemma coe_to_real_hom : ⇑to_real_hom = coe := rfl
 
 instance : comm_group_with_zero ℝ≥0 :=
-{ zero_ne_one    := assume h, zero_ne_one $ nnreal.eq_iff.2 h,
+{ exists_pair_ne := ⟨0, 1, assume h, zero_ne_one $ nnreal.eq_iff.2 h⟩,
   inv_zero       := nnreal.eq $ show (0⁻¹ : ℝ) = 0, from inv_zero,
   mul_inv_cancel := assume x h, nnreal.eq $ mul_inv_cancel $ ne_iff.2 h,
   .. (by apply_instance : has_inv ℝ≥0),
@@ -198,11 +198,10 @@ instance : linear_ordered_comm_group_with_zero ℝ≥0 :=
   .. nnreal.comm_group_with_zero }
 
 instance : canonically_ordered_comm_semiring ℝ≥0 :=
-{ .. nnreal.linear_ordered_semiring,
-  .. nnreal.canonically_ordered_add_monoid,
+{ .. nnreal.canonically_ordered_add_monoid,
   .. nnreal.comm_semiring,
   .. (show no_zero_divisors ℝ≥0, by apply_instance),
-  .. (show nonzero ℝ≥0, by apply_instance) }
+  .. nnreal.comm_group_with_zero }
 
 instance : densely_ordered ℝ≥0 :=
 ⟨assume a b (h : (a : ℝ) < b), let ⟨c, hac, hcb⟩ := dense h in
diff --git a/src/data/zmod/basic.lean b/src/data/zmod/basic.lean
index 0caee568d90ea..2d4587244c198 100644
--- a/src/data/zmod/basic.lean
+++ b/src/data/zmod/basic.lean
@@ -429,11 +429,11 @@ begin
   { apply fin.val_mul }
 end
 
-instance nonzero (n : ℕ) [fact (1 < n)] : nonzero (zmod n) :=
-{ zero_ne_one := assume h, zero_ne_one $
+instance nontrivial (n : ℕ) [fact (1 < n)] : nontrivial (zmod n) :=
+⟨⟨0, 1, assume h, zero_ne_one $
    calc 0 = (0 : zmod n).val : by rw val_zero
       ... = (1 : zmod n).val : congr_arg zmod.val h
-      ... = 1                : val_one n }
+      ... = 1                : val_one n ⟩⟩
 
 /-- The inversion on `zmod n`.
 It is setup in such a way that `a * a⁻¹` is equal to `gcd a.val n`.
@@ -754,8 +754,8 @@ instance : field (zmod p) :=
 { mul_inv_cancel := mul_inv_cancel_aux p,
   inv_zero := inv_zero p,
   .. zmod.comm_ring p,
-  .. zmod.nonzero p,
-  .. zmod.has_inv p }
+  .. zmod.has_inv p,
+  .. zmod.nontrivial p }
 
 end zmod
 
diff --git a/src/data/zsqrtd/basic.lean b/src/data/zsqrtd/basic.lean
index cb03058e8ca4b..97889da3a0437 100644
--- a/src/data/zsqrtd/basic.lean
+++ b/src/data/zsqrtd/basic.lean
@@ -115,8 +115,8 @@ instance : semiring ℤ√d           := by apply_instance
 instance : ring ℤ√d               := by apply_instance
 instance : distrib ℤ√d            := by apply_instance
 
-instance : nonzero ℤ√d :=
-{ zero_ne_one := dec_trivial }
+instance : nontrivial ℤ√d :=
+⟨⟨0, 1, dec_trivial⟩⟩
 
 @[simp] theorem coe_nat_re (n : ℕ) : (n : ℤ√d).re = n :=
 by induction n; simp *
@@ -153,8 +153,8 @@ by simp [ext]
 theorem mul_conj {x y : ℤ} : (⟨x, y⟩ * conj ⟨x, y⟩ : ℤ√d) = x * x - d * y * y :=
 by simp [ext, sub_eq_add_neg, mul_comm]
 
-theorem conj_mul : Π {a b : ℤ√d}, conj (a * b) = conj a * conj b :=
-by simp [ext, add_comm]
+theorem conj_mul {a b : ℤ√d} : conj (a * b) = conj a * conj b :=
+by { simp [ext], ring }
 
 protected lemma coe_int_add (m n : ℤ) : (↑(m + n) : ℤ√d) = ↑m + ↑n := by simp [ext]
 protected lemma coe_int_sub (m n : ℤ) : (↑(m - n) : ℤ√d) = ↑m - ↑n := by simp [ext, sub_eq_add_neg]
@@ -551,9 +551,8 @@ protected theorem eq_zero_or_eq_zero_of_mul_eq_zero : Π {a b : ℤ√d}, a * b
              ... = d * y * y * z : by simp [h2, mul_assoc, mul_left_comm]
 
 instance : integral_domain ℤ√d :=
-{ zero_ne_one := zero_ne_one,
-  eq_zero_or_eq_zero_of_mul_eq_zero := @zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero,
-  ..zsqrtd.comm_ring }
+{ eq_zero_or_eq_zero_of_mul_eq_zero := @zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero,
+  .. zsqrtd.comm_ring, .. zsqrtd.nontrivial }
 
 protected theorem mul_pos (a b : ℤ√d) (a0 : 0 < a) (b0 : 0 < b) : 0 < a * b := λab,
 or.elim (eq_zero_or_eq_zero_of_mul_eq_zero
@@ -563,10 +562,9 @@ or.elim (eq_zero_or_eq_zero_of_mul_eq_zero
 
 instance : decidable_linear_ordered_comm_ring ℤ√d :=
 { add_le_add_left := @zsqrtd.add_le_add_left,
-  zero_ne_one     := zero_ne_one,
   mul_pos         := @zsqrtd.mul_pos,
   zero_lt_one     := dec_trivial,
-  ..zsqrtd.comm_ring, ..zsqrtd.decidable_linear_order }
+  .. zsqrtd.comm_ring, .. zsqrtd.decidable_linear_order, .. zsqrtd.nontrivial }
 
 instance : decidable_linear_ordered_semiring ℤ√d := by apply_instance
 instance : linear_ordered_semiring ℤ√d           := by apply_instance
diff --git a/src/data/zsqrtd/gaussian_int.lean b/src/data/zsqrtd/gaussian_int.lean
index d2c88327f3d89..38ff9fb627202 100644
--- a/src/data/zsqrtd/gaussian_int.lean
+++ b/src/data/zsqrtd/gaussian_int.lean
@@ -180,8 +180,8 @@ by rw [norm_mul, int.nat_abs_mul];
   exact le_mul_of_one_le_right' (nat.zero_le _)
     (int.coe_nat_le.1 (by rw [coe_nat_abs_norm]; exact norm_pos.2 hy))
 
-instance : nonzero ℤ[i] :=
-{ zero_ne_one := dec_trivial }
+instance : nontrivial ℤ[i] :=
+⟨⟨0, 1, dec_trivial⟩⟩
 
 instance : euclidean_domain ℤ[i] :=
 { quotient := (/),
@@ -193,7 +193,7 @@ instance : euclidean_domain ℤ[i] :=
   remainder_lt := nat_abs_norm_mod_lt,
   mul_left_not_lt := λ a b hb0, not_lt_of_ge $ norm_le_norm_mul_left a hb0,
   .. gaussian_int.comm_ring,
-  .. gaussian_int.nonzero }
+  .. gaussian_int.nontrivial }
 
 open principal_ideal_ring
 
diff --git a/src/field_theory/perfect_closure.lean b/src/field_theory/perfect_closure.lean
index 959ef695c52c7..65e1839e7a932 100644
--- a/src/field_theory/perfect_closure.lean
+++ b/src/field_theory/perfect_closure.lean
@@ -351,7 +351,7 @@ instance : has_inv (perfect_closure K p) :=
 end)⟩
 
 instance : field (perfect_closure K p) :=
-{ zero_ne_one := λ H, zero_ne_one ((eq_iff _ _ _ _).1 H),
+{ exists_pair_ne := ⟨0, 1, λ H, zero_ne_one ((eq_iff _ _ _ _).1 H)⟩,
   mul_inv_cancel := λ e, induction_on e $ λ ⟨m, x⟩ H,
     have _ := mt (eq_iff _ _ _ _).2 H, (eq_iff _ _ _ _).2
       (by simp only [(frobenius _ _).iterate_map_one, (frobenius K p).iterate_map_zero,
diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean
index 4473e53c00260..9c83fa7561b6d 100644
--- a/src/field_theory/subfield.lean
+++ b/src/field_theory/subfield.lean
@@ -15,7 +15,7 @@ end prio
 
 instance is_subfield.field [is_subfield S] : field S :=
 { inv := λ x, ⟨x⁻¹, is_subfield.inv_mem x.2⟩,
-  zero_ne_one := λ h, zero_ne_one (subtype.ext_iff_val.1 h),
+  exists_pair_ne := ⟨0, 1, λ h, zero_ne_one (subtype.ext_iff_val.1 h)⟩,
   mul_inv_cancel := λ a ha, subtype.ext_iff_val.2 (mul_inv_cancel
     (λ h, ha $ subtype.ext_iff_val.2 h)),
   inv_zero := subtype.ext_iff_val.2 inv_zero,
diff --git a/src/group_theory/free_abelian_group.lean b/src/group_theory/free_abelian_group.lean
index fd3e611da55ed..8d60533fae415 100644
--- a/src/group_theory/free_abelian_group.lean
+++ b/src/group_theory/free_abelian_group.lean
@@ -262,6 +262,9 @@ instance [monoid α] : semigroup (free_abelian_group α) :=
       exact (lift.add _ _ _).symm }
   end }
 
+lemma mul_def [monoid α] (x y : free_abelian_group α) :
+  x * y = lift (λ x₂, lift (λ x₁, of (x₁ * x₂)) x) y := rfl
+
 instance [monoid α] : ring (free_abelian_group α) :=
 { one := free_abelian_group.of 1,
   mul_one := λ x, begin
diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean
index 13d225ef380d0..58d12231e7140 100644
--- a/src/linear_algebra/dimension.lean
+++ b/src/linear_algebra/dimension.lean
@@ -5,6 +5,7 @@ Author: Mario Carneiro, Johannes Hölzl, Sander Dahmen
 -/
 import linear_algebra.basis
 import set_theory.ordinal
+
 /-!
 # Dimension of modules and vector spaces
 
@@ -48,7 +49,7 @@ variables {K V}
 open vector_space
 
 section
-theorem is_basis.le_span (zero_ne_one : (0 : K) ≠ 1) {v : ι → V} {J : set V} (hv : is_basis K v)
+theorem is_basis.le_span {v : ι → V} {J : set V} (hv : is_basis K v)
    (hJ : span K J = ⊤) : cardinal.mk (range v) ≤ cardinal.mk J :=
 begin
   cases le_or_lt cardinal.omega (cardinal.mk J) with oJ oJ,
@@ -63,10 +64,11 @@ begin
       rw hJ at this,
       replace : hv.repr (v i) ∈ (finsupp.supported K K (⋃ j, S j)) := this trivial,
       rw [hv.repr_eq_single, finsupp.mem_supported,
-        finsupp.support_single_ne_zero zero_ne_one.symm] at this,
-      subst b,
-      rcases mem_Union.1 (this (finset.mem_singleton_self _)) with ⟨j, hj⟩,
-      exact mem_Union.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩ },
+        finsupp.support_single_ne_zero one_ne_zero] at this,
+      { subst b,
+        rcases mem_Union.1 (this (finset.mem_singleton_self _)) with ⟨j, hj⟩,
+        exact mem_Union.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩ },
+      { apply_instance } },
     refine le_of_not_lt (λ IJ, _),
     suffices : cardinal.mk (⋃ j, S' j) < cardinal.mk (range v),
     { exact not_le_of_lt this ⟨set.embedding_of_subset _ _ hs⟩ },
@@ -90,12 +92,12 @@ begin
   rw ←cardinal.lift_inj.{(max w w') u'},
   rw [cardinal.lift_lift, cardinal.lift_lift],
   apply le_antisymm,
-  { convert cardinal.lift_le.{u' (max w w')}.2 (hv.le_span zero_ne_one hv'.2),
+  { convert cardinal.lift_le.{u' (max w w')}.2 (hv.le_span hv'.2),
     { rw cardinal.lift_max.{w u' w'},
       apply (cardinal.mk_range_eq_of_injective (hv.injective zero_ne_one)).symm, },
     { rw cardinal.lift_max.{w' u' w},
       apply (cardinal.mk_range_eq_of_injective (hv'.injective zero_ne_one)).symm, }, },
-  { convert cardinal.lift_le.{u' (max w w')}.2 (hv'.le_span zero_ne_one hv.2),
+  { convert cardinal.lift_le.{u' (max w w')}.2 (hv'.le_span hv.2),
     { rw cardinal.lift_max.{w' u' w},
       apply (cardinal.mk_range_eq_of_injective (hv'.injective zero_ne_one)).symm, },
     { rw cardinal.lift_max.{w u' w'},
@@ -356,9 +358,9 @@ begin
   exact (h $ bot_unique $ assume s hs, (submodule.mem_bot K).2 $ this s hs)
 end
 
-lemma exists_mem_ne_zero_of_dim_pos {s : submodule K V} (h : vector_space.dim K s > 0) :
+lemma exists_mem_ne_zero_of_dim_pos {s : submodule K V} (h : 0 < vector_space.dim K s) :
   ∃ b : V, b ∈ s ∧ b ≠ 0 :=
-exists_mem_ne_zero_of_ne_bot $ assume eq, by rw [(>), eq, dim_bot] at h; exact lt_irrefl _ h
+exists_mem_ne_zero_of_ne_bot $ assume eq, by rw [eq, dim_bot] at h; exact lt_irrefl _ h
 
 lemma exists_is_basis_fintype (h : dim K V < cardinal.omega) :
   ∃ s : (set V), (is_basis K (subtype.val : s → V)) ∧ nonempty (fintype s) :=
@@ -426,12 +428,23 @@ begin
     rw [←dim_top, this, dim_bot] }
 end
 
-lemma dim_pos_iff_exists_ne_zero : 0 < vector_space.dim K V  ↔ ∃ x : V, x ≠ 0 :=
+lemma dim_pos_iff_exists_ne_zero : 0 < vector_space.dim K V ↔ ∃ x : V, x ≠ 0 :=
 begin
   rw ←not_iff_not,
   simpa using dim_zero_iff_forall_zero
 end
 
+lemma dim_pos_iff_nontrivial : 0 < vector_space.dim K V ↔ nontrivial V :=
+begin
+  rw dim_pos_iff_exists_ne_zero,
+  split,
+  { rintros ⟨x, h⟩, exact ⟨⟨x, 0, h⟩⟩ },
+  { introsI, exact exists_ne 0 }
+end
+
+lemma dim_pos [h : nontrivial V] : 0 < vector_space.dim K V :=
+dim_pos_iff_nontrivial.2 h
+
 end vector_space
 
 section unconstrained_universes
diff --git a/src/logic/nontrivial.lean b/src/logic/nontrivial.lean
new file mode 100644
index 0000000000000..b9ea8448bea6e
--- /dev/null
+++ b/src/logic/nontrivial.lean
@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+
+import logic.unique
+import logic.function.basic
+import tactic.localized
+import tactic.push_neg
+
+/-!
+# Nontrivial types
+
+A type is *nontrivial* if it contains at least two elements. This is useful in particular for rings
+(where it is equivalent to the fact that zero is different from one) and for vector spaces
+(where it is equivalent to the fact that the dimension is positive).
+
+We introduce a typeclass `nontrivial` formalizing this property.
+-/
+
+variables {α : Type*} {β : Type*}
+
+open_locale classical
+
+/-- Predicate typeclass for expressing that a type is not reduced to a single element. In rings,
+this is equivalent to `0 ≠ 1`. In vector spaces, this is equivalent to positive dimension. -/
+class nontrivial (α : Type*) : Prop :=
+(exists_pair_ne : ∃ (x y : α), x ≠ y)
+
+lemma nontrivial_iff : nontrivial α ↔ ∃ (x y : α), x ≠ y :=
+⟨λ h, h.exists_pair_ne, λ h, ⟨h⟩⟩
+
+lemma exists_pair_ne (α : Type*) [nontrivial α] : ∃ (x y : α), x ≠ y :=
+nontrivial.exists_pair_ne
+
+lemma exists_ne [nontrivial α] (x : α) : ∃ y, y ≠ x :=
+begin
+  rcases exists_pair_ne α with ⟨y, y', h⟩,
+  by_cases hx : x = y,
+  { rw ← hx at h,
+    exact ⟨y', h.symm⟩ },
+  { exact ⟨y, ne.symm hx⟩ }
+end
+
+lemma nontrivial_of_ne (x y : α) (h : x ≠ y) : nontrivial α :=
+⟨⟨x, y, h⟩⟩
+
+section prio
+set_option default_priority 100 -- see Note [default priority]
+
+instance nontrivial.to_nonempty [nontrivial α] : nonempty α :=
+let ⟨x, _⟩ := exists_pair_ne α in ⟨x⟩
+
+end prio
+
+/-- An inhabited type is either nontrivial, or has a unique element. -/
+noncomputable def nontrivial_psum_unique (α : Type*) [inhabited α] :
+  psum (nontrivial α) (unique α) :=
+if h : nontrivial α then psum.inl h else psum.inr
+{ default := default α,
+  uniq := λ (x : α),
+  begin
+    change x = default α,
+    contrapose! h,
+    use [x, default α]
+  end }
+
+lemma subsingleton_iff : subsingleton α ↔ ∀ (x y : α), x = y :=
+⟨by { introsI h, exact subsingleton.elim }, λ h, ⟨h⟩⟩
+
+lemma not_nontrivial_iff_subsingleton : ¬(nontrivial α) ↔ subsingleton α :=
+by { rw [nontrivial_iff, subsingleton_iff], push_neg, refl }
+
+/-- A type is either a subsingleton or nontrivial. -/
+lemma subsingleton_or_nontrivial (α : Type*) :  subsingleton α ∨ nontrivial α :=
+by { rw [← not_nontrivial_iff_subsingleton, or_comm], exact classical.em _ }
+
+instance nontrivial_prod_left [nontrivial α] [nonempty β] : nontrivial (α × β) :=
+begin
+  inhabit β,
+  rcases exists_pair_ne α with ⟨x, y, h⟩,
+  use [(x, default β), (y, default β)],
+  contrapose! h,
+  exact congr_arg prod.fst h
+end
+
+instance nontrivial_prod_right [nontrivial α] [nonempty β] : nontrivial (β × α) :=
+begin
+  inhabit β,
+  rcases exists_pair_ne α with ⟨x, y, h⟩,
+  use [(default β, x), (default β, y)],
+  contrapose! h,
+  exact congr_arg prod.snd h
+end
+
+instance option.nontrivial [nonempty α] : nontrivial (option α) :=
+by { inhabit α, use [none, some (default α)] }
+
+/-- Pushforward a `nontrivial` instance along an injective function. -/
+protected lemma function.injective.nontrivial [nontrivial α]
+  {f : α → β} (hf : function.injective f) : nontrivial β :=
+let ⟨x, y, h⟩ := exists_pair_ne α in ⟨⟨f x, f y, hf.ne h⟩⟩
diff --git a/src/number_theory/lucas_lehmer.lean b/src/number_theory/lucas_lehmer.lean
index c65c02d98a1b0..5dfd6749a4ff3 100644
--- a/src/number_theory/lucas_lehmer.lean
+++ b/src/number_theory/lucas_lehmer.lean
@@ -222,8 +222,8 @@ instance : comm_ring (X q) :=
 { mul_comm := λ x y, by { ext; { dsimp, ring }, },
   ..(infer_instance : ring (X q))}
 
-instance [fact (1 < (q : ℕ))] : nonzero (X q) :=
-{ zero_ne_one := λ h, begin injection h with h1 _, exact zero_ne_one h1, end, }
+instance [fact (1 < (q : ℕ))] : nontrivial (X q) :=
+⟨⟨0, 1, λ h, by { injection h with h1 _, exact zero_ne_one h1 } ⟩⟩
 
 @[simp]
 lemma nat_coe_fst (n : ℕ) : (n : X q).fst = (n : zmod q) :=
diff --git a/src/number_theory/quadratic_reciprocity.lean b/src/number_theory/quadratic_reciprocity.lean
index c13a273ef01dd..840064de3ad8d 100644
--- a/src/number_theory/quadratic_reciprocity.lean
+++ b/src/number_theory/quadratic_reciprocity.lean
@@ -306,10 +306,13 @@ else
           ... ≤ _ : nat.div_mul_div_le_div _ _ _)
   ... = _ : by rw [← card_sigma];
     exact card_congr (λ a _, ⟨a.1, a.2⟩)
-      (by simp {contextual := tt})
-      (λ ⟨_, _⟩ ⟨_, _⟩, by simp {contextual := tt})
+      (by simp only [mem_filter, mem_sigma, and_self, forall_true_iff, mem_product]
+        {contextual := tt})
+      (λ ⟨_, _⟩ ⟨_, _⟩, by simp only [prod.mk.inj_iff, eq_self_iff_true, and_self, heq_iff_eq,
+        forall_true_iff] {contextual := tt})
       (λ ⟨b₁, b₂⟩ h, ⟨⟨b₁, b₂⟩,
-        by revert h; simp {contextual := tt}⟩)
+        by revert h; simp only [mem_filter, eq_self_iff_true, exists_prop_of_true, mem_sigma,
+          and_self, forall_true_iff, mem_product] {contextual := tt}⟩)
 
 /-- Each of the sums in this lemma is the cardinality of the set integer points in each of the
   two triangles formed by the diagonal of the rectangle `(0, p/2) × (0, q/2)`. Adding them
@@ -319,39 +322,43 @@ private lemma sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : fact p.prime]
   ∑ a in Ico 1 (p / 2).succ, (a * q) / p +
   ∑ a in Ico 1 (q / 2).succ, (a * p) / q =
   (p / 2) * (q / 2) :=
-have hswap : (((Ico 1 (q / 2).succ).product (Ico 1 (p / 2).succ)).filter
+begin
+  have hswap : (((Ico 1 (q / 2).succ).product (Ico 1 (p / 2).succ)).filter
     (λ x : ℕ × ℕ, x.2 * q ≤ x.1 * p)).card =
   (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
     (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p)).card :=
   card_congr (λ x _, prod.swap x)
-    (λ ⟨_, _⟩, by simp {contextual := tt})
-    (λ ⟨_, _⟩ ⟨_, _⟩, by simp {contextual := tt})
-    (λ ⟨x₁, x₂⟩ h, ⟨⟨x₂, x₁⟩, by revert h; simp {contextual := tt}⟩),
-have hdisj : disjoint
+    (λ ⟨_, _⟩, by simp only [mem_filter, and_self, prod.swap_prod_mk, forall_true_iff, mem_product]
+      {contextual := tt})
+    (λ ⟨_, _⟩ ⟨_, _⟩, by simp only [prod.mk.inj_iff, eq_self_iff_true, and_self, prod.swap_prod_mk,
+      forall_true_iff] {contextual := tt})
+    (λ ⟨x₁, x₂⟩ h, ⟨⟨x₂, x₁⟩, by revert h; simp only [mem_filter, eq_self_iff_true, and_self,
+      exists_prop_of_true, prod.swap_prod_mk, forall_true_iff, mem_product] {contextual := tt}⟩),
+  have hdisj : disjoint
     (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
       (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q))
     (((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
       (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p)),
-  from disjoint_filter.2 $ λ x hx hpq hqp,
-  have hxp : x.1 < p, from lt_of_le_of_lt
-    (show x.1 ≤ p / 2, by simp [*, nat.lt_succ_iff] at *; tauto)
-    (nat.div_lt_self hp.pos dec_trivial),
-  begin
+  { apply disjoint_filter.2 (λ x hx hpq hqp, _),
+    have hxp : x.1 < p, from lt_of_le_of_lt
+      (show x.1 ≤ p / 2, by simp only [*, lt_succ_iff, Ico.mem, mem_product] at *; tauto)
+      (nat.div_lt_self hp.pos dec_trivial),
     have : (x.1 : zmod p) = 0,
-    { simpa [hq0] using congr_arg (coe : ℕ → zmod p) (le_antisymm hpq hqp) },
+      { simpa [hq0] using congr_arg (coe : ℕ → zmod p) (le_antisymm hpq hqp) },
     apply_fun zmod.val at this,
     rw [val_cast_of_lt hxp, val_zero] at this,
-    simp * at *
-  end,
-have hunion : ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
+    simpa only [this, le_zero_iff_eq, Ico.mem, one_ne_zero, false_and, mem_product] using hx },
+  have hunion : ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
       (λ x : ℕ × ℕ, x.2 * p ≤ x.1 * q) ∪
     ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)).filter
       (λ x : ℕ × ℕ, x.1 * q ≤ x.2 * p) =
     ((Ico 1 (p / 2).succ).product (Ico 1 (q / 2).succ)),
-  from finset.ext $ λ x, by have := le_total (x.2 * p) (x.1 * q); simp; tauto,
-by rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion,
-    card_product];
-  simp
+  from finset.ext (λ x, by have := le_total (x.2 * p) (x.1 * q);
+    simp only [mem_union, mem_filter, Ico.mem, mem_product]; tauto),
+  rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_disjoint_union hdisj, hunion,
+    card_product],
+  simp only [Ico.card, nat.sub_zero, succ_sub_succ_eq_sub]
+end
 
 variables (p q : ℕ) [fact p.prime] [fact q.prime]
 
diff --git a/src/order/filter/filter_product.lean b/src/order/filter/filter_product.lean
index 87a52b3bfc5fb..dfc28f23781fb 100644
--- a/src/order/filter/filter_product.lean
+++ b/src/order/filter/filter_product.lean
@@ -39,7 +39,7 @@ protected def division_ring [division_ring β] (U : is_ultrafilter φ) : divisio
   inv_mul_cancel := λ f, induction_on f $ λ f hf, coe_eq.2 $ (U.em (λ y, f y = 0)).elim
     (λ H, (hf $ coe_eq.2 H).elim) (λ H, H.mono $ λ x, inv_mul_cancel),
   inv_zero := coe_eq.2 $ by simp only [(∘), inv_zero],
-  .. germ.ring, .. germ.has_inv, .. germ.nonzero U.1 }
+  .. germ.ring, .. germ.has_inv, .. germ.nontrivial U.1 }
 
 /-- If `φ` is an ultrafilter then the ultraproduct is a field.
 This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
@@ -78,8 +78,7 @@ This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
 protected def ordered_ring [ordered_ring β] (U : is_ultrafilter φ) : ordered_ring β* :=
 { mul_pos := λ x y, induction_on₂ x y $ λ f g hf hg, (coe_pos U).2 $
     ((coe_pos U).1 hg).mp $ ((coe_pos U).1 hf).mono $ λ x, mul_pos,
-  .. germ.ring, .. germ.ordered_add_comm_group,
-  .. germ.nonzero U.1 }
+  .. germ.ring, .. germ.ordered_add_comm_group, .. germ.nontrivial U.1 }
 
 /-- If `φ` is an ultrafilter then the ultraproduct is a linear ordered ring.
 This cannot be an instance, since it depends on `φ` being an ultrafilter. -/
diff --git a/src/order/filter/germ.lean b/src/order/filter/germ.lean
index 74155231e223c..87ea9b15959ab 100644
--- a/src/order/filter/germ.lean
+++ b/src/order/filter/germ.lean
@@ -330,11 +330,10 @@ section ring
 
 variables {R : Type*}
 
-/-- If `0 ≠ 1` in `β` and `l` is a non-trivial filter (`l ≠ ⊥`), then `0 ≠ 1` in `germ l β`.
+/-- If `β` is nontrivial and `l` is a non-trivial filter (`l ≠ ⊥`), then `germ l β` is nontrivial.
 This cannot be an `instance` because it depends on `l ≠ ⊥`. -/
-protected lemma nonzero [has_zero R] [has_one R] [nonzero R] (hl : l ≠ ⊥) :
-  nonzero (germ l R) :=
-{ zero_ne_one := mt (const_inj hl).1 zero_ne_one }
+protected lemma nontrivial [nontrivial R] (hl : l ≠ ⊥) : nontrivial (germ l R) :=
+let ⟨x, y, h⟩ := exists_pair_ne R in ⟨⟨↑x, ↑y, mt (const_inj hl).1 h⟩⟩
 
 instance [mul_zero_class R] : mul_zero_class (germ l R) :=
 { zero := 0,
diff --git a/src/ring_theory/algebraic.lean b/src/ring_theory/algebraic.lean
index 871bc6d4073a1..905fa786a86be 100644
--- a/src/ring_theory/algebraic.lean
+++ b/src/ring_theory/algebraic.lean
@@ -69,7 +69,7 @@ end
 end
 
 section zero_ne_one
-variables (R : Type u) {A : Type v} [comm_ring R] [nonzero R] [comm_ring A] [algebra R A]
+variables (R : Type u) {A : Type v} [comm_ring R] [nontrivial R] [comm_ring A] [algebra R A]
 
 /-- An integral element of an algebra is algebraic.-/
 lemma is_integral.is_algebraic {x : A} (h : is_integral R x) : is_algebraic R x :=
diff --git a/src/ring_theory/fintype.lean b/src/ring_theory/fintype.lean
index 2922e7fc61271..56e93236bdc14 100644
--- a/src/ring_theory/fintype.lean
+++ b/src/ring_theory/fintype.lean
@@ -12,6 +12,6 @@ import data.fintype.basic
 
 open_locale classical
 
-lemma card_units_lt (R : Type*) [semiring R] [nonzero R] [fintype R] :
+lemma card_units_lt (R : Type*) [semiring R] [nontrivial R] [fintype R] :
   fintype.card (units R) < fintype.card R :=
 card_lt_card_of_injective_of_not_mem (coe : units R → R) units.ext not_is_unit_zero
diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean
index d0e87147c7768..d93bbaf6b33db 100644
--- a/src/ring_theory/fractional_ideal.lean
+++ b/src/ring_theory/fractional_ideal.lean
@@ -429,11 +429,11 @@ open_locale classical
 
 variables {K : Type*} [field K] {g : fraction_map R K}
 
-instance : nonzero (fractional_ideal g) :=
-{ zero_ne_one := λ h,
+instance : nontrivial (fractional_ideal g) :=
+⟨⟨0, 1, λ h,
   have this : (1 : K) ∈ (0 : fractional_ideal g) :=
     by rw ←g.to_map.map_one; convert coe_mem_one _,
-  @one_ne_zero _ _ _ domain.to_nonzero (mem_zero_iff.mp this) }
+  one_ne_zero (mem_zero_iff.mp this) ⟩⟩
 
 lemma fractional_div_of_nonzero {I J : fractional_ideal g} (h : J ≠ 0) :
   is_fractional g (I.1 / J.1) :=
@@ -477,7 +477,7 @@ by { rw inv_nonzero h, refl }
 
 @[simp] lemma div_one {I : fractional_ideal g} : I / 1 = I :=
 begin
-  rw [div_nonzero (@one_ne_zero (fractional_ideal g) _ _ _)],
+  rw [div_nonzero (@one_ne_zero (fractional_ideal g) _ _)],
   ext,
   split; intro h,
   { convert mem_div_iff_forall_mul_mem.mp h 1
@@ -491,7 +491,7 @@ begin
 end
 
 lemma ne_zero_of_mul_eq_one (I J : fractional_ideal g) (h : I * J = 1) : I ≠ 0 :=
-λ hI, @zero_ne_one (fractional_ideal g) _ _ _ (by { convert h, simp [hI], })
+λ hI, @zero_ne_one (fractional_ideal g) _ _ (by { convert h, simp [hI], })
 
 /-- `I⁻¹` is the inverse of `I` if `I` has an inverse. -/
 theorem right_inverse_eq (I J : fractional_ideal g) (h : I * J = 1) :
diff --git a/src/ring_theory/free_comm_ring.lean b/src/ring_theory/free_comm_ring.lean
index 5dba6dffeb0cf..1dd9a511f3ff9 100644
--- a/src/ring_theory/free_comm_ring.lean
+++ b/src/ring_theory/free_comm_ring.lean
@@ -9,7 +9,7 @@ import ring_theory.ideal_operations
 import ring_theory.free_ring
 
 noncomputable theory
-local attribute [instance, priority 100] classical.prop_decidable
+open_locale classical
 
 universes u v
 
@@ -69,7 +69,7 @@ free_abelian_group.lift.sub _ _ _
 @[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y :=
 begin
   refine free_abelian_group.induction_on y (mul_zero _).symm _ _ _,
-  { intros s2, conv_lhs { dsimp only [(*), distrib.mul, ring.mul, comm_ring.mul, semigroup.mul] },
+  { intros s2, conv_lhs { dsimp only [free_abelian_group.mul_def] },
     rw [free_abelian_group.lift.of, lift, free_abelian_group.lift.of],
     refine free_abelian_group.induction_on x (zero_mul _).symm _ _ _,
     { intros s1, iterate 3 { rw free_abelian_group.lift.of },
diff --git a/src/ring_theory/free_ring.lean b/src/ring_theory/free_ring.lean
index e51795cbbe432..6e2a5c5cb1cbf 100644
--- a/src/ring_theory/free_ring.lean
+++ b/src/ring_theory/free_ring.lean
@@ -62,7 +62,8 @@ free_abelian_group.lift.sub _ _ _
 @[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y :=
 begin
   refine free_abelian_group.induction_on y (mul_zero _).symm _ _ _,
-  { intros L2, conv_lhs { dsimp only [(*), distrib.mul, ring.mul, semigroup.mul] },
+  { intros L2,
+    conv_lhs { dsimp only [free_abelian_group.mul_def] },
     rw [free_abelian_group.lift.of, lift, free_abelian_group.lift.of],
     refine free_abelian_group.induction_on x (zero_mul _).symm _ _ _,
     { intros L1, iterate 3 { rw free_abelian_group.lift.of },
diff --git a/src/ring_theory/ideal_operations.lean b/src/ring_theory/ideal_operations.lean
index 8eeddb3e3546a..9940b6081f6bd 100644
--- a/src/ring_theory/ideal_operations.lean
+++ b/src/ring_theory/ideal_operations.lean
@@ -779,7 +779,7 @@ lemma ker_eq_bot_iff_eq_zero : ker f = ⊥ ↔ ∀ x, f x = 0 → x = 0 :=
 by rw [submodule.ext'_iff, ker_eq]; exact is_add_group_hom.trivial_ker_iff_eq_zero f
 
 /-- If the target is not the zero ring, then one is not in the kernel.-/
-lemma not_one_mem_ker [nonzero S] (f : R →+* S) : (1:R) ∉ ker f :=
+lemma not_one_mem_ker [nontrivial S] (f : R →+* S) : (1:R) ∉ ker f :=
 by { rw [mem_ker, f.map_one], exact one_ne_zero }
 
 end comm_ring
diff --git a/src/ring_theory/ideals.lean b/src/ring_theory/ideals.lean
index d336123426306..98d3a6be84a18 100644
--- a/src/ring_theory/ideals.lean
+++ b/src/ring_theory/ideals.lean
@@ -252,8 +252,8 @@ eq_comm.trans $ eq_zero_iff_mem.trans (eq_top_iff_one _).symm
 theorem zero_ne_one_iff {I : ideal α} : (0 : I.quotient) ≠ 1 ↔ I ≠ ⊤ :=
 not_congr zero_eq_one_iff
 
-protected theorem nonzero {I : ideal α} (hI : I ≠ ⊤) : nonzero I.quotient :=
-{ zero_ne_one := zero_ne_one_iff.2 hI }
+protected theorem nontrivial {I : ideal α} (hI : I ≠ ⊤) : nontrivial I.quotient :=
+⟨⟨0, 1, zero_ne_one_iff.2 hI⟩⟩
 
 instance (I : ideal α) [hI : I.is_prime] : integral_domain I.quotient :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b,
@@ -261,8 +261,8 @@ instance (I : ideal α) [hI : I.is_prime] : integral_domain I.quotient :=
       (hI.mem_or_mem (eq_zero_iff_mem.1 hab)).elim
         (or.inl ∘ eq_zero_iff_mem.2)
         (or.inr ∘ eq_zero_iff_mem.2),
-  ..quotient.nonzero hI.1,
-  ..quotient.comm_ring I }
+  .. quotient.comm_ring I,
+  .. quotient.nontrivial hI.1 }
 
 lemma exists_inv {I : ideal α} [hI : I.is_maximal] :
  ∀ {a : I.quotient}, a ≠ 0 → ∃ b : I.quotient, a * b = 1 :=
@@ -366,7 +366,7 @@ section prio
 set_option default_priority 100 -- see Note [default priority]
 /-- A commutative ring is local if it has a unique maximal ideal. Note that
   `local_ring` is a predicate. -/
-class local_ring (α : Type u) [comm_ring α] extends nonzero α : Prop :=
+class local_ring (α : Type u) [comm_ring α] extends nontrivial α : Prop :=
 (is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a)))
 end prio
 
@@ -439,13 +439,13 @@ end local_ring
 
 lemma local_of_nonunits_ideal [comm_ring α] (hnze : (0:α) ≠ 1)
   (h : ∀ x y ∈ nonunits α, x + y ∈ nonunits α) : local_ring α :=
-{ zero_ne_one := hnze,
+{ exists_pair_ne := ⟨0, 1, hnze⟩,
   is_local := λ x, or_iff_not_imp_left.mpr $ λ hx,
-begin
-  by_contra H,
-  apply h _ _ hx H,
-  simp [-sub_eq_add_neg, add_sub_cancel'_right]
-end}
+  begin
+    by_contra H,
+    apply h _ _ hx H,
+    simp [-sub_eq_add_neg, add_sub_cancel'_right]
+  end }
 
 lemma local_of_unique_max_ideal [comm_ring α] (h : ∃! I : ideal α, I.is_maximal) :
   local_ring α :=
diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean
index 792b95337a5c2..33c8e4eb377af 100644
--- a/src/ring_theory/integral_closure.lean
+++ b/src/ring_theory/integral_closure.lean
@@ -368,7 +368,7 @@ section integral_domain
 variables {R S : Type*} [comm_ring R] [integral_domain S] [algebra R S]
 
 instance : integral_domain (integral_closure R S) :=
-{ zero_ne_one := mt subtype.ext_iff_val.mp zero_ne_one,
+{ exists_pair_ne := ⟨0, 1, mt subtype.ext_iff_val.mp zero_ne_one⟩,
   eq_zero_or_eq_zero_of_mul_eq_zero := λ ⟨a, ha⟩ ⟨b, hb⟩ h,
     or.imp subtype.ext_iff_val.mpr subtype.ext_iff_val.mpr (eq_zero_or_eq_zero_of_mul_eq_zero (subtype.ext_iff_val.mp h)),
   ..(integral_closure R S).comm_ring R S }
diff --git a/src/ring_theory/localization.lean b/src/ring_theory/localization.lean
index 403352c06e9b4..cc8f5660d3b44 100644
--- a/src/ring_theory/localization.lean
+++ b/src/ring_theory/localization.lean
@@ -876,7 +876,7 @@ lemma eq_zero_of_ne_zero_of_mul_eq_zero
 
 lemma mem_non_zero_divisors_iff_ne_zero {x : A} :
   x ∈ non_zero_divisors A ↔ x ≠ 0 :=
-⟨λ hm hz, @zero_ne_one A _ _ domain.to_nonzero (hm 1 $ by rw [hz, one_mul]).symm,
+⟨λ hm hz, zero_ne_one (hm 1 $ by rw [hz, one_mul]).symm,
 λ hnx z, eq_zero_of_ne_zero_of_mul_eq_zero hnx⟩
 
 lemma map_ne_zero_of_mem_non_zero_divisors {B : Type*} [ring B] {g : A →+* B}
@@ -934,8 +934,7 @@ def to_integral_domain [comm_ring K] (φ : fraction_map A K) : integral_domain K
         { exact or.inl (φ.eq_zero_of_fst_eq_zero hx H) },
       { exact or.inr (φ.eq_zero_of_fst_eq_zero hy H) },
     end,
-  zero_ne_one := by erw [←φ.to_map.map_zero, ←φ.to_map.map_one];
-    exact λ h, @zero_ne_one _ _ _ domain.to_nonzero (φ.injective h),
+  exists_pair_ne := ⟨φ.to_map 0, φ.to_map 1, λ h, zero_ne_one (φ.injective h)⟩,
   ..(infer_instance : comm_ring K) }
 
 /-- The inverse of an element in the field of fractions of an integral domain. -/
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index 1ccc35e74a413..db21b68998cd3 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -339,7 +339,7 @@ lemma well_founded_submodule_gt (R M) [ring R] [add_comm_group M] [module R M] :
   ∀ [is_noetherian R M], well_founded ((>) : submodule R M → submodule R M → Prop) :=
 is_noetherian_iff_well_founded.mp
 
-lemma finite_of_linear_independent {R M} [comm_ring R] [nonzero R] [add_comm_group M] [module R M]
+lemma finite_of_linear_independent {R M} [comm_ring R] [nontrivial R] [add_comm_group M] [module R M]
   [is_noetherian R M] {s : set M} (hs : linear_independent R (coe : s → M)) : s.finite :=
 begin
   refine classical.by_contradiction (λ hf, order_embedding.well_founded_iff_no_descending_seq.1
diff --git a/src/ring_theory/polynomial/basic.lean b/src/ring_theory/polynomial/basic.lean
index 4982e00046a44..218f31584df1a 100644
--- a/src/ring_theory/polynomial/basic.lean
+++ b/src/ring_theory/polynomial/basic.lean
@@ -260,7 +260,8 @@ is_noetherian_submodule_left.1 (is_noetherian_of_fg_of_noetherian _
 end ideal
 
 /-- Hilbert basis theorem: a polynomial ring over a noetherian ring is a noetherian ring. -/
-protected theorem polynomial.is_noetherian_ring [is_noetherian_ring R] : is_noetherian_ring (polynomial R) :=
+protected theorem polynomial.is_noetherian_ring [is_noetherian_ring R] :
+  is_noetherian_ring (polynomial R) :=
 ⟨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))
@@ -288,7 +289,7 @@ from hs ▸ λ x hx, submodule.span_induction hx (λ _ hx, ideal.subset_span hx)
     have : (0 : R) ≠ 1,
     { intro h, apply hp0, ext i, refine (mul_one _).symm.trans _,
       rw [← h, mul_zero], refl },
-    haveI : nonzero R := ⟨this⟩,
+    haveI : nontrivial R := ⟨⟨0, 1, this⟩⟩,
     have : p.leading_coeff ∈ I.leading_coeff_nth N,
     { rw HN, exact hm2 k ((I.mem_leading_coeff_nth _ _).2
         ⟨_, hp, hn ▸ polynomial.degree_le_nat_degree, rfl⟩) },
@@ -416,14 +417,13 @@ end
 instance {R : Type u} {σ : Type v} [integral_domain R] :
   integral_domain (mv_polynomial σ R) :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := mv_polynomial.eq_zero_or_eq_zero_of_mul_eq_zero,
-  zero_ne_one :=
+  exists_pair_ne := ⟨0, 1, λ H,
   begin
-    intro H,
     have : eval₂ id (λ s, (0:R)) (0 : mv_polynomial σ R) =
       eval₂ id (λ s, (0:R)) (1 : mv_polynomial σ R),
     { congr, exact H },
     simpa,
-  end,
+  end⟩,
   .. (by apply_instance : comm_ring (mv_polynomial σ R)) }
 
 end mv_polynomial
diff --git a/src/ring_theory/power_series.lean b/src/ring_theory/power_series.lean
index 5777bb2d54074..a5b4827e2cfbc 100644
--- a/src/ring_theory/power_series.lean
+++ b/src/ring_theory/power_series.lean
@@ -596,27 +596,11 @@ end
 
 end ring
 
-section comm_ring
-variable [comm_ring α]
-
-/-- Multivariate formal power series over a local ring form a local ring.-/
-instance is_local_ring [local_ring α] : local_ring (mv_power_series σ α) :=
-{ zero_ne_one := by { have H : (0:α) ≠ 1 := ‹local_ring α›.zero_ne_one, contrapose! H,
-    simpa using congr_arg (constant_coeff σ α) H },
-  is_local := by { intro φ, rcases local_ring.is_local (constant_coeff σ α φ) with ⟨u,h⟩|⟨u,h⟩;
-    [left, right];
-    { refine is_unit_of_mul_eq_one _ _ (mul_inv_of_unit _ u _),
-      simpa using h.symm } } }
-
--- TODO(jmc): once adic topology lands, show that this is complete
-
-end comm_ring
-
-section nonzero
-variables [semiring α] [nonzero α]
+section nontrivial
+variables [semiring α] [nontrivial α]
 
-instance : nonzero (mv_power_series σ α) :=
-{ zero_ne_one := assume h, zero_ne_one $ show (0:α) = 1, from congr_arg (constant_coeff σ α) h }
+instance : nontrivial (mv_power_series σ α) :=
+⟨⟨0, 1, assume h, zero_ne_one $ show (0:α) = 1, from congr_arg (constant_coeff σ α) h ⟩⟩
 
 lemma X_inj {s t : σ} : (X s : mv_power_series σ α) = X t ↔ s = t :=
 ⟨begin
@@ -627,7 +611,21 @@ lemma X_inj {s t : σ} : (X s : mv_power_series σ α) = X t ↔ s = t :=
   { exfalso, exact one_ne_zero h }
 end, congr_arg X⟩
 
-end nonzero
+end nontrivial
+
+section comm_ring
+variable [comm_ring α]
+
+/-- Multivariate formal power series over a local ring form a local ring. -/
+instance is_local_ring [local_ring α] : local_ring (mv_power_series σ α) :=
+{ is_local := by { intro φ, rcases local_ring.is_local (constant_coeff σ α φ) with ⟨u,h⟩|⟨u,h⟩;
+    [left, right];
+    { refine is_unit_of_mul_eq_one _ _ (mul_inv_of_unit _ u _),
+      simpa using h.symm } } }
+
+-- TODO(jmc): once adic topology lands, show that this is complete
+
+end comm_ring
 
 section local_ring
 variables {β : Type*} [comm_ring α] [comm_ring β] (f : α →+* β)
@@ -651,8 +649,7 @@ end⟩
 variables [local_ring α] [local_ring β]
 
 instance : local_ring (mv_power_series σ α) :=
-{ zero_ne_one := zero_ne_one,
-  is_local := local_ring.is_local }
+{ is_local := local_ring.is_local }
 
 end local_ring
 
@@ -776,7 +773,7 @@ instance [semiring α]        : semiring        (power_series α) := by apply_in
 instance [comm_semiring α]   : comm_semiring   (power_series α) := by apply_instance
 instance [ring α]            : ring            (power_series α) := by apply_instance
 instance [comm_ring α]       : comm_ring       (power_series α) := by apply_instance
-instance [semiring α] [nonzero α] : nonzero    (power_series α) := by apply_instance
+instance [semiring α] [nontrivial α] : nontrivial    (power_series α) := by apply_instance
 instance [semiring α]        : semimodule α    (power_series α) := by apply_instance
 instance [comm_ring α]       : algebra α       (power_series α) := by apply_instance
 
@@ -1150,8 +1147,8 @@ end
 
 instance : integral_domain (power_series α) :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := eq_zero_or_eq_zero_of_mul_eq_zero,
-  .. power_series.comm_ring,
-  .. power_series.nonzero }
+  .. power_series.nontrivial,
+  .. power_series.comm_ring }
 
 /-- The ideal spanned by the variable in the power series ring
  over an integral domain is a prime ideal.-/
@@ -1419,7 +1416,7 @@ by rw [order_monomial, if_neg h]
 end order_basic
 
 section order_zero_ne_one
-variables [comm_semiring α] [nonzero α]
+variables [comm_semiring α] [nontrivial α]
 
 /-- The order of the formal power series `1` is `0`.-/
 @[simp] lemma order_one : order (1 : power_series α) = 0 :=
diff --git a/src/ring_theory/prod.lean b/src/ring_theory/prod.lean
index 442d790fafc19..4c8554bb61736 100644
--- a/src/ring_theory/prod.lean
+++ b/src/ring_theory/prod.lean
@@ -43,11 +43,6 @@ instance [ring R] [ring S] : ring (R × S) :=
 instance [comm_ring R] [comm_ring S] : comm_ring (R × S) :=
 { .. prod.ring, .. prod.comm_monoid }
 
-/-- Product of two commutative rings is a nonzero commutative ring provided that the first
-ring is a nonzero ring. -/
-instance [has_zero R] [has_one R] [nonzero R] [has_zero S] [has_one S] : nonzero (R × S) :=
-{ zero_ne_one := mt (congr_arg prod.fst) zero_ne_one }
-
 end prod
 
 namespace ring_hom
diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean
index 76edb142cc94c..ab97947a34a68 100644
--- a/src/ring_theory/subring.lean
+++ b/src/ring_theory/subring.lean
@@ -64,7 +64,7 @@ instance subtype.comm_ring {S : set cR} [is_subring S] : comm_ring (subtype S) :
 
 instance subring.domain {D : Type*} [integral_domain D] (S : set D) [is_subring S] :
   integral_domain S :=
-{ zero_ne_one := mt subtype.ext_iff_val.1 zero_ne_one,
+{ exists_pair_ne := ⟨0, 1, mt subtype.ext_iff_val.1 zero_ne_one⟩,
   eq_zero_or_eq_zero_of_mul_eq_zero := λ ⟨x, hx⟩ ⟨y, hy⟩,
     by { simp only [subtype.ext_iff_val, subtype.coe_mk], exact eq_zero_or_eq_zero_of_mul_eq_zero },
   .. subset.comm_ring }
diff --git a/src/ring_theory/unique_factorization_domain.lean b/src/ring_theory/unique_factorization_domain.lean
index b0bd837ffb301..c811e2321981d 100644
--- a/src/ring_theory/unique_factorization_domain.lean
+++ b/src/ring_theory/unique_factorization_domain.lean
@@ -314,7 +314,8 @@ begin
   apply function.hfunext,
   { have : a ~ᵤ 0 ↔ b ~ᵤ 0, from
       iff.intro (assume ha0, hab.symm.trans ha0) (assume hb0, hab.trans hb0),
-    simp [quotient_mk_eq_mk, mk_eq_zero, ← associated_zero_iff_eq_zero, this] },
+    simp only [associated_zero_iff_eq_zero] at this,
+    simp only [quotient_mk_eq_mk, this, mk_eq_zero] },
   exact (assume ha hb eq, heq_of_eq $ congr_arg some $ factors'_cong _ _ hab)
 end
 
diff --git a/src/set_theory/cardinal.lean b/src/set_theory/cardinal.lean
index cbf8140743cdf..4567675c35b6e 100644
--- a/src/set_theory/cardinal.lean
+++ b/src/set_theory/cardinal.lean
@@ -110,13 +110,16 @@ not_iff_comm.1
 
 instance : has_one cardinal.{u} := ⟨⟦punit⟧⟩
 
-instance : nonzero cardinal.{u} :=
-{ zero_ne_one := ne.symm $ ne_zero_iff_nonempty.2 ⟨punit.star⟩ }
+instance : nontrivial cardinal.{u} :=
+⟨⟨1, 0, ne_zero_iff_nonempty.2 ⟨punit.star⟩⟩⟩
 
 theorem le_one_iff_subsingleton {α : Type u} : mk α ≤ 1 ↔ subsingleton α :=
 ⟨λ ⟨f⟩, ⟨λ a b, f.injective (subsingleton.elim _ _)⟩,
  λ ⟨h⟩, ⟨⟨λ a, punit.star, λ a b _, h _ _⟩⟩⟩
 
+theorem one_lt_iff_nontrivial {α : Type u} : 1 < mk α ↔ nontrivial α :=
+by { rw [← not_iff_not, not_nontrivial_iff_subsingleton, ← le_one_iff_subsingleton], simp }
+
 instance : has_add cardinal.{u} :=
 ⟨λq₁ q₂, quotient.lift_on₂ q₁ q₂ (λα β, mk (α ⊕ β)) $ assume α β γ δ ⟨e₁⟩ ⟨e₂⟩,
   quotient.sound ⟨equiv.sum_congr e₁ e₂⟩⟩
diff --git a/src/set_theory/ordinal.lean b/src/set_theory/ordinal.lean
index 1749009e746a9..cca8075dd6280 100644
--- a/src/set_theory/ordinal.lean
+++ b/src/set_theory/ordinal.lean
@@ -979,11 +979,14 @@ theorem type_ne_zero_iff_nonempty [is_well_order α r] : type r ≠ 0 ↔ nonemp
 @[simp] theorem type_eq_zero_iff_empty [is_well_order α r] : type r = 0 ↔ ¬ nonempty α :=
 (not_iff_comm.1 type_ne_zero_iff_nonempty).symm
 
-instance : nonzero ordinal.{u} :=
-{ zero_ne_one := ne.symm $ type_ne_zero_iff_nonempty.2 ⟨punit.star⟩ }
+protected lemma one_ne_zero : (1 : ordinal) ≠ 0 :=
+type_ne_zero_iff_nonempty.2 ⟨punit.star⟩
+
+instance : nontrivial ordinal.{u} :=
+⟨⟨1, 0, ordinal.one_ne_zero⟩⟩
 
 theorem zero_lt_one : (0 : ordinal) < 1 :=
-lt_iff_le_and_ne.2 ⟨zero_le _, zero_ne_one⟩
+lt_iff_le_and_ne.2 ⟨zero_le _, ne.symm $ ordinal.one_ne_zero⟩
 
 /-- The ordinal predecessor of `o` is `o'` if `o = succ o'`,
   and `o` otherwise. -/
@@ -1651,7 +1654,7 @@ by rw [← le_zero, div_le $ pos_iff_ne_zero.1 $ lt_of_le_of_lt (zero_le _) h];
 by simpa only [add_zero, zero_div] using mul_add_div a b0 0
 
 @[simp] theorem div_one (a : ordinal) : a / 1 = a :=
-by simpa only [one_mul] using mul_div_cancel a one_ne_zero
+by simpa only [one_mul] using mul_div_cancel a ordinal.one_ne_zero
 
 @[simp] theorem div_self {a : ordinal} (h : a ≠ 0) : a / a = 1 :=
 by simpa only [mul_one] using mul_div_cancel 1 h
@@ -2032,7 +2035,7 @@ begin
   { simp only [power_zero] },
   { intros _ ih, simp only [power_succ, ih, mul_one] },
   refine λ b l IH, eq_of_forall_ge_iff (λ c, _),
-  rw [power_le_of_limit one_ne_zero l],
+  rw [power_le_of_limit ordinal.one_ne_zero l],
   exact ⟨λ H, by simpa only [power_zero] using H 0 l.pos,
          λ H b' h, by rwa IH _ h⟩,
 end
@@ -2585,7 +2588,8 @@ by unfold CNF; rw [dif_neg b0, dif_neg b0, CNF_rec_ne_zero b0 o0]
 
 theorem one_CNF {o : ordinal} (o0 : o ≠ 0) :
   CNF 1 o = [(0, o)] :=
-by rw [CNF_ne_zero one_ne_zero o0, log_not_one_lt (lt_irrefl _), power_zero, mod_one, CNF_zero, div_one]
+by rw [CNF_ne_zero ordinal.one_ne_zero o0, log_not_one_lt (lt_irrefl _), power_zero, mod_one,
+       CNF_zero, div_one]
 
 theorem CNF_foldr {b : ordinal} (b0 : b ≠ 0) (o) :
   (CNF b o).foldr (λ p r, b ^ p.1 * p.2 + r) 0 = o :=
diff --git a/src/topology/metric_space/isometry.lean b/src/topology/metric_space/isometry.lean
index 72303da27d636..4132b4487d881 100644
--- a/src/topology/metric_space/isometry.lean
+++ b/src/topology/metric_space/isometry.lean
@@ -327,11 +327,9 @@ lemma embedding_of_subset_dist_le (a b : α) :
   dist (embedding_of_subset x a) (embedding_of_subset x b) ≤ dist a b :=
 begin
   refine (dist_le dist_nonneg).2 (λn, _),
-  have A : dist a (x n) + (dist (x 0) (x n) + (-dist b (x n) + -dist (x 0) (x n)))
-    = dist a (x n) - dist b (x n), by ring,
-  simp only [embedding_of_subset_coe, real.dist_eq, A, add_comm, neg_add_rev, _root_.neg_neg,
-             sub_eq_add_neg, add_left_comm],
-  exact abs_dist_sub_le _ _ _
+  simp only [embedding_of_subset_coe, real.dist_eq],
+  convert abs_dist_sub_le a b (x n) using 2,
+  ring
 end
 
 /-- When the reference set is dense, the embedding map is an isometry on its image. -/