diff --git a/archive/imo/imo1988_q6.lean b/archive/imo/imo1988_q6.lean
index 726012f2cf71e..aebb4e890a512 100644
--- a/archive/imo/imo1988_q6.lean
+++ b/archive/imo/imo1988_q6.lean
@@ -141,7 +141,7 @@ begin
   -- Finally, it also means that (m_x, m_y) does not lie in the base locus,
   -- that m_x ≠ 0, m_x ≠ m_y, B(m_x) ≠ m_y, and B(m_x) ≠ m_x + m_y.
   rcases h_base with ⟨h_base, hmx, hm_diag, hm_B₁, hm_B₂⟩,
-  replace hmx : 0 < mx := nat.pos_iff_ne_zero.mpr hmx,
+  replace hmx : 0 < mx := pos_iff_ne_zero.mpr hmx,
   -- Consider the quadratic equation that (m_x, m_y) satisfies.
   have h_quad := hHm, rw H_quad at h_quad,
   -- We find the other root of the equation, and Vieta's formulas.
diff --git a/src/algebra/archimedean.lean b/src/algebra/archimedean.lean
index a30c94cc8a0be..10df326163e48 100644
--- a/src/algebra/archimedean.lean
+++ b/src/algebra/archimedean.lean
@@ -83,7 +83,7 @@ lemma exists_nat_pow_near {x : α} {y : α} (hx : 1 ≤ x) (hy : 1 < y) :
 have h : ∃ n : ℕ, x < y ^ n, from pow_unbounded_of_one_lt _ hy,
 by classical; exact let n := nat.find h in
   have hn  : x < y ^ n, from nat.find_spec h,
-  have hnp : 0 < n,     from nat.pos_iff_ne_zero.2 (λ hn0,
+  have hnp : 0 < n,     from pos_iff_ne_zero.2 (λ hn0,
     by rw [hn0, pow_zero] at hn; exact (not_le_of_gt hn hx)),
   have hnsp : nat.pred n + 1 = n,     from nat.succ_pred_eq_of_pos hnp,
   have hltn : nat.pred n < n,         from nat.pred_lt (ne_of_gt hnp),
diff --git a/src/algebra/char_p/basic.lean b/src/algebra/char_p/basic.lean
index d45ed106d6a14..e588f1664a82c 100644
--- a/src/algebra/char_p/basic.lean
+++ b/src/algebra/char_p/basic.lean
@@ -335,7 +335,7 @@ match p, hc with
 end
 
 lemma char_is_prime_of_pos (p : ℕ) [h : fact (0 < p)] [char_p α p] : fact p.prime :=
-(char_p.char_is_prime_or_zero α _).resolve_right (nat.pos_iff_ne_zero.1 h)
+(char_p.char_is_prime_or_zero α _).resolve_right (pos_iff_ne_zero.1 h)
 
 theorem char_is_prime [fintype α] (p : ℕ) [char_p α p] : p.prime :=
 or.resolve_right (char_is_prime_or_zero α p) (char_ne_zero_of_fintype α p)
diff --git a/src/algebra/group_with_zero/power.lean b/src/algebra/group_with_zero/power.lean
index 76a3b12222b90..edf5adcb17b61 100644
--- a/src/algebra/group_with_zero/power.lean
+++ b/src/algebra/group_with_zero/power.lean
@@ -25,7 +25,7 @@ by { contrapose!, rintro rfl, exact zero_pow' n hn }
 @[simp] lemma zero_pow_eq_zero [nontrivial M] {n : ℕ} : (0 : M) ^ n = 0 ↔ 0 < n :=
 begin
   split; intro h,
-  { rw [nat.pos_iff_ne_zero], rintro rfl, simpa using h },
+  { rw [pos_iff_ne_zero], rintro rfl, simpa using h },
   { exact zero_pow' n h.ne.symm }
 end
 
diff --git a/src/algebra/invertible.lean b/src/algebra/invertible.lean
index 524f685c75ee8..c6c2613552d2a 100644
--- a/src/algebra/invertible.lean
+++ b/src/algebra/invertible.lean
@@ -237,7 +237,7 @@ invertible_of_nonzero (λ h, not_dvd ((char_p.cast_eq_zero_iff K p t).mp h))
 
 instance invertible_of_pos {K : Type*} [field K] [char_zero K] (n : ℕ) [h : fact (0 < n)] :
   invertible (n : K) :=
-invertible_of_nonzero $ by simpa [nat.pos_iff_ne_zero] using h
+invertible_of_nonzero $ by simpa [pos_iff_ne_zero] using h
 
 end char_p
 
diff --git a/src/algebra/ordered_monoid.lean b/src/algebra/ordered_monoid.lean
index cdfc0f27cae06..701f4a6382536 100644
--- a/src/algebra/ordered_monoid.lean
+++ b/src/algebra/ordered_monoid.lean
@@ -558,6 +558,14 @@ variables [canonically_ordered_monoid α] {a b c d : α}
 lemma le_iff_exists_mul : a ≤ b ↔ ∃c, b = a * c :=
 canonically_ordered_monoid.le_iff_exists_mul a b
 
+@[to_additive]
+lemma self_le_mul_right (a b : α) : a ≤ a * b :=
+le_iff_exists_mul.mpr ⟨b, rfl⟩
+
+@[to_additive]
+lemma self_le_mul_left (a b : α) : a ≤ b * a :=
+by { rw [mul_comm], exact self_le_mul_right a b }
+
 @[simp, to_additive zero_le] lemma one_le (a : α) : 1 ≤ a := le_iff_exists_mul.mpr ⟨a, by simp⟩
 
 @[simp, to_additive] lemma bot_eq_one : (⊥ : α) = 1 :=
@@ -566,14 +574,12 @@ le_antisymm bot_le (one_le ⊥)
 @[simp, to_additive] lemma mul_eq_one_iff : a * b = 1 ↔ a = 1 ∧ b = 1 :=
 mul_eq_one_iff' (one_le _) (one_le _)
 
--- TODO -- global replace le_zero_iff_eq by n nonpos_iff_eq_zero?
-@[simp, to_additive le_zero_iff_eq] lemma le_one_iff_eq : a ≤ 1 ↔ a = 1 :=
+@[simp, to_additive] lemma le_one_iff_eq_one : a ≤ 1 ↔ a = 1 :=
 iff.intro
   (assume h, le_antisymm h (one_le a))
   (assume h, h ▸ le_refl a)
 
--- TODO -- global replace zero_lt_iff_ne_zero by pos_iff_ne_zero?
-@[to_additive zero_lt_iff_ne_zero] lemma one_lt_iff_ne_one : 1 < a ↔ a ≠ 1 :=
+@[to_additive] lemma one_lt_iff_ne_one : 1 < a ↔ a ≠ 1 :=
 iff.intro ne_of_gt $ assume hne, lt_of_le_of_ne (one_le _) hne.symm
 
 @[to_additive] lemma exists_pos_mul_of_lt (h : a < b) : ∃ c > 1, a * c = b :=
diff --git a/src/algebra/ordered_ring.lean b/src/algebra/ordered_ring.lean
index 07f9ada056c5a..52d71d17ff53b 100644
--- a/src/algebra/ordered_ring.lean
+++ b/src/algebra/ordered_ring.lean
@@ -948,7 +948,7 @@ mul_le_mul h le_rfl
 lemma zero_lt_one [nontrivial α] : (0:α) < 1 := (zero_le 1).lt_of_ne zero_ne_one
 
 lemma mul_pos : 0 < a * b ↔ (0 < a) ∧ (0 < b) :=
-by simp only [zero_lt_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
+by simp only [pos_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
 
 end canonically_ordered_semiring
 
diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean
index a652781d74e51..4cfc2fdd58cec 100644
--- a/src/analysis/analytic/basic.lean
+++ b/src/analysis/analytic/basic.lean
@@ -142,7 +142,7 @@ lemma lt_radius_of_is_O (h₀ : r ≠ 0) {a : ℝ} (ha : a ∈ Ioo (-1 : ℝ) 1)
 begin
   rcases ((tfae_exists_lt_is_o_pow (λ n, ∥p n∥ * r ^ n) 1).out 2 5).mp ⟨a, ha, hp⟩
     with ⟨a, ha, C, hC, hp⟩,
-  replace h₀ : 0 < r := zero_lt_iff_ne_zero.2 h₀,
+  replace h₀ : 0 < r := pos_iff_ne_zero.2 h₀,
   lift a to ℝ≥0 using ha.1.le,
   have : (r : ℝ) < r / a :=
     (lt_div_iff ha.1).2 (by simpa only [mul_one] using mul_lt_mul_of_pos_left ha.2 h₀),
@@ -301,7 +301,7 @@ begin
   have zero_mem : (0 : E) ∈ emetric.ball (0 : E) r, by simp [hf.r_pos],
   have : ∀ i ≠ 0, pf i (λ j, 0) = 0,
   { assume i hi,
-    have : 0 < i := zero_lt_iff_ne_zero.2 hi,
+    have : 0 < i := pos_iff_ne_zero.2 hi,
     exact continuous_multilinear_map.map_coord_zero _ (⟨0, this⟩ : fin i) rfl },
   have A := (hf.has_sum zero_mem).unique (has_sum_single _ this),
   simpa [v_eq] using A.symm,
diff --git a/src/analysis/convex/integral.lean b/src/analysis/convex/integral.lean
index f5db808c75258..3a5aa3e7f265b 100644
--- a/src/analysis/convex/integral.lean
+++ b/src/analysis/convex/integral.lean
@@ -66,7 +66,7 @@ begin
       (λ y, μ ((F n) ⁻¹' {y})) (λ _ _, (measure_lt_top _ _))],
   rw [← this, simple_func.integral],
   refine hs.center_mass_mem (λ _ _, ennreal.to_real_nonneg) _ _,
-  { rw [this, ennreal.to_real_pos_iff, zero_lt_iff_ne_zero, ne.def, measure.measure_univ_eq_zero],
+  { rw [this, ennreal.to_real_pos_iff, pos_iff_ne_zero, ne.def, measure.measure_univ_eq_zero],
     exact ⟨hμ, measure_ne_top _ _⟩ },
   { simp only [simple_func.mem_range],
     rintros _ ⟨x, rfl⟩,
diff --git a/src/analysis/p_series.lean b/src/analysis/p_series.lean
index 63e598c9b4961..e55321c6f9ed2 100644
--- a/src/analysis/p_series.lean
+++ b/src/analysis/p_series.lean
@@ -182,7 +182,7 @@ begin
         ((h.tendsto_cofinite_zero.eventually (gt_mem_nhds zero_lt_one)).and
           (eventually_cofinite_ne 0)).exists,
       apply hk₀,
-      rw [← zero_lt_iff_ne_zero, ← @nat.cast_pos ℝ] at hk₀,
+      rw [← pos_iff_ne_zero, ← @nat.cast_pos ℝ] at hk₀,
       simpa [inv_lt_one_iff_of_pos (rpow_pos_of_pos hk₀ _), one_lt_rpow_iff_of_pos hk₀, hp,
         hp.not_lt, hk₀] using hk₁ } }
 end
diff --git a/src/analysis/special_functions/pow.lean b/src/analysis/special_functions/pow.lean
index fbb65a3a64fac..f17a6633823ed 100644
--- a/src/analysis/special_functions/pow.lean
+++ b/src/analysis/special_functions/pow.lean
@@ -109,7 +109,7 @@ have h : -π < (log x * (↑n)⁻¹).im ∧ (log x * (↑n)⁻¹).im ≤ π,
               (mul_le_mul_of_nonneg_right (by rw ← nat.cast_one; exact nat.cast_le.2 hn) h)
             ... ≤ _ : by simp [log, arg_le_pi]⟩),
 by rw [← cpow_nat_cast, ← cpow_mul _ h.1 h.2,
-    inv_mul_cancel (show (n : ℂ) ≠ 0, from nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 hn)),
+    inv_mul_cancel (show (n : ℂ) ≠ 0, from nat.cast_ne_zero.2 (pos_iff_ne_zero.1 hn)),
     cpow_one]
 
 end complex
@@ -415,12 +415,12 @@ by rw [rpow_def_of_pos hx, exp_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, lo
 
 lemma pow_nat_rpow_nat_inv {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : 0 < n) :
   (x ^ n) ^ (n⁻¹ : ℝ) = x :=
-have hn0 : (n : ℝ) ≠ 0, by simpa [nat.pos_iff_ne_zero] using hn,
+have hn0 : (n : ℝ) ≠ 0, by simpa [pos_iff_ne_zero] using hn,
 by rw [← rpow_nat_cast, ← rpow_mul hx, mul_inv_cancel hn0, rpow_one]
 
 lemma rpow_nat_inv_pow_nat {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : 0 < n) :
   (x ^ (n⁻¹ : ℝ)) ^ n = x :=
-have hn0 : (n : ℝ) ≠ 0, by simpa [nat.pos_iff_ne_zero] using hn,
+have hn0 : (n : ℝ) ≠ 0, by simpa [pos_iff_ne_zero] using hn,
 by rw [← rpow_nat_cast, ← rpow_mul hx, inv_mul_cancel hn0, rpow_one]
 
 section prove_rpow_is_continuous
@@ -891,7 +891,7 @@ nnreal.eq $ real.rpow_one _
 nnreal.eq $ real.one_rpow _
 
 lemma rpow_add {x : ℝ≥0} (hx : x ≠ 0) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z :=
-nnreal.eq $ real.rpow_add (zero_lt_iff_ne_zero.2 hx) _ _
+nnreal.eq $ real.rpow_add (pos_iff_ne_zero.2 hx) _ _
 
 lemma rpow_add' (x : ℝ≥0) {y z : ℝ} (h : y + z ≠ 0) : x ^ (y + z) = x ^ y * x ^ z :=
 nnreal.eq $ real.rpow_add' x.2 h
@@ -906,7 +906,7 @@ lemma rpow_neg_one (x : ℝ≥0) : x ^ (-1 : ℝ) = x ⁻¹ :=
 by simp [rpow_neg]
 
 lemma rpow_sub {x : ℝ≥0} (hx : x ≠ 0) (y z : ℝ) : x ^ (y - z) = x ^ y / x ^ z :=
-nnreal.eq $ real.rpow_sub (zero_lt_iff_ne_zero.2 hx) y z
+nnreal.eq $ real.rpow_sub (pos_iff_ne_zero.2 hx) y z
 
 lemma rpow_sub' (x : ℝ≥0) {y z : ℝ} (h : y - z ≠ 0) :
   x ^ (y - z) = x ^ y / x ^ z :=
diff --git a/src/analysis/special_functions/trigonometric.lean b/src/analysis/special_functions/trigonometric.lean
index 98e03e0e8880c..3241e9824a1bb 100644
--- a/src/analysis/special_functions/trigonometric.lean
+++ b/src/analysis/special_functions/trigonometric.lean
@@ -1789,7 +1789,7 @@ lemma times_cont_diff_on_arcsin {n : with_top ℕ} :
 lemma times_cont_diff_at_arcsin_iff {x : ℝ} {n : with_top ℕ} :
   times_cont_diff_at ℝ n arcsin x ↔ n = 0 ∨ (x ≠ -1 ∧ x ≠ 1) :=
 ⟨λ h, or_iff_not_imp_left.2 $ λ hn, differentiable_at_arcsin.1 $ h.differentiable_at $
-  with_top.one_le_iff_pos.2 (zero_lt_iff_ne_zero.2 hn),
+  with_top.one_le_iff_pos.2 (pos_iff_ne_zero.2 hn),
   λ h, h.elim (λ hn, hn.symm ▸ (times_cont_diff_zero.2 continuous_arcsin).times_cont_diff_at) $
     λ hx, times_cont_diff_at_arcsin hx.1 hx.2⟩
 
@@ -2217,7 +2217,7 @@ begin
   { use 0, simp only [hx, zero_pow_eq_zero, hn] },
   { use exp (log x / n),
     rw [← exp_nat_mul, mul_div_cancel', exp_log hx],
-    exact_mod_cast (nat.pos_iff_ne_zero.mp hn) }
+    exact_mod_cast (pos_iff_ne_zero.mp hn) }
 end
 
 lemma exists_eq_mul_self (x : ℂ) : ∃ z, x = z * z :=
@@ -2614,7 +2614,7 @@ end
 
 lemma surj_on_tan : surj_on tan (Ioo (-(π / 2)) (π / 2)) univ :=
 have _ := neg_lt_self pi_div_two_pos,
-continuous_on_tan_Ioo.surj_on_of_tendsto (nonempty_Ioo.2 this) 
+continuous_on_tan_Ioo.surj_on_of_tendsto (nonempty_Ioo.2 this)
   (by simp [tendsto_tan_neg_pi_div_two, this]) (by simp [tendsto_tan_pi_div_two, this])
 
 lemma tan_surjective : function.surjective tan :=
diff --git a/src/combinatorics/composition.lean b/src/combinatorics/composition.lean
index e7c83b2f353c9..60780f93ce12d 100644
--- a/src/combinatorics/composition.lean
+++ b/src/combinatorics/composition.lean
@@ -279,7 +279,7 @@ begin
   have i_pos : (0 : ℕ) < i,
   { by_contradiction i_pos,
     push_neg at i_pos,
-    simp [le_zero_iff_eq.mp i_pos, c.size_up_to_zero] at H,
+    simp [nonpos_iff_eq_zero.mp i_pos, c.size_up_to_zero] at H,
     exact nat.not_succ_le_zero j H },
   let i₁ := (i : ℕ).pred,
   have i₁_lt_i : i₁ < i := nat.pred_lt (ne_of_gt i_pos),
diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean
index b80215a7e9510..9f4afaa34f38d 100644
--- a/src/data/complex/exponential.lean
+++ b/src/data/complex/exponential.lean
@@ -434,7 +434,7 @@ have hj : ∀ j : ℕ, ∑ m in range j, (x + y) ^ m / m! =
       rw [add_pow, div_eq_mul_inv, sum_mul],
       refine finset.sum_congr rfl (λ i hi, _),
       have h₁ : (m.choose i : ℂ) ≠ 0 := nat.cast_ne_zero.2
-        (nat.pos_iff_ne_zero.1 (nat.choose_pos (nat.le_of_lt_succ (mem_range.1 hi)))),
+        (pos_iff_ne_zero.1 (nat.choose_pos (nat.le_of_lt_succ (mem_range.1 hi)))),
       have h₂ := nat.choose_mul_factorial_mul_factorial (nat.le_of_lt_succ $ finset.mem_range.1 hi),
       rw [← h₂, nat.cast_mul, nat.cast_mul, mul_inv', mul_inv'],
       simp only [mul_left_comm (m.choose i : ℂ), mul_assoc, mul_left_comm (m.choose i : ℂ)⁻¹,
@@ -1188,11 +1188,11 @@ calc ∑ m in filter (λ k, n ≤ k) (range j), (1 / m! : α)
   by simp [mul_inv', mul_sum.symm, sum_mul.symm, -nat.factorial_succ, mul_comm, inv_pow']
 ... = (n.succ - n.succ * n.succ⁻¹ ^ (j - n)) / (n! * n) :
   have h₁ : (n.succ : α) ≠ 1, from @nat.cast_one α _ _ ▸ mt nat.cast_inj.1
-        (mt nat.succ.inj (nat.pos_iff_ne_zero.1 hn)),
+        (mt nat.succ.inj (pos_iff_ne_zero.1 hn)),
   have h₂ : (n.succ : α) ≠ 0, from nat.cast_ne_zero.2 (nat.succ_ne_zero _),
   have h₃ : (n! * n : α) ≠ 0,
-    from mul_ne_zero (nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 (nat.factorial_pos _)))
-    (nat.cast_ne_zero.2 (nat.pos_iff_ne_zero.1 hn)),
+    from mul_ne_zero (nat.cast_ne_zero.2 (pos_iff_ne_zero.1 (nat.factorial_pos _)))
+    (nat.cast_ne_zero.2 (pos_iff_ne_zero.1 hn)),
   have h₄ : (n.succ - 1 : α) = n, by simp,
   by rw [← geom_series_def, geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃,
       mul_comm _ (n! * n : α), ← mul_assoc (n!⁻¹ : α), ← mul_inv_rev', h₄,
diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
index 5c7b316cf3d22..a7f2676c0448a 100644
--- a/src/data/finset/basic.lean
+++ b/src/data/finset/basic.lean
@@ -1850,7 +1850,7 @@ card_image_of_inj_on $ λ x _ y _ h, H h
 
 lemma fiber_card_ne_zero_iff_mem_image (s : finset α) (f : α → β) [decidable_eq β] (y : β) :
   (s.filter (λ x, f x = y)).card ≠ 0 ↔ y ∈ s.image f :=
-by { rw [←zero_lt_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image] }
+by { rw [←pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image] }
 
 @[simp] lemma card_map {α β} (f : α ↪ β) {s : finset α} : (s.map f).card = s.card :=
 multiset.card_map _ _
diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index 12ccc86ced2ee..1b32bcf240a24 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -3348,7 +3348,7 @@ begin
   induction m with m IH generalizing L n,
   { simp only [min_eq_left, eq_self_iff_true, nat.zero_le, take] },
   { cases n,
-    { simp only [nat.nat_zero_eq_zero, le_zero_iff_eq, take, take_nil],
+    { simp only [nat.nat_zero_eq_zero, nonpos_iff_eq_zero, take, take_nil],
       split,
       { cases L,
         { exact absurd hm (not_lt_of_le m.succ.zero_le) },
diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean
index df3bd158a7943..9e529a0cff8c9 100644
--- a/src/data/mv_polynomial/basic.lean
+++ b/src/data/mv_polynomial/basic.lean
@@ -931,7 +931,7 @@ begin
   obtain ⟨i, hi, hgi⟩ : ∃ i ∈ d.support, g i = 0 := h d (finsupp.mem_support_iff.mp hd),
   rw [eval₂_hom_monomial, finsupp.prod, finset.prod_eq_zero hi, mul_zero],
   rw [hgi, zero_pow],
-  rwa [nat.pos_iff_ne_zero, ← finsupp.mem_support_iff]
+  rwa [pos_iff_ne_zero, ← finsupp.mem_support_iff]
 end
 
 lemma aeval_eq_zero [algebra R S₂] (f : σ → S₂) (φ : mv_polynomial σ R)
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
index 7f1de25fd136b..8558562657152 100644
--- a/src/data/nat/basic.lean
+++ b/src/data/nat/basic.lean
@@ -168,9 +168,6 @@ iff.intro
 
 /-! ### Equalities and inequalities involving zero and one -/
 
-theorem pos_iff_ne_zero : 0 < n ↔ n ≠ 0 :=
-⟨ne_of_gt, nat.pos_of_ne_zero⟩
-
 lemma one_lt_iff_ne_zero_and_ne_one : ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n ≠ 1
 | 0     := dec_trivial
 | 1     := dec_trivial
@@ -1271,7 +1268,7 @@ by simp [find_eq_iff]
 
 @[simp] lemma find_pos {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :
   0 < nat.find h ↔ ¬ p 0 :=
-by rw [nat.pos_iff_ne_zero, not_iff_not, nat.find_eq_zero]
+by rw [pos_iff_ne_zero, not_iff_not, nat.find_eq_zero]
 
 end find
 
@@ -1301,7 +1298,7 @@ lemma find_greatest_eq_iff {b m} :
 begin
   induction b with b ihb generalizing m,
   { rw [eq_comm, iff.comm],
-    simp only [le_zero_iff_eq, ne.def, and_iff_left_iff_imp, find_greatest_zero],
+    simp only [nonpos_iff_eq_zero, ne.def, and_iff_left_iff_imp, find_greatest_zero],
     rintro rfl,
     exact ⟨λ h, (h rfl).elim, λ n hlt heq, (hlt.ne heq.symm).elim⟩ },
   { by_cases hb : P (b + 1),
diff --git a/src/data/nat/cast.lean b/src/data/nat/cast.lean
index 9b3a98b65dc6c..b10551a4d43e3 100644
--- a/src/data/nat/cast.lean
+++ b/src/data/nat/cast.lean
@@ -102,7 +102,7 @@ show ((m * n : ℕ) : α) + m = m * (n + 1), by rw [cast_mul n, left_distrib, mu
 begin
   rcases n_dvd with ⟨k, rfl⟩,
   have : n ≠ 0, {rintro rfl, simpa using n_nonzero},
-  rw nat.mul_div_cancel_left _ (nat.pos_iff_ne_zero.2 this),
+  rw nat.mul_div_cancel_left _ (pos_iff_ne_zero.2 this),
   rw [nat.cast_mul, mul_div_cancel_left _ n_nonzero],
 end
 
diff --git a/src/data/nat/digits.lean b/src/data/nat/digits.lean
index 714654a779a9d..f93cb193dddc8 100644
--- a/src/data/nat/digits.lean
+++ b/src/data/nat/digits.lean
@@ -302,10 +302,10 @@ begin
   have hnpos : 0 < n := nat.pos_of_ne_zero hn,
   by_cases hnb : n < b + 2,
   { simp_rw [digits_of_lt b.succ.succ n hnpos hnb],
-    exact nat.pos_iff_ne_zero.mp hnpos },
+    exact pos_iff_ne_zero.mp hnpos },
   { rw digits_last (show 2 ≤ b + 2, from dec_trivial) hnpos,
     refine IH _ (nat.div_lt_self hnpos dec_trivial) _,
-    { rw ←nat.pos_iff_ne_zero,
+    { rw ←pos_iff_ne_zero,
       exact nat.div_pos (le_of_not_lt hnb) dec_trivial } },
 end
 
@@ -406,7 +406,7 @@ begin
     list.length_init, of_digits_singleton, add_comm (l.length - 1), pow_add, pow_one],
   apply nat.mul_le_mul_left,
   refine le_trans _ (nat.le_add_left _ _),
-  have : 0 < l.last hl, { rwa [nat.pos_iff_ne_zero] },
+  have : 0 < l.last hl, { rwa [pos_iff_ne_zero] },
   convert nat.mul_le_mul_left _ this, rw [mul_one]
 end
 
diff --git a/src/data/nat/fib.lean b/src/data/nat/fib.lean
index b03780b68d800..1f2cda4f49e59 100644
--- a/src/data/nat/fib.lean
+++ b/src/data/nat/fib.lean
@@ -93,7 +93,7 @@ begin
     rw fib_succ_succ,
     suffices : 1 + (n' + 1) ≤ fib n' + fib (n' + 1), by rwa [nat.succ_eq_add_one, add_comm],
     have : n' ≠ 0, by { intro h, have : 5 ≤ 1, by rwa h at five_le_n, norm_num at this },
-    have : 1 ≤ fib n', from nat.succ_le_of_lt (fib_pos $ zero_lt_iff_ne_zero.mpr this),
+    have : 1 ≤ fib n', from nat.succ_le_of_lt (fib_pos $ pos_iff_ne_zero.mpr this),
     mono }
 end
 
@@ -129,12 +129,12 @@ begin
   { rw h, simp },
   replace h := nat.succ_pred_eq_of_pos h, rw [← h, succ_eq_add_one],
   calc gcd (fib m) (fib (n.pred + 1 + m))
-        = gcd (fib m) (fib (n.pred) * (fib m) + fib (n.pred + 1) * fib (m + 1)) : 
+        = gcd (fib m) (fib (n.pred) * (fib m) + fib (n.pred + 1) * fib (m + 1)) :
     by { rw fib_add n.pred _, ring }
-    ... = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) : 
+    ... = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) :
     by rw [add_comm, gcd_add_mul_self (fib m) _ (fib (n.pred))]
-    ... = gcd (fib m) (fib (n.pred + 1)) : 
-    coprime.gcd_mul_right_cancel_right 
+    ... = gcd (fib m) (fib (n.pred + 1)) :
+    coprime.gcd_mul_right_cancel_right
       (fib (n.pred + 1)) (coprime.symm (fib_coprime_fib_succ m))
 end
 
@@ -142,7 +142,7 @@ lemma gcd_fib_add_mul_self (m n : ℕ) : ∀ k, gcd (fib m) (fib (n + k * m)) =
 | 0     := by simp
 | (k+1) := by rw [← gcd_fib_add_mul_self k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]
 
-/-- `fib n` is a strong divisibility sequence, 
+/-- `fib n` is a strong divisibility sequence,
   see https://proofwiki.org/wiki/GCD_of_Fibonacci_Numbers -/
 lemma fib_gcd (m n : ℕ) : fib (gcd m n) = gcd (fib m) (fib n) :=
 begin
diff --git a/src/data/nat/prime.lean b/src/data/nat/prime.lean
index 089d1dcdaad17..38fff598fa0b9 100644
--- a/src/data/nat/prime.lean
+++ b/src/data/nat/prime.lean
@@ -624,7 +624,7 @@ def min_fac_helper (n k : ℕ) : Prop :=
 0 < k ∧ bit1 k ≤ nat.min_fac (bit1 n)
 
 theorem min_fac_helper.n_pos {n k : ℕ} (h : min_fac_helper n k) : 0 < n :=
-nat.pos_iff_ne_zero.2 $ λ e,
+pos_iff_ne_zero.2 $ λ e,
 by rw e at h; exact not_le_of_lt (nat.bit1_lt h.1) h.2
 
 lemma min_fac_ne_bit0 {n k : ℕ} : nat.min_fac (bit1 n) ≠ bit0 k :=
diff --git a/src/data/padics/padic_norm.lean b/src/data/padics/padic_norm.lean
index 64011a8e6dae6..50d5e71656b94 100644
--- a/src/data/padics/padic_norm.lean
+++ b/src/data/padics/padic_norm.lean
@@ -446,7 +446,7 @@ open_locale big_operators
 lemma prod_pow_prime_padic_val_nat (n : nat) (hn : n ≠ 0) (m : nat) (pr : n < m) :
   ∏ p in finset.filter nat.prime (finset.range m), p ^ (padic_val_nat p n) = n :=
 begin
-  rw ← nat.pos_iff_ne_zero at hn,
+  rw ← pos_iff_ne_zero at hn,
   have H : (factors n : multiset ℕ).prod = n,
   { rw [multiset.coe_prod, prod_factors hn], },
   rw finset.prod_multiset_count at H,
diff --git a/src/data/pnat/basic.lean b/src/data/pnat/basic.lean
index a235d1e72c730..87856d143cd1b 100644
--- a/src/data/pnat/basic.lean
+++ b/src/data/pnat/basic.lean
@@ -362,7 +362,7 @@ theorem dvd_one_iff (n : ℕ+) : n ∣ 1 ↔ n = 1 :=
 
 lemma pos_of_div_pos {n : ℕ+} {a : ℕ} (h : a ∣ n) : 0 < a :=
 begin
-  apply zero_lt_iff_ne_zero.2,
+  apply pos_iff_ne_zero.2,
   intro hzero,
   rw hzero at h,
   exact pnat.ne_zero n (eq_zero_of_zero_dvd h)
diff --git a/src/data/polynomial/degree/definitions.lean b/src/data/polynomial/degree/definitions.lean
index f4920aaaced2d..e90f102c640a2 100644
--- a/src/data/polynomial/degree/definitions.lean
+++ b/src/data/polynomial/degree/definitions.lean
@@ -683,7 +683,7 @@ lemma degree_nonneg_iff_ne_zero : 0 ≤ degree p ↔ p ≠ 0 :=
   λ hp0, le_of_not_gt (λ h, by simp [gt, degree_eq_bot, *] at *)⟩
 
 lemma nat_degree_eq_zero_iff_degree_le_zero : p.nat_degree = 0 ↔ p.degree ≤ 0 :=
-by rw [← le_zero_iff_eq, nat_degree_le_iff_degree_le, with_bot.coe_zero]
+by rw [← nonpos_iff_eq_zero, nat_degree_le_iff_degree_le, with_bot.coe_zero]
 
 theorem degree_le_iff_coeff_zero (f : polynomial R) (n : with_bot ℕ) :
   degree f ≤ n ↔ ∀ m : ℕ, n < m → coeff f m = 0 :=
diff --git a/src/data/polynomial/degree/trailing_degree.lean b/src/data/polynomial/degree/trailing_degree.lean
index 520499a864938..530497d260836 100644
--- a/src/data/polynomial/degree/trailing_degree.lean
+++ b/src/data/polynomial/degree/trailing_degree.lean
@@ -170,7 +170,7 @@ lemma trailing_degree_one_le : (0 : with_top ℕ) ≤ trailing_degree (1 : polyn
 by rw [← C_1]; exact le_trailing_degree_C
 
 @[simp] lemma nat_trailing_degree_C (a : R) : nat_trailing_degree (C a) = 0 :=
-le_zero_iff_eq.1 nat_trailing_degree_monomial_le
+nonpos_iff_eq_zero.1 nat_trailing_degree_monomial_le
 
 @[simp] lemma nat_trailing_degree_one : nat_trailing_degree (1 : polynomial R) = 0 :=
 nat_trailing_degree_C 1
diff --git a/src/data/polynomial/reverse.lean b/src/data/polynomial/reverse.lean
index 329316d1128e5..9c5bed695fe3b 100644
--- a/src/data/polynomial/reverse.lean
+++ b/src/data/polynomial/reverse.lean
@@ -207,7 +207,7 @@ begin
   { have : coeff f 1 = 0 := coeff_eq_zero_of_nat_degree_lt (by simp only [hf, zero_lt_one]),
     simp [*, rev_at] },
   { rw rev_at_le,
-    exact nat.succ_le_iff.2 (zero_lt_iff_ne_zero.2 hf) }
+    exact nat.succ_le_iff.2 (pos_iff_ne_zero.2 hf) }
 end
 
 end polynomial
diff --git a/src/data/rat/floor.lean b/src/data/rat/floor.lean
index df905d3fd258c..01eb966c96aaf 100644
--- a/src/data/rat/floor.lean
+++ b/src/data/rat/floor.lean
@@ -56,7 +56,7 @@ begin
         by rwa [n_eq_c_mul_num, d_eq_c_mul_denom],
       suffices : c > 0, by solve_by_elim [int.mul_div_mul_of_pos],
       have q_denom_mul_c_pos : (0 : ℤ) < q.denom * c, by
-      { have : (d : ℤ) > 0, by exact_mod_cast (nat.pos_iff_ne_zero.elim_right d_ne_zero),
+      { have : (d : ℤ) > 0, by exact_mod_cast (pos_iff_ne_zero.elim_right d_ne_zero),
         rwa [d_eq_c_mul_denom, mul_comm] at this },
       suffices : (0 : ℤ) ≤ q.denom, from pos_of_mul_pos_left q_denom_mul_c_pos this,
       exact_mod_cast (le_of_lt q.pos) } }
diff --git a/src/data/rat/sqrt.lean b/src/data/rat/sqrt.lean
index af6c6befa0d08..11f75f9180f76 100644
--- a/src/data/rat/sqrt.lean
+++ b/src/data/rat/sqrt.lean
@@ -27,7 +27,7 @@ theorem exists_mul_self (x : ℚ) : (∃ q, q * q = x) ↔ rat.sqrt x * rat.sqrt
 
 theorem sqrt_nonneg (q : ℚ) : 0 ≤ rat.sqrt q :=
 nonneg_iff_zero_le.1 $ (mk_nonneg _ $ int.coe_nat_pos.2 $
-nat.pos_of_ne_zero $ λ H, nat.pos_iff_ne_zero.1 q.pos $ nat.sqrt_eq_zero.1 H).2
+nat.pos_of_ne_zero $ λ H, pos_iff_ne_zero.1 q.pos $ nat.sqrt_eq_zero.1 H).2
 $ int.coe_nat_nonneg _
 
 end rat
diff --git a/src/data/real/cardinality.lean b/src/data/real/cardinality.lean
index 6d2a74d0172a4..eca413c7e62fb 100644
--- a/src/data/real/cardinality.lean
+++ b/src/data/real/cardinality.lean
@@ -165,7 +165,7 @@ begin
   { convert Iic_union_Ioi, exact Iio_union_right },
   rw ← hu,
   refine lt_of_le_of_lt (mk_union_le _ _) _,
-  refine lt_of_le_of_lt (add_le_add_right _ (mk_union_le _ _)) _,
+  refine lt_of_le_of_lt (add_le_add_right (mk_union_le _ _) _) _,
   have h2 : (λ x, a + a - x) '' Ioi a = Iio a,
   { convert image_const_sub_Ioi _ _, simp },
   rw ← h2,
diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean
index a1262b7d9f1d5..e22f28bdd1961 100644
--- a/src/data/real/ennreal.lean
+++ b/src/data/real/ennreal.lean
@@ -326,7 +326,7 @@ begin
 end
 
 @[simp] lemma mul_pos : 0 < a * b ↔ 0 < a ∧ 0 < b :=
-by simp only [zero_lt_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
+by simp only [pos_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
 
 lemma pow_eq_top : ∀ n:ℕ, a^n=∞ → a=∞
 | 0 := by simp
@@ -384,7 +384,7 @@ begin
 end
 
 @[simp] lemma max_eq_zero_iff : max a b = 0 ↔ a = 0 ∧ b = 0 :=
-by simp only [le_zero_iff_eq.symm, max_le_iff]
+by simp only [nonpos_iff_eq_zero.symm, max_le_iff]
 
 @[simp] lemma max_zero_left : max 0 a = a := max_eq_right (zero_le a)
 @[simp] lemma max_zero_right : max a 0 = a := max_eq_left (zero_le a)
@@ -397,7 +397,7 @@ protected lemma pow_pos : 0 < a → ∀ n : ℕ, 0 < a^n :=
   canonically_ordered_semiring.pow_pos
 
 protected lemma pow_ne_zero : a ≠ 0 → ∀ n : ℕ, a^n ≠ 0 :=
-by simpa only [zero_lt_iff_ne_zero] using ennreal.pow_pos
+by simpa only [pos_iff_ne_zero] using ennreal.pow_pos
 
 @[simp] lemma not_lt_zero : ¬ a < 0 := by simp
 
@@ -564,7 +564,7 @@ lemma mul_le_mul_left : a ≠ 0 → a ≠ ∞ → (a * b ≤ a * c ↔ b ≤ c)
 begin
   cases a; cases b; cases c;
     simp [none_eq_top, some_eq_coe, mul_top, top_mul, -coe_mul, coe_mul.symm] {contextual := tt},
-  assume h, exact mul_le_mul_left (zero_lt_iff_ne_zero.2 h)
+  assume h, exact mul_le_mul_left (pos_iff_ne_zero.2 h)
 end
 
 lemma mul_le_mul_right : c ≠ 0 → c ≠ ∞ → (a * c ≤ b * c ↔ a ≤ b) :=
@@ -663,11 +663,11 @@ ennreal.sub_le_iff_le_add.2 $ by { rw add_comm, exact ennreal.sub_le_iff_le_add.
 protected lemma sub_lt_sub_self : a ≠ ∞ → a ≠ 0 → 0 < b → a - b < a :=
 match a, b with
 | none, _ := by { have := none_eq_top, assume h, contradiction }
-| (some a), none := by {intros, simp only [none_eq_top, sub_infty, zero_lt_iff_ne_zero], assumption}
+| (some a), none := by {intros, simp only [none_eq_top, sub_infty, pos_iff_ne_zero], assumption}
 | (some a), (some b) :=
   begin
     simp only [some_eq_coe, coe_sub.symm, coe_pos, coe_eq_zero, coe_lt_coe, ne.def],
-    assume h₁ h₂, apply nnreal.sub_lt_self, exact zero_lt_iff_ne_zero.2 h₂
+    assume h₁ h₂, apply nnreal.sub_lt_self, exact pos_iff_ne_zero.2 h₂
   end
 end
 
@@ -885,7 +885,7 @@ begin
     zero_pow, top_pow, nat.zero_lt_succ] at *,
   rw [← coe_inv h, ← coe_pow, ← coe_inv, nnreal.inv_pow, coe_pow],
   rw [← ne.def] at h,
-  rw [← zero_lt_iff_ne_zero] at *,
+  rw [← pos_iff_ne_zero] at *,
   apply pow_pos h
 end
 
@@ -907,7 +907,7 @@ inv_zero ▸ inv_eq_inv
 lemma inv_ne_top : a⁻¹ ≠ ∞ ↔ a ≠ 0 := by simp
 
 @[simp] lemma inv_lt_top {x : ennreal} : x⁻¹ < ∞ ↔ 0 < x :=
-by { simp only [lt_top_iff_ne_top, inv_ne_top, zero_lt_iff_ne_zero] }
+by { simp only [lt_top_iff_ne_top, inv_ne_top, pos_iff_ne_zero] }
 
 lemma div_lt_top {x y : ennreal} (h1 : x < ∞) (h2 : 0 < y) : x / y < ∞ :=
 mul_lt_top h1 (inv_lt_top.mpr h2)
@@ -918,7 +918,7 @@ inv_top ▸ inv_eq_inv
 lemma inv_ne_zero : a⁻¹ ≠ 0 ↔ a ≠ ∞ := by simp
 
 @[simp] lemma inv_pos : 0 < a⁻¹ ↔ a ≠ ∞ :=
-zero_lt_iff_ne_zero.trans inv_ne_zero
+pos_iff_ne_zero.trans inv_ne_zero
 
 @[simp] lemma inv_lt_inv : a⁻¹ < b⁻¹ ↔ b < a :=
 begin
@@ -930,7 +930,7 @@ begin
       cases eq_or_lt_of_le (zero_le b) with hb hb,
     { subst a, subst b, simp },
     { subst a, simp },
-    { subst b, simp [zero_lt_iff_ne_zero, lt_top_iff_ne_top, inv_ne_top] },
+    { subst b, simp [pos_iff_ne_zero, lt_top_iff_ne_top, inv_ne_top] },
     { rw [← coe_inv (ne_of_gt ha), ← coe_inv (ne_of_gt hb), coe_lt_coe, coe_lt_coe],
       simp only [nnreal.coe_lt_coe.symm] at *,
       exact inv_lt_inv ha hb } }
@@ -1077,7 +1077,7 @@ by rw [div_def, ← mul_add, inv_two_add_inv_two, mul_one]
 by simp [div_def, mul_eq_zero]
 
 @[simp] lemma div_pos_iff : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞ :=
-by simp [zero_lt_iff_ne_zero, not_or_distrib]
+by simp [pos_iff_ne_zero, not_or_distrib]
 
 lemma half_pos {a : ennreal} (h : 0 < a) : 0 < a / 2 :=
 by simp [ne_of_gt h]
diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
index 5106ed7d6ff91..ac1c8c3ccaf1a 100644
--- a/src/data/real/nnreal.lean
+++ b/src/data/real/nnreal.lean
@@ -516,7 +516,7 @@ by simp only [nnreal.div_def, finset.sum_mul]
 inv_eq_zero
 
 @[simp] lemma inv_pos {r : ℝ≥0} : 0 < r⁻¹ ↔ 0 < r :=
-by simp [zero_lt_iff_ne_zero]
+by simp [pos_iff_ne_zero]
 
 lemma div_pos {r p : ℝ≥0}  (hr : 0 < r) (hp : 0 < p) : 0 < r / p :=
 mul_pos hr (inv_pos.2 hp)
@@ -551,16 +551,16 @@ by rw [mul_comm, div_mul_cancel _ h]
 @[simp] lemma inv_inv {r : ℝ≥0} : r⁻¹⁻¹ = r := nnreal.eq (inv_inv' _)
 
 @[simp] lemma inv_le {r p : ℝ≥0} (h : r ≠ 0) : r⁻¹ ≤ p ↔ 1 ≤ r * p :=
-by rw [← mul_le_mul_left (zero_lt_iff_ne_zero.2 h), mul_inv_cancel h]
+by rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h]
 
 lemma inv_le_of_le_mul {r p : ℝ≥0} (h : 1 ≤ r * p) : r⁻¹ ≤ p :=
 by by_cases r = 0; simp [*, inv_le]
 
 @[simp] lemma le_inv_iff_mul_le {r p : ℝ≥0} (h : p ≠ 0) : (r ≤ p⁻¹ ↔ r * p ≤ 1) :=
-by rw [← mul_le_mul_left (zero_lt_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm]
+by rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm]
 
 @[simp] lemma lt_inv_iff_mul_lt {r p : ℝ≥0} (h : p ≠ 0) : (r < p⁻¹ ↔ r * p < 1) :=
-by rw [← mul_lt_mul_left (zero_lt_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm]
+by rw [← mul_lt_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm]
 
 lemma mul_le_iff_le_inv {a b r : ℝ≥0} (hr : r ≠ 0) : r * a ≤ b ↔ a ≤ r⁻¹ * b :=
 have 0 < r, from lt_of_le_of_ne (zero_le r) hr.symm,
@@ -570,7 +570,7 @@ lemma le_div_iff_mul_le {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ a * r
 by rw [div_def, mul_comm, ← mul_le_iff_le_inv hr, mul_comm]
 
 lemma div_le_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a / r ≤ b ↔ a ≤ b * r :=
-@div_le_iff ℝ _ a r b $ zero_lt_iff_ne_zero.2 hr
+@div_le_iff ℝ _ a r b $ pos_iff_ne_zero.2 hr
 
 lemma lt_div_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a < b / r ↔ a * r < b :=
 lt_iff_lt_of_le_iff_le (div_le_iff hr)
@@ -584,7 +584,7 @@ end
 
 lemma le_of_forall_lt_one_mul_le {x y : ℝ≥0} (h : ∀a<1, a * x ≤ y) : x ≤ y :=
 le_of_forall_ge_of_dense $ assume a ha,
-  have hx : x ≠ 0 := zero_lt_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha),
+  have hx : x ≠ 0 := pos_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha),
   have hx' : x⁻¹ ≠ 0, by rwa [(≠), inv_eq_zero],
   have a * x⁻¹ < 1, by rwa [← lt_inv_iff_mul_lt hx', inv_inv],
   have (a * x⁻¹) * x ≤ y, from h _ this,
@@ -607,7 +607,7 @@ by simpa [div_def] using half_lt_self zero_ne_one.symm
 lemma div_lt_iff {a b c : ℝ≥0} (hc : c ≠ 0) : b / c < a ↔ b < a * c :=
 begin
   rw [← nnreal.coe_lt_coe, ← nnreal.coe_lt_coe, nnreal.coe_div, nnreal.coe_mul],
-  exact div_lt_iff (zero_lt_iff_ne_zero.mpr hc)
+  exact div_lt_iff (pos_iff_ne_zero.mpr hc)
 end
 
 lemma div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) : a / b < 1 :=
diff --git a/src/data/zmod/basic.lean b/src/data/zmod/basic.lean
index a6c6826179618..d10f7f2a05cf8 100644
--- a/src/data/zmod/basic.lean
+++ b/src/data/zmod/basic.lean
@@ -381,7 +381,7 @@ lemma cast_hom_bijective [fintype R] (h : fintype.card R = n) :
 begin
   haveI : fact (0 < n) :=
   begin
-    rw [nat.pos_iff_ne_zero],
+    rw [pos_iff_ne_zero],
     unfreezingI { rintro rfl },
     exact fintype.card_eq_zero_iff.mp h 0
   end,
diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 4fb70f1a1d0a6..e6f4ef1b8cbd7 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -541,7 +541,7 @@ theorem irreducible.separable {F : Type u} [field F] [char_zero F] {f : polynomi
   (hf : irreducible f) (hf0 : f ≠ 0) : f.separable :=
 begin
   rw [separable_iff_derivative_ne_zero hf, ne, ← degree_eq_bot, degree_derivative_eq], rintro ⟨⟩,
-  rw [nat.pos_iff_ne_zero, ne, nat_degree_eq_zero_iff_degree_le_zero, degree_le_zero_iff],
+  rw [pos_iff_ne_zero, ne, nat_degree_eq_zero_iff_degree_le_zero, degree_le_zero_iff],
   refine λ hf1, hf.1 _, rw [hf1, is_unit_C, is_unit_iff_ne_zero],
   intro hf2, rw [hf2, C_0] at hf1, exact absurd hf1 hf0
 end
diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean
index cd1e4d610b337..1f4e42afc83ee 100644
--- a/src/group_theory/order_of_element.lean
+++ b/src/group_theory/order_of_element.lean
@@ -491,7 +491,7 @@ lemma card_order_of_eq_totient_aux₂ {d : ℕ} (hd : d ∣ fintype.card α) :
   (univ.filter (λ a : α, order_of a = d)).card = φ d :=
 by_contradiction $ λ h,
 have h0 : (univ.filter (λ a : α , order_of a = d)).card = 0 :=
-  not_not.1 (mt nat.pos_iff_ne_zero.2 (mt (card_order_of_eq_totient_aux₁ hn hd) h)),
+  not_not.1 (mt pos_iff_ne_zero.2 (mt (card_order_of_eq_totient_aux₁ hn hd) h)),
 let c := fintype.card α in
 have hc0 : 0 < c, from fintype.card_pos_iff.2 ⟨1⟩,
 lt_irrefl c $
@@ -513,7 +513,7 @@ lt_irrefl c $
         (λ h, by rw h))
   ... < φ d + ∑ m in ((range c.succ).filter (∣ c)).erase d, φ m :
     lt_add_of_pos_left _ (totient_pos (nat.pos_of_ne_zero
-      (λ h, nat.pos_iff_ne_zero.1 hc0 (eq_zero_of_zero_dvd $ h ▸ hd))))
+      (λ h, pos_iff_ne_zero.1 hc0 (eq_zero_of_zero_dvd $ h ▸ hd))))
   ... = ∑ m in insert d (((range c.succ).filter (∣ c)).erase d), φ m : eq.symm (sum_insert (by simp))
   ... = ∑ m in (range c.succ).filter (∣ c), φ m : finset.sum_congr
       (finset.insert_erase (mem_filter.2 ⟨mem_range.2 (lt_succ_of_le (le_of_dvd hc0 hd)), hd⟩)) (λ _ _, rfl)
diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean
index dbec094ed408a..85078612474d6 100644
--- a/src/linear_algebra/dimension.lean
+++ b/src/linear_algebra/dimension.lean
@@ -287,7 +287,7 @@ by classical; exact let ⟨f⟩ := quotient_prod_linear_equiv p in dim_prod.symm
 
 theorem dim_quotient_le (p : submodule K V) :
   dim K p.quotient ≤ dim K V :=
-by { rw ← dim_quotient_add_dim p, exact cardinal.le_add_right _ _ }
+by { rw ← dim_quotient_add_dim p, exact self_le_add_right _ _ }
 
 /-- rank-nullity theorem -/
 theorem dim_range_add_dim_ker (f : V →ₗ[K] V₁) : dim K f.range + dim K f.ker = dim K V :=
@@ -297,7 +297,7 @@ begin
 end
 
 lemma dim_range_le (f : V →ₗ[K] V₁) : dim K f.range ≤ dim K V :=
-by rw ← dim_range_add_dim_ker f; exact le_add_right (le_refl _)
+by { rw ← dim_range_add_dim_ker f, exact self_le_add_right _ _ }
 
 lemma dim_map_le (f : V →ₗ V₁) (p : submodule K V) : dim K (p.map f) ≤ dim K p :=
 begin
@@ -316,13 +316,13 @@ lemma dim_eq_of_surjective (f : V →ₗ[K] V₁) (h : surjective f) : dim K V =
 by rw [← dim_range_add_dim_ker f, ← dim_range_of_surjective f h]
 
 lemma dim_le_of_surjective (f : V →ₗ[K] V₁) (h : surjective f) : dim K V₁ ≤ dim K V :=
-by rw [dim_eq_of_surjective f h]; refine le_add_right (le_refl _)
+by { rw [dim_eq_of_surjective f h], refine self_le_add_right _ _ }
 
 lemma dim_eq_of_injective (f : V →ₗ[K] V₁) (h : injective f) : dim K V = dim K f.range :=
 by rw [← dim_range_add_dim_ker f, linear_map.ker_eq_bot.2 h]; simp [dim_bot]
 
 lemma dim_submodule_le (s : submodule K V) : dim K s ≤ dim K V :=
-by { rw ← dim_quotient_add_dim s, exact cardinal.le_add_left _ _ }
+by { rw ← dim_quotient_add_dim s, exact self_le_add_left _ _ }
 
 lemma dim_le_of_injective (f : V →ₗ[K] V₁) (h : injective f) :
   dim K V ≤ dim K V₁ :=
@@ -406,7 +406,7 @@ dim_add_dim_split (of_le le_sup_left) (of_le le_sup_right) (of_le inf_le_left) (
 
 lemma dim_add_le_dim_add_dim (s t : submodule K V) :
   dim K (s ⊔ t : submodule K V) ≤ dim K s + dim K t :=
-by rw [← dim_sup_add_dim_inf_eq]; exact le_add_right (le_refl _)
+by { rw [← dim_sup_add_dim_inf_eq], exact self_le_add_right _ _ }
 
 end
 
@@ -469,7 +469,7 @@ section rank
 def rank (f : V →ₗ[K] V') : cardinal := dim K f.range
 
 lemma rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ dim K V :=
-by rw [← dim_range_add_dim_ker f]; exact le_add_right (le_refl _)
+by { rw [← dim_range_add_dim_ker f], exact self_le_add_right _ _ }
 
 lemma rank_le_range (f : V →ₗ[K] V₁) : rank f ≤ dim K V₁ :=
 dim_submodule_le _
diff --git a/src/measure_theory/bochner_integration.lean b/src/measure_theory/bochner_integration.lean
index 82fcf97123501..148927603d93c 100644
--- a/src/measure_theory/bochner_integration.lean
+++ b/src/measure_theory/bochner_integration.lean
@@ -1269,7 +1269,7 @@ integral_eq_zero_iff_of_nonneg_ae (eventually_of_forall hf) hfi
 
 lemma integral_pos_iff_support_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : integrable f μ) :
   (0 < ∫ x, f x ∂μ) ↔ 0 < μ (function.support f) :=
-by simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, zero_lt_iff_ne_zero, ne.def, @eq_comm ℝ 0,
+by simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, ne.def, @eq_comm ℝ 0,
   integral_eq_zero_iff_of_nonneg_ae hf hfi, filter.eventually_eq, ae_iff, pi.zero_apply,
   function.support]
 
diff --git a/src/measure_theory/content.lean b/src/measure_theory/content.lean
index 0a02c99302a9b..e4a7962137362 100644
--- a/src/measure_theory/content.lean
+++ b/src/measure_theory/content.lean
@@ -105,7 +105,7 @@ lemma inner_content_Sup_nat [t2_space G] {μ : compacts G → ennreal}
 begin
   have h3 : ∀ (t : finset ℕ) (K : ℕ → compacts G), μ (t.sup K) ≤ t.sum (λ i, μ (K i)),
   { intros t K, refine finset.induction_on t _ _,
-    { simp only [h1, le_zero_iff_eq, finset.sum_empty, finset.sup_empty] },
+    { simp only [h1, nonpos_iff_eq_zero, finset.sum_empty, finset.sup_empty] },
     { intros n s hn ih, rw [finset.sup_insert, finset.sum_insert hn],
       exact le_trans (h2 _ _) (add_le_add_left ih _) }},
   refine bsupr_le (λ K hK, _),
diff --git a/src/measure_theory/haar_measure.lean b/src/measure_theory/haar_measure.lean
index b9d230053078d..d5c014af2132d 100644
--- a/src/measure_theory/haar_measure.lean
+++ b/src/measure_theory/haar_measure.lean
@@ -552,7 +552,7 @@ lemma haar_measure_self [locally_compact_space G] {K₀ : positive_compacts G} :
   haar_measure K₀ K₀.1 = 1 :=
 begin
   rw [haar_measure_apply K₀.2.1.is_measurable, ennreal.div_self],
-  { rw [← zero_lt_iff_ne_zero], exact haar_outer_measure_self_pos },
+  { rw [← pos_iff_ne_zero], exact haar_outer_measure_self_pos },
   { exact ne_of_lt (haar_outer_measure_lt_top_of_is_compact K₀.2.1) }
 end
 
@@ -561,7 +561,7 @@ lemma haar_measure_pos_of_is_open [locally_compact_space G] {K₀ : positive_com
 begin
   rw [haar_measure_apply hU.is_measurable, ennreal.div_pos_iff],
   refine ⟨_, ne_of_lt $ haar_outer_measure_lt_top_of_is_compact K₀.2.1⟩,
-  rw [← zero_lt_iff_ne_zero], apply haar_outer_measure_pos_of_is_open hU h2U
+  rw [← pos_iff_ne_zero], apply haar_outer_measure_pos_of_is_open hU h2U
 end
 
 lemma regular_haar_measure [locally_compact_space G] {K₀ : positive_compacts G} :
diff --git a/src/measure_theory/integration.lean b/src/measure_theory/integration.lean
index 70dd4a41af067..1b371bd3e2223 100644
--- a/src/measure_theory/integration.lean
+++ b/src/measure_theory/integration.lean
@@ -965,7 +965,7 @@ begin
     have : (rs.map c) x < ⨆ (n : ℕ), f n x,
     { refine lt_of_lt_of_le (ennreal.coe_lt_coe.2 (_)) (hsf x),
       suffices : r * s x < 1 * s x, simpa [rs],
-      exact mul_lt_mul_of_pos_right ha (zero_lt_iff_ne_zero.2 this) },
+      exact mul_lt_mul_of_pos_right ha (pos_iff_ne_zero.2 this) },
     rcases lt_supr_iff.1 this with ⟨i, hi⟩,
     exact mem_Union.2 ⟨i, le_of_lt hi⟩ },
   have mono : ∀r:ennreal, monotone (λn, (rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a}),
@@ -1255,7 +1255,7 @@ begin
   refine iff.intro (assume h, _) (assume h, _),
   { have : ∀n:ℕ, ∀ᵐ a ∂μ, f a < n⁻¹,
     { assume n,
-      rw [ae_iff, ← le_zero_iff_eq, ← @ennreal.zero_div n⁻¹,
+      rw [ae_iff, ← nonpos_iff_eq_zero, ← @ennreal.zero_div n⁻¹,
         ennreal.le_div_iff_mul_le, mul_comm],
       simp only [not_lt],
       -- TODO: why `rw ← h` fails with "not an equality or an iff"?
@@ -1280,7 +1280,7 @@ end
 
 lemma lintegral_pos_iff_support {f : α → ennreal} (hf : measurable f) :
   0 < ∫⁻ a, f a ∂μ ↔ 0 < μ (function.support f) :=
-by simp [zero_lt_iff_ne_zero, hf, filter.eventually_eq, ae_iff, function.support]
+by simp [pos_iff_ne_zero, hf, filter.eventually_eq, ae_iff, function.support]
 
 /-- Weaker version of the monotone convergence theorem-/
 lemma lintegral_supr_ae {f : ℕ → α → ennreal} (hf : ∀n, measurable (f n))
diff --git a/src/measure_theory/lebesgue_measure.lean b/src/measure_theory/lebesgue_measure.lean
index 525613fa56f82..78474f1f12bd5 100644
--- a/src/measure_theory/lebesgue_measure.lean
+++ b/src/measure_theory/lebesgue_measure.lean
@@ -22,7 +22,7 @@ namespace measure_theory
 def lebesgue_length (s : set ℝ) : ennreal := ⨅a b (h : s ⊆ Ico a b), of_real (b - a)
 
 @[simp] lemma lebesgue_length_empty : lebesgue_length ∅ = 0 :=
-le_zero_iff_eq.1 $ infi_le_of_le 0 $ infi_le_of_le 0 $ by simp
+nonpos_iff_eq_zero.1 $ infi_le_of_le 0 $ infi_le_of_le 0 $ by simp
 
 @[simp] lemma lebesgue_length_Ico (a b : ℝ) :
   lebesgue_length (Ico a b) = of_real (b - a) :=
diff --git a/src/measure_theory/measure_space.lean b/src/measure_theory/measure_space.lean
index c0ea4c62058bf..caacdb4422ba3 100644
--- a/src/measure_theory/measure_space.lean
+++ b/src/measure_theory/measure_space.lean
@@ -192,7 +192,7 @@ ne_empty_iff_nonempty.1 $ λ h', h $ h'.symm ▸ measure_empty
 lemma measure_mono (h : s₁ ⊆ s₂) : μ s₁ ≤ μ s₂ := μ.mono h
 
 lemma measure_mono_null (h : s₁ ⊆ s₂) (h₂ : μ s₂ = 0) : μ s₁ = 0 :=
-le_zero_iff_eq.1 $ h₂ ▸ measure_mono h
+nonpos_iff_eq_zero.1 $ h₂ ▸ measure_mono h
 
 lemma measure_mono_top (h : s₁ ⊆ s₂) (h₁ : μ s₁ = ⊤) : μ s₂ = ⊤ :=
 top_unique $ h₁ ▸ measure_mono h
@@ -663,7 +663,7 @@ end Inf
 
 protected lemma zero_le (μ : measure α) : 0 ≤ μ := bot_le
 
-lemma le_zero_iff_eq' : μ ≤ 0 ↔ μ = 0 :=
+lemma nonpos_iff_eq_zero' : μ ≤ 0 ↔ μ = 0 :=
 μ.zero_le.le_iff_eq
 
 @[simp] lemma measure_univ_eq_zero : μ univ = 0 ↔ μ = 0 :=
@@ -790,7 +790,7 @@ by rw [restrict_apply ht]
 
 lemma restrict_apply_eq_zero' (hs : is_measurable s) : μ.restrict s t = 0 ↔ μ (t ∩ s) = 0 :=
 begin
-  refine ⟨λ h, le_zero_iff_eq.1 (h ▸ le_restrict_apply _ _), λ h, _⟩,
+  refine ⟨λ h, nonpos_iff_eq_zero.1 (h ▸ le_restrict_apply _ _), λ h, _⟩,
   rcases exists_is_measurable_superset_of_null h with ⟨t', htt', ht', ht'0⟩,
   apply measure_mono_null ((inter_subset _ _ _).1 htt'),
   rw [restrict_apply (hs.compl.union ht'), union_inter_distrib_right, compl_inter_self,
@@ -1304,7 +1304,7 @@ end
 ae_eq_bot.trans restrict_eq_zero
 
 @[simp] lemma ae_restrict_ne_bot {s} : (μ.restrict s).ae.ne_bot ↔ 0 < μ s :=
-(not_congr ae_restrict_eq_bot).trans zero_lt_iff_ne_zero.symm
+(not_congr ae_restrict_eq_bot).trans pos_iff_ne_zero.symm
 
 /-- A version of the Borel-Cantelli lemma: if sᵢ is a sequence of measurable sets such that
 ∑ μ sᵢ exists, then for almost all x, x does not belong to almost all sᵢ. -/
@@ -1423,7 +1423,7 @@ variables [has_no_atoms μ]
 
 lemma measure_countable (h : countable s) : μ s = 0 :=
 begin
-  rw [← bUnion_of_singleton s, ← le_zero_iff_eq],
+  rw [← bUnion_of_singleton s, ← nonpos_iff_eq_zero],
   refine le_trans (measure_bUnion_le h _) _,
   simp
 end
@@ -1728,7 +1728,7 @@ lemma sub_def : μ - ν = Inf {d | μ ≤ d + ν} := rfl
 
 lemma sub_eq_zero_of_le (h : μ ≤ ν) : μ - ν = 0 :=
 begin
-  rw [← le_zero_iff_eq', measure.sub_def],
+  rw [← nonpos_iff_eq_zero', measure.sub_def],
   apply @Inf_le (measure α) _ _,
   simp [h],
 end
@@ -1853,7 +1853,7 @@ theorem is_null_measurable.union_null (hs : is_null_measurable μ s) (hz : μ z
   is_null_measurable μ (s ∪ z) :=
 begin
   rcases hs with ⟨t, z', rfl, ht, hz'⟩,
-  exact ⟨t, z' ∪ z, set.union_assoc _ _ _, ht, le_zero_iff_eq.1
+  exact ⟨t, z' ∪ z, set.union_assoc _ _ _, ht, nonpos_iff_eq_zero.1
     (le_trans (measure_union_le _ _) $ by simp [hz, hz'])⟩
 end
 
@@ -1885,7 +1885,7 @@ begin
   refine is_null_measurable_iff.2 ⟨s \ Inter f,
     diff_subset_diff_right (subset_Inter (λ i, (hf i).1)),
     hs.diff (is_measurable.Inter (λ i, (hf i).2.1)),
-    measure_mono_null _ (le_zero_iff_eq.1 $ le_of_not_lt $ λ h, _)⟩,
+    measure_mono_null _ (nonpos_iff_eq_zero.1 $ le_of_not_lt $ λ h, _)⟩,
   { exact Inter f },
   { rw [diff_subset_iff, diff_union_self],
     exact subset.trans (diff_subset _ _) (subset_union_left _ _) },
diff --git a/src/measure_theory/outer_measure.lean b/src/measure_theory/outer_measure.lean
index 917dd98ea3616..f74c7fa524c7f 100644
--- a/src/measure_theory/outer_measure.lean
+++ b/src/measure_theory/outer_measure.lean
@@ -180,7 +180,7 @@ section supremum
 instance : has_Sup (outer_measure α) :=
 ⟨λms, {
   measure_of := λs, ⨆ m ∈ ms, (m : outer_measure α) s,
-  empty      := le_zero_iff_eq.1 $ bsupr_le $ λ m h, le_of_eq m.empty,
+  empty      := nonpos_iff_eq_zero.1 $ bsupr_le $ λ m h, le_of_eq m.empty,
   mono       := assume s₁ s₂ hs, bsupr_le_bsupr $ assume m hm, m.mono hs,
   Union_nat  := assume f, bsupr_le $ assume m hm,
     calc m (⋃i, f i) ≤ (∑' (i : ℕ), m (f i)) : m.Union_nat _
diff --git a/src/measure_theory/simple_func_dense.lean b/src/measure_theory/simple_func_dense.lean
index 7fe2def69820b..f2d8bf38243ff 100644
--- a/src/measure_theory/simple_func_dense.lean
+++ b/src/measure_theory/simple_func_dense.lean
@@ -79,7 +79,7 @@ lemma edist_nearest_pt_le (e : ℕ → α) (x : α) {k N : ℕ} (hk : k ≤ N) :
   edist (nearest_pt e N x) x ≤ edist (e k) x :=
 begin
   induction N with N ihN generalizing k,
-  { simp [le_zero_iff_eq.1 hk, le_refl] },
+  { simp [nonpos_iff_eq_zero.1 hk, le_refl] },
   { simp only [nearest_pt, nearest_pt_ind_succ, map_apply],
     split_ifs,
     { rcases hk.eq_or_lt with rfl|hk,
diff --git a/src/number_theory/pythagorean_triples.lean b/src/number_theory/pythagorean_triples.lean
index be05fbc0e0189..e6c22d425db2a 100644
--- a/src/number_theory/pythagorean_triples.lean
+++ b/src/number_theory/pythagorean_triples.lean
@@ -162,7 +162,7 @@ begin
   obtain ⟨k, x0, y0, k0, h2, rfl, rfl⟩ :
     ∃ (k : ℕ) x0 y0, 0 < k ∧ int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
     int.exists_gcd_one' (nat.pos_of_ne_zero h0),
-  have hk : (k : ℤ) ≠ 0, { norm_cast, rwa nat.pos_iff_ne_zero at k0 },
+  have hk : (k : ℤ) ≠ 0, { norm_cast, rwa pos_iff_ne_zero at k0 },
   rw [int.gcd_mul_right, h2, int.nat_abs_of_nat, one_mul] at h ⊢,
   rw [mul_comm x0, mul_comm y0, mul_iff k hk] at h,
   rwa [int.mul_div_cancel _ hk, int.mul_div_cancel _ hk, int.mul_div_cancel_left _ hk],
diff --git a/src/number_theory/quadratic_reciprocity.lean b/src/number_theory/quadratic_reciprocity.lean
index a5a9326cffc74..5a8d3488911c3 100644
--- a/src/number_theory/quadratic_reciprocity.lean
+++ b/src/number_theory/quadratic_reciprocity.lean
@@ -120,7 +120,7 @@ begin
   { intros a ha, simp only [cast_id, nat_cast_val], },
   { intros _ _ _ _ h, rw units.ext_iff, exact val_injective p h },
   { intros b hb,
-    rw [Ico.mem, nat.succ_le_iff, ← succ_sub hp, succ_sub_one, nat.pos_iff_ne_zero] at hb,
+    rw [Ico.mem, nat.succ_le_iff, ← succ_sub hp, succ_sub_one, pos_iff_ne_zero] at hb,
     refine ⟨units.mk0 b _, finset.mem_univ _, _⟩,
     { assume h, apply hb.1, apply_fun val at h,
       simpa only [val_cast_of_lt hb.right, val_zero] using h },
@@ -144,7 +144,7 @@ lemma Ico_map_val_min_abs_nat_abs_eq_Ico_map_id
   (Ico 1 (p / 2).succ).1.map (λ a, a) :=
 begin
   have he : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2,
-    by simp [nat.lt_succ_iff, nat.succ_le_iff, nat.pos_iff_ne_zero] {contextual := tt},
+    by simp [nat.lt_succ_iff, nat.succ_le_iff, pos_iff_ne_zero] {contextual := tt},
   have hep : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x < p,
     from λ x hx, lt_of_le_of_lt (he hx).2 (nat.div_lt_self hp.pos dec_trivial),
   have hpe : ∀ {x}, x ∈ Ico 1 (p / 2).succ → ¬ p ∣ x,
@@ -153,7 +153,7 @@ begin
     (a * x : zmod p).val_min_abs.nat_abs ∈ Ico 1 (p / 2).succ,
   { assume x hx,
     simp [hap, char_p.cast_eq_zero_iff (zmod p) p, hpe hx, lt_succ_iff, succ_le_iff,
-        nat.pos_iff_ne_zero, nat_abs_val_min_abs_le _], },
+        pos_iff_ne_zero, nat_abs_val_min_abs_le _], },
   have hsurj : ∀ (b : ℕ) (hb : b ∈ Ico 1 (p / 2).succ),
     ∃ x ∈ Ico 1 (p / 2).succ, b = (a * x : zmod p).val_min_abs.nat_abs,
   { assume b hb,
@@ -331,7 +331,7 @@ begin
       { 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,
-    simpa only [this, le_zero_iff_eq, Ico.mem, one_ne_zero, false_and, mem_product] using hx },
+    simpa only [this, nonpos_iff_eq_zero, 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
diff --git a/src/ring_theory/eisenstein_criterion.lean b/src/ring_theory/eisenstein_criterion.lean
index 9dcce2f4139fe..7a79944caecc5 100644
--- a/src/ring_theory/eisenstein_criterion.lean
+++ b/src/ring_theory/eisenstein_criterion.lean
@@ -109,7 +109,7 @@ begin
     clear_except hmnd hmp hnq,
     omega },
   obtain rfl | rfl : m = 0 ∨ n = 0,
-  { rwa [nat.pos_iff_ne_zero, nat.pos_iff_ne_zero, imp_false, not_not,
+  { rwa [pos_iff_ne_zero, pos_iff_ne_zero, imp_false, not_not,
       ← or_iff_not_imp_left] at hmn },
   { exact or.inl (is_unit_of_nat_degree_eq_zero_of_forall_dvd_is_unit hu hpmqn.1) },
   { exact or.inr (is_unit_of_nat_degree_eq_zero_of_forall_dvd_is_unit
diff --git a/src/ring_theory/int/basic.lean b/src/ring_theory/int/basic.lean
index 7478d2c8969a9..17ed9f5c0b190 100644
--- a/src/ring_theory/int/basic.lean
+++ b/src/ring_theory/int/basic.lean
@@ -209,7 +209,7 @@ theorem irreducible_iff_nat_prime : ∀(a : ℕ), irreducible a ↔ nat.prime a
   end
 
 lemma nat.prime_iff_prime {p : ℕ} : p.prime ↔ _root_.prime (p : ℕ) :=
-⟨λ hp, ⟨nat.pos_iff_ne_zero.1 hp.pos, mt is_unit_iff_dvd_one.1 hp.not_dvd_one,
+⟨λ hp, ⟨pos_iff_ne_zero.1 hp.pos, mt is_unit_iff_dvd_one.1 hp.not_dvd_one,
     λ a b, hp.dvd_mul.1⟩,
   λ hp, ⟨nat.one_lt_iff_ne_zero_and_ne_one.2 ⟨hp.1, λ h1, hp.2.1 $ h1.symm ▸ is_unit_one⟩,
     λ a h, let ⟨b, hab⟩ := h in
@@ -320,7 +320,7 @@ lemma finite_int_iff {a b : ℤ} : finite a b ↔ (a.nat_abs ≠ 1 ∧ b ≠ 0)
 begin
   have := int.nat_abs_eq a,
   have := @int.nat_abs_ne_zero_of_ne_zero b,
-  rw [finite_int_iff_nat_abs_finite, finite_nat_iff, nat.pos_iff_ne_zero],
+  rw [finite_int_iff_nat_abs_finite, finite_nat_iff, pos_iff_ne_zero],
   split; finish
 end
 
diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index ca7ad9817dc25..7fd8de82efa83 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -384,7 +384,7 @@ lemma multiplicity_eq_zero_of_coprime {p a b : ℕ} (hp : p ≠ 1)
   (hab : nat.coprime a b) : multiplicity p a = 0 :=
 begin
   rw [multiplicity_le_multiplicity_iff] at hle,
-  rw [← le_zero_iff_eq, ← not_lt, enat.pos_iff_one_le, ← enat.coe_one,
+  rw [← nonpos_iff_eq_zero, ← not_lt, enat.pos_iff_one_le, ← enat.coe_one,
     ← pow_dvd_iff_le_multiplicity],
   assume h,
   have := nat.dvd_gcd h (hle _ h),
diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean
index bb19389cee9d7..566977c0c0c58 100644
--- a/src/ring_theory/roots_of_unity.lean
+++ b/src/ring_theory/roots_of_unity.lean
@@ -693,7 +693,7 @@ begin
     rintro ⟨a, ⟨d, hd⟩, ha⟩,
     have hazero : 0 < a,
     { contrapose! hd with ha0,
-      simp only [le_zero_iff_eq, zero_mul, *] at *,
+      simp only [nonpos_iff_eq_zero, zero_mul, *] at *,
       exact n.ne_zero },
     rw mem_primitive_roots hazero at ha,
     rw [hd, pow_mul, ha.pow_eq_one, one_pow] },
diff --git a/src/ring_theory/unique_factorization_domain.lean b/src/ring_theory/unique_factorization_domain.lean
index 5b1d6537b8ded..8010ebd8ab7d0 100644
--- a/src/ring_theory/unique_factorization_domain.lean
+++ b/src/ring_theory/unique_factorization_domain.lean
@@ -1073,7 +1073,7 @@ end
 theorem le_of_count_ne_zero {m p : associates α} (h0 : m ≠ 0)
   (hp : irreducible p) : count p m.factors ≠ 0 → p ≤ m :=
 begin
-  rw [← nat.pos_iff_ne_zero],
+  rw [← pos_iff_ne_zero],
   intro h,
   rw [← pow_one p],
   apply (prime_pow_dvd_iff_le h0 hp).2,
diff --git a/src/ring_theory/witt_vector/witt_polynomial.lean b/src/ring_theory/witt_vector/witt_polynomial.lean
index 5d2ba835a6a6d..4d3d03cc81fb7 100644
--- a/src/ring_theory/witt_vector/witt_polynomial.lean
+++ b/src/ring_theory/witt_vector/witt_polynomial.lean
@@ -154,7 +154,7 @@ begin
   have : ∀ i, (monomial (finsupp.single i (p ^ (n - i))) (p ^ i : R)).vars = {i},
   { intro i,
     rw vars_monomial_single,
-    { rw ← nat.pos_iff_ne_zero,
+    { rw ← pos_iff_ne_zero,
       apply pow_pos hp.pos },
     { rw [← nat.cast_pow, nat.cast_ne_zero],
       apply ne_of_gt,
diff --git a/src/set_theory/cardinal.lean b/src/set_theory/cardinal.lean
index 2f1c8456e447f..0bb237bce0fc0 100644
--- a/src/set_theory/cardinal.lean
+++ b/src/set_theory/cardinal.lean
@@ -154,6 +154,18 @@ quotient.induction_on a $ assume α, quotient.sound ⟨equiv.punit_prod α⟩
 private theorem left_distrib (a b c : cardinal.{u}) : a * (b + c) = a * b + a * c :=
 quotient.induction_on₃ a b c $ assume α β γ, quotient.sound ⟨equiv.prod_sum_distrib α β γ⟩
 
+protected theorem eq_zero_or_eq_zero_of_mul_eq_zero  {a b : cardinal.{u}} :
+  a * b = 0 → a = 0 ∨ b = 0 :=
+begin
+  refine quotient.induction_on b _,
+  refine quotient.induction_on a _,
+  intros a b h,
+  contrapose h,
+  simp_rw [not_or_distrib, ← ne.def] at h,
+  have := @prod.nonempty a b (ne_zero_iff_nonempty.mp h.1) (ne_zero_iff_nonempty.mp h.2),
+  exact ne_zero_iff_nonempty.mpr this
+end
+
 instance : comm_semiring cardinal.{u} :=
 { zero          := 0,
   one           := 1,
@@ -231,44 +243,40 @@ from (quotient.induction_on₃ a b c $ assume α β γ,
 section order_properties
 open sum
 
-theorem zero_le : ∀(a : cardinal), 0 ≤ a :=
+protected theorem zero_le : ∀(a : cardinal), 0 ≤ a :=
 by rintro ⟨α⟩; exact ⟨embedding.of_not_nonempty $ λ ⟨a⟩, a.elim⟩
 
-theorem le_zero (a : cardinal) : a ≤ 0 ↔ a = 0 :=
-by simp [le_antisymm_iff, zero_le]
-
-theorem pos_iff_ne_zero {o : cardinal} : 0 < o ↔ o ≠ 0 :=
-by simp [lt_iff_le_and_ne, eq_comm, zero_le]
-
-@[simp] theorem zero_lt_one : (0 : cardinal) < 1 :=
-lt_of_le_of_ne (zero_le _) zero_ne_one
-
-lemma zero_power_le (c : cardinal.{u}) : (0 : cardinal.{u}) ^ c ≤ 1 :=
-by { by_cases h : c = 0, rw [h, power_zero], rw [zero_power h], apply zero_le }
-
-theorem add_le_add : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a + c ≤ b + d :=
+protected theorem add_le_add : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a + c ≤ b + d :=
 by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨e₁.sum_map e₂⟩
 
-theorem add_le_add_left (a) {b c : cardinal} : b ≤ c → a + b ≤ a + c :=
-add_le_add (le_refl _)
+protected theorem add_le_add_left (a) {b c : cardinal} : b ≤ c → a + b ≤ a + c :=
+cardinal.add_le_add (le_refl _)
 
-theorem add_le_add_right {a b : cardinal} (c) (h : a ≤ b) : a + c ≤ b + c :=
-add_le_add h (le_refl _)
 
-theorem le_add_right (a b : cardinal) : a ≤ a + b :=
-by simpa using add_le_add_left a (zero_le b)
+protected theorem le_iff_exists_add {a b : cardinal} : a ≤ b ↔ ∃ c, b = a + c :=
+⟨quotient.induction_on₂ a b $ λ α β ⟨⟨f, hf⟩⟩,
+  have (α ⊕ ((range f)ᶜ : set β)) ≃ β, from
+    (equiv.sum_congr (equiv.set.range f hf) (equiv.refl _)).trans $
+    (equiv.set.sum_compl (range f)),
+  ⟨⟦↥(range f)ᶜ⟧, quotient.sound ⟨this.symm⟩⟩,
+ λ ⟨c, e⟩, add_zero a ▸ e.symm ▸ cardinal.add_le_add_left _ (cardinal.zero_le _)⟩
 
-theorem le_add_left (a b : cardinal) : a ≤ b + a :=
-by simpa using add_le_add_right a (zero_le b)
+instance : order_bot cardinal.{u} :=
+{ bot := 0, bot_le := cardinal.zero_le, ..cardinal.linear_order }
 
-theorem mul_le_mul : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a * c ≤ b * d :=
-by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨e₁.prod_map e₂⟩
+instance : canonically_ordered_comm_semiring cardinal.{u} :=
+{ add_le_add_left       := λ a b h c, cardinal.add_le_add_left _ h,
+  lt_of_add_lt_add_left := λ a b c, lt_imp_lt_of_le_imp_le (cardinal.add_le_add_left _),
+  le_iff_exists_add     := @cardinal.le_iff_exists_add,
+  eq_zero_or_eq_zero_of_mul_eq_zero := @cardinal.eq_zero_or_eq_zero_of_mul_eq_zero,
+  ..cardinal.order_bot,
+  ..cardinal.comm_semiring, ..cardinal.linear_order }
 
-theorem mul_le_mul_left (a) {b c : cardinal} : b ≤ c → a * b ≤ a * c :=
-mul_le_mul (le_refl _)
+@[simp] theorem zero_lt_one : (0 : cardinal) < 1 :=
+lt_of_le_of_ne (zero_le _) zero_ne_one
 
-theorem mul_le_mul_right {a b : cardinal} (c) (h : a ≤ b) : a * c ≤ b * c :=
-mul_le_mul h (le_refl _)
+lemma zero_power_le (c : cardinal.{u}) : (0 : cardinal.{u}) ^ c ≤ 1 :=
+by { by_cases h : c = 0, rw [h, power_zero], rw [zero_power h], apply zero_le }
 
 theorem power_le_power_left : ∀{a b c : cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c :=
 by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩; exact
@@ -285,25 +293,9 @@ end
 theorem power_le_power_right {a b c : cardinal} : a ≤ b → a ^ c ≤ b ^ c :=
 quotient.induction_on₃ a b c $ assume α β γ ⟨e⟩, ⟨embedding.arrow_congr_left e⟩
 
-theorem le_iff_exists_add {a b : cardinal} : a ≤ b ↔ ∃ c, b = a + c :=
-⟨quotient.induction_on₂ a b $ λ α β ⟨⟨f, hf⟩⟩,
-  have (α ⊕ ((range f)ᶜ : set β)) ≃ β, from
-    (equiv.sum_congr (equiv.set.range f hf) (equiv.refl _)).trans $
-    (equiv.set.sum_compl (range f)),
-  ⟨⟦↥(range f)ᶜ⟧, quotient.sound ⟨this.symm⟩⟩,
- λ ⟨c, e⟩, add_zero a ▸ e.symm ▸ add_le_add_left _ (zero_le _)⟩
-
 end order_properties
 
-instance : order_bot cardinal.{u} :=
-{ bot := 0, bot_le := zero_le, ..cardinal.linear_order }
 
-instance : canonically_ordered_add_monoid cardinal.{u} :=
-{ add_le_add_left       := λ a b h c, add_le_add_left _ h,
-  lt_of_add_lt_add_left := λ a b c, lt_imp_lt_of_le_imp_le (add_le_add_left _),
-  le_iff_exists_add     := @le_iff_exists_add,
-  ..cardinal.order_bot,
-  ..cardinal.comm_semiring, ..cardinal.linear_order }
 
 theorem cantor : ∀(a : cardinal.{u}), a < 2 ^ a :=
 by rw ← prop_eq_two; rintros ⟨a⟩; exact ⟨
@@ -423,7 +415,7 @@ theorem sum_le_sup {ι : Type u} (f : ι → cardinal.{u}) : sum f ≤ mk ι * s
 by rw ← sum_const; exact sum_le_sum _ _ (le_sup _)
 
 theorem sup_eq_zero {ι} {f : ι → cardinal} (h : ι → false) : sup f = 0 :=
-by { rw [←le_zero, sup_le], intro x, exfalso, exact h x }
+by { rw [← nonpos_iff_eq_zero, sup_le], intro x, exfalso, exact h x }
 
 /-- The indexed product of cardinals is the cardinality of the Pi type
   (dependent product). -/
@@ -443,7 +435,7 @@ theorem prod_le_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : pro
 theorem prod_ne_zero {ι} (f : ι → cardinal) : prod f ≠ 0 ↔ ∀ i, f i ≠ 0 :=
 begin
   suffices : nonempty (Π i, (f i).out) ↔ ∀ i, nonempty (f i).out,
-    by simpa [← ne_zero_iff_nonempty, prod],
+  { simpa [← ne_zero_iff_nonempty, prod] },
   exact classical.nonempty_pi
 end
 
@@ -722,7 +714,7 @@ match a, b, lt_omega.1 ha, lt_omega.1 hb with
 end
 
 lemma add_lt_omega_iff {a b : cardinal} : a + b < omega ↔ a < omega ∧ b < omega :=
-⟨λ h, ⟨lt_of_le_of_lt (le_add_right _ _) h, lt_of_le_of_lt (le_add_left _ _) h⟩,
+⟨λ h, ⟨lt_of_le_of_lt (self_le_add_right _ _) h, lt_of_le_of_lt (self_le_add_left _ _) h⟩,
   λ⟨h1, h2⟩, add_lt_omega h1 h2⟩
 
 theorem mul_lt_omega {a b : cardinal} (ha : a < omega) (hb : b < omega) : a * b < omega :=
@@ -736,8 +728,10 @@ begin
   { intro h, by_cases ha : a = 0, { left, exact ha },
     right, by_cases hb : b = 0, { left, exact hb },
     right, rw [← ne, ← one_le_iff_ne_zero] at ha hb, split,
-    { rw [← mul_one a], refine lt_of_le_of_lt (mul_le_mul (le_refl a) hb) h },
-    { rw [← _root_.one_mul b], refine lt_of_le_of_lt (mul_le_mul ha (le_refl b)) h }},
+    { rw [← mul_one a],
+      refine lt_of_le_of_lt (canonically_ordered_semiring.mul_le_mul (le_refl a) hb) h },
+    { rw [← _root_.one_mul b],
+      refine lt_of_le_of_lt (canonically_ordered_semiring.mul_le_mul ha (le_refl b)) h }},
   rintro (rfl|rfl|⟨ha,hb⟩); simp only [*, mul_lt_omega, omega_pos, _root_.zero_mul, mul_zero]
 end
 
@@ -954,7 +948,7 @@ quot.sound ⟨equiv.set.union_sum_inter S T⟩
 /-- The cardinality of a union is at most the sum of the cardinalities
 of the two sets. -/
 lemma mk_union_le {α : Type u} (S T : set α) : mk (S ∪ T : set α) ≤ mk S + mk T :=
-@mk_union_add_mk_inter α S T ▸ le_add_right (mk (S ∪ T : set α)) (mk (S ∩ T : set α))
+@mk_union_add_mk_inter α S T ▸ self_le_add_right (mk (S ∪ T : set α)) (mk (S ∩ T : set α))
 
 theorem mk_union_of_disjoint {α : Type u} {S T : set α} (H : disjoint S T) :
   mk (S ∪ T : set α) = mk S + mk T :=
diff --git a/src/set_theory/cardinal_ordinal.lean b/src/set_theory/cardinal_ordinal.lean
index 1f48e5c010604..35f7ec01301b6 100644
--- a/src/set_theory/cardinal_ordinal.lean
+++ b/src/set_theory/cardinal_ordinal.lean
@@ -45,7 +45,7 @@ theorem ord_is_limit {c} (co : omega ≤ c) : (ord c).is_limit :=
 begin
   refine ⟨λ h, omega_ne_zero _, λ a, lt_imp_lt_of_le_imp_le _⟩,
   { rw [← ordinal.le_zero, ord_le] at h,
-    simpa only [card_zero, le_zero] using le_trans co h },
+    simpa only [card_zero, nonpos_iff_eq_zero] using le_trans co h },
   { intro h, rw [ord_le] at h ⊢,
     rwa [← @add_one_of_omega_le (card a), ← card_succ],
     rw [← ord_le, ← le_succ_of_is_limit, ord_le],
@@ -142,7 +142,7 @@ cardinal.aleph_idx.rel_iso.to_equiv.symm_apply_apply c
 cardinal.aleph_idx.rel_iso.to_equiv.apply_symm_apply o
 
 @[simp] theorem aleph'_zero : aleph' 0 = 0 :=
-by rw [← le_zero, ← aleph'_aleph_idx 0, aleph'_le];
+by rw [← nonpos_iff_eq_zero, ← aleph'_aleph_idx 0, aleph'_le];
    apply ordinal.zero_le
 
 @[simp] theorem aleph'_succ {o : ordinal.{u}} : aleph' o.succ = (aleph' o).succ :=
@@ -222,7 +222,8 @@ aleph'_is_normal.trans $ add_is_normal ordinal.omega
 theorem mul_eq_self {c : cardinal} (h : omega ≤ c) : c * c = c :=
 begin
   refine le_antisymm _
-    (by simpa only [mul_one] using mul_le_mul_left c (le_trans (le_of_lt one_lt_omega) h)),
+    (by simpa only [mul_one] using
+      canonically_ordered_semiring.mul_le_mul_left' (one_lt_omega.le.trans h) c),
   -- the only nontrivial part is `c * c ≤ c`. We prove it inductively.
   refine acc.rec_on (cardinal.wf.apply c) (λ c _,
     quotient.induction_on c $ λ α IH ol, _) h,
@@ -272,21 +273,24 @@ of the cardinalities of `α` and `β`. -/
 theorem mul_eq_max {a b : cardinal} (ha : omega ≤ a) (hb : omega ≤ b) : a * b = max a b :=
 le_antisymm
   (mul_eq_self (le_trans ha (le_max_left a b)) ▸
-    mul_le_mul (le_max_left _ _) (le_max_right _ _)) $
+    canonically_ordered_semiring.mul_le_mul (le_max_left _ _) (le_max_right _ _)) $
 max_le
-  (by simpa only [mul_one] using mul_le_mul_left a (le_trans (le_of_lt one_lt_omega) hb))
-  (by simpa only [one_mul] using mul_le_mul_right b (le_trans (le_of_lt one_lt_omega) ha))
+  (by simpa only [mul_one] using
+    canonically_ordered_semiring.mul_le_mul_left' (one_lt_omega.le.trans hb) a)
+  (by simpa only [one_mul] using
+    canonically_ordered_semiring.mul_le_mul_right' (one_lt_omega.le.trans ha) b)
 
 theorem mul_lt_of_lt {a b c : cardinal} (hc : omega ≤ c)
   (h1 : a < c) (h2 : b < c) : a * b < c :=
-lt_of_le_of_lt (mul_le_mul (le_max_left a b) (le_max_right a b)) $
+lt_of_le_of_lt (canonically_ordered_semiring.mul_le_mul (le_max_left a b) (le_max_right a b)) $
 (lt_or_le (max a b) omega).elim
   (λ h, lt_of_lt_of_le (mul_lt_omega h h) hc)
   (λ h, by rw mul_eq_self h; exact max_lt h1 h2)
 
 lemma mul_le_max_of_omega_le_left {a b : cardinal} (h : omega ≤ a) : a * b ≤ max a b :=
 begin
-  convert mul_le_mul (le_max_left a b) (le_max_right a b), rw [mul_eq_self],
+  convert canonically_ordered_semiring.mul_le_mul (le_max_left a b) (le_max_right a b),
+  rw [mul_eq_self],
   refine le_trans h (le_max_left a b)
 end
 
@@ -295,7 +299,8 @@ begin
   apply le_antisymm, apply mul_le_max_of_omega_le_left h,
   cases le_or_gt omega b with hb hb, rw [mul_eq_max h hb],
   have : b ≤ a, exact le_trans (le_of_lt hb) h,
-  rw [max_eq_left this], convert mul_le_mul_left _ (one_le_iff_ne_zero.mpr h'), rw [mul_one],
+  rw [max_eq_left this],
+  convert canonically_ordered_semiring.mul_le_mul_left' (one_le_iff_ne_zero.mpr h') _, rw [mul_one],
 end
 
 lemma mul_eq_left {a b : cardinal} (ha : omega ≤ a) (hb : b ≤ a) (hb' : b ≠ 0) : a * b = a :=
@@ -305,7 +310,8 @@ lemma mul_eq_right {a b : cardinal} (hb : omega ≤ b) (ha : a ≤ b) (ha' : a 
 by { rw [mul_comm, mul_eq_left hb ha ha'] }
 
 lemma le_mul_left {a b : cardinal} (h : b ≠ 0) : a ≤ b * a :=
-by { convert mul_le_mul_right _ (one_le_iff_ne_zero.mpr h), rw [one_mul] }
+by { convert canonically_ordered_semiring.mul_le_mul_right' (one_le_iff_ne_zero.mpr h) _,
+  rw [one_mul] }
 
 lemma le_mul_right {a b : cardinal} (h : b ≠ 0) : a ≤ a * b :=
 by { rw [mul_comm], exact le_mul_left h }
@@ -338,8 +344,8 @@ end
 theorem add_eq_self {c : cardinal} (h : omega ≤ c) : c + c = c :=
 le_antisymm
   (by simpa only [nat.cast_bit0, nat.cast_one, mul_eq_self h, two_mul] using
-     mul_le_mul_right c (le_trans (le_of_lt $ nat_lt_omega 2) h))
-  (le_add_left c c)
+     canonically_ordered_semiring.mul_le_mul_right' ((nat_lt_omega 2).le.trans h) c)
+  (self_le_add_left c c)
 
 /-- If `α` is an infinite type, then the cardinality of `α ⊕ β` is the maximum
 of the cardinalities of `α` and `β`. -/
@@ -347,7 +353,7 @@ theorem add_eq_max {a b : cardinal} (ha : omega ≤ a) : a + b = max a b :=
 le_antisymm
   (add_eq_self (le_trans ha (le_max_left a b)) ▸
     add_le_add (le_max_left _ _) (le_max_right _ _)) $
-max_le (le_add_right _ _) (le_add_left _ _)
+max_le (self_le_add_right _ _) (self_le_add_left _ _)
 
 theorem add_lt_of_lt {a b c : cardinal} (hc : omega ≤ c)
   (h1 : a < c) (h2 : b < c) : a + b < c :=
@@ -360,7 +366,7 @@ lemma eq_of_add_eq_of_omega_le {a b c : cardinal} (h : a + b = c) (ha : a < c) (
   b = c :=
 begin
   apply le_antisymm,
-  { rw [← h], apply cardinal.le_add_left },
+  { rw [← h], apply self_le_add_left },
   rw[← not_lt], intro hb,
   have : a + b < c := add_lt_of_lt hc ha hb,
   simpa [h, lt_irrefl] using this
@@ -377,7 +383,7 @@ begin
   rw [max_le_iff], split,
   { intro h, cases (le_or_lt omega a) with ha ha,
     { left, use ha, rw [← not_lt], intro hb, apply ne_of_gt _ h,
-      exact lt_of_lt_of_le hb (le_add_left b a) },
+      exact lt_of_lt_of_le hb (self_le_add_left b a) },
     right, rw [← h, add_lt_omega_iff, lt_omega, lt_omega] at ha,
     rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩, norm_cast at h ⊢,
     rw [← add_right_inj, h, add_zero] },
@@ -400,7 +406,7 @@ begin
     rw [eq_of_add_eq_of_omega_le h this hb] },
   { have hc : c < omega,
     { rw [← not_le], intro hc,
-      apply lt_irrefl omega, apply lt_of_le_of_lt (le_trans hc (le_add_left _ a)),
+      apply lt_irrefl omega, apply lt_of_le_of_lt (le_trans hc (self_le_add_left _ a)),
       rw [← h], apply add_lt_omega ha hb },
     rw [lt_omega] at *,
     rcases ha with ⟨n, rfl⟩, rcases hb with ⟨m, rfl⟩, rcases hc with ⟨k, rfl⟩,
@@ -419,8 +425,8 @@ H3.symm ▸ (quotient.induction_on κ (λ α H1, nat.rec_on n
   (le_of_lt $ lt_of_lt_of_le (by rw [nat.cast_zero, power_zero];
     from one_lt_omega) H1)
   (λ n ih, trans_rel_left _
-    (by rw [nat.cast_succ, power_add, power_one];
-      from mul_le_mul_right _ ih)
+    (by { rw [nat.cast_succ, power_add, power_one];
+      exact canonically_ordered_semiring.mul_le_mul_right' ih _ })
     (mul_eq_self H1))) H1)
 
 lemma power_self_eq {c : cardinal} (h : omega ≤ c) : c ^ c = 2 ^ c :=
@@ -493,7 +499,7 @@ begin
   { refine ⟨embedding.subtype_map _ _⟩, apply embedding.image,
     use sum.inr, apply sum.inr.inj, intros s hs, exact le_trans mk_image_le hs },
   refine le_trans
-    (mk_bounded_set_le_of_omega_le (ulift.{u} nat ⊕ α) c (le_add_right omega (mk α))) _,
+    (mk_bounded_set_le_of_omega_le (ulift.{u} nat ⊕ α) c (self_le_add_right omega (mk α))) _,
   rw [max_comm, ←add_eq_max]; refl
 end
 
@@ -610,14 +616,14 @@ by simp [bit1]
 by { rw ←not_iff_not, simp [bit0], }
 
 @[simp] lemma zero_lt_bit1 (a : cardinal) : 0 < bit1 a :=
-lt_of_lt_of_le zero_lt_one (le_add_left _ _)
+lt_of_lt_of_le zero_lt_one (self_le_add_left _ _)
 
 @[simp] lemma one_le_bit0 (a : cardinal) : 1 ≤ bit0 a ↔ 0 < a :=
 ⟨λ h, (zero_lt_bit0 a).mp (lt_of_lt_of_le zero_lt_one h),
- λ h, le_trans (one_le_iff_pos.mpr h) (le_add_left a a)⟩
+ λ h, le_trans (one_le_iff_pos.mpr h) (self_le_add_left a a)⟩
 
 @[simp] lemma one_le_bit1 (a : cardinal) : 1 ≤ bit1 a :=
-le_add_left _ _
+self_le_add_left _ _
 
 theorem bit0_eq_self {c : cardinal} (h : omega ≤ c) : bit0 c = c :=
 add_eq_self h
@@ -698,10 +704,10 @@ end
 begin
   split,
   { assume h,
-    apply bit0_le_bit1.1 (le_trans ((bit0 a).le_add_right 1) h) },
+    apply bit0_le_bit1.1 (le_trans (self_le_add_right (bit0 a) 1) h) },
   { assume h,
-    calc a + a + 1 ≤ a + b + 1 : add_le_add_right 1 (add_le_add_left a h)
-           ... ≤ b + b + 1 : add_le_add_right 1 (add_le_add_right b h) }
+    calc a + a + 1 ≤ a + b + 1 : add_le_add_right (add_le_add_left h a) 1
+           ... ≤ b + b + 1 : add_le_add_right (add_le_add_right h b) 1 }
 end
 
 @[simp] lemma bit1_le_bit0 {a b : cardinal} : bit1 a ≤ bit0 b ↔ (a < b ∨ (a ≤ b ∧ omega ≤ a)) :=
diff --git a/src/set_theory/cofinality.lean b/src/set_theory/cofinality.lean
index 53998cf0caeb8..6e3cc4761f1d6 100644
--- a/src/set_theory/cofinality.lean
+++ b/src/set_theory/cofinality.lean
@@ -445,7 +445,8 @@ theorem succ_is_regular {c : cardinal.{u}} (h : omega ≤ c) : is_regular (succ
   rw [← αe, re] at this ⊢,
   rcases cof_eq' r this with ⟨S, H, Se⟩,
   rw [← Se],
-  apply lt_imp_lt_of_le_imp_le (mul_le_mul_right c),
+  apply lt_imp_lt_of_le_imp_le
+    (λ (h : mk S ≤ c), canonically_ordered_semiring.mul_le_mul_right' h c),
   rw [mul_eq_self h, ← succ_le, ← αe, ← sum_const],
   refine le_trans _ (sum_le_sum (λ x:S, card (typein r x)) _ _),
   { simp [typein, sum_mk (λ x:S, {a//r a x})],
diff --git a/src/set_theory/game/state.lean b/src/set_theory/game/state.lean
index 21978ae26b3a2..784d1ee2cc473 100644
--- a/src/set_theory/game/state.lean
+++ b/src/set_theory/game/state.lean
@@ -72,8 +72,8 @@ turns remaining.
 -/
 def of_aux : Π (n : ℕ) (s : S) (h : turn_bound s ≤ n), pgame
 | 0 s h     := pgame.mk {t // t ∈ L s} {t // t ∈ R s}
-    (λ t, begin exfalso, exact turn_bound_ne_zero_of_left_move t.2 (le_zero_iff_eq.mp h) end)
-    (λ t, begin exfalso, exact turn_bound_ne_zero_of_right_move t.2 (le_zero_iff_eq.mp h) end)
+    (λ t, begin exfalso, exact turn_bound_ne_zero_of_left_move t.2 (nonpos_iff_eq_zero.mp h) end)
+    (λ t, begin exfalso, exact turn_bound_ne_zero_of_right_move t.2 (nonpos_iff_eq_zero.mp h) end)
 | (n+1) s h :=
   pgame.mk {t // t ∈ L s} {t // t ∈ R s}
     (λ t, of_aux n t (turn_bound_of_left t.2 n h))
@@ -87,27 +87,27 @@ def of_aux_relabelling : Π (s : S) (n m : ℕ) (hn : turn_bound s ≤ n) (hm :
     dsimp [pgame.of_aux],
     fsplit, refl, refl,
     { intro i, dsimp at i, exfalso,
-      exact turn_bound_ne_zero_of_left_move i.2 (le_zero_iff_eq.mp hn) },
+      exact turn_bound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn) },
     { intro j, dsimp at j, exfalso,
-      exact turn_bound_ne_zero_of_right_move j.2 (le_zero_iff_eq.mp hm) }
+      exact turn_bound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hm) }
   end
 | s 0 (m+1) hn hm :=
   begin
     dsimp [pgame.of_aux],
     fsplit, refl, refl,
     { intro i, dsimp at i, exfalso,
-      exact turn_bound_ne_zero_of_left_move i.2 (le_zero_iff_eq.mp hn) },
+      exact turn_bound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn) },
     { intro j, dsimp at j, exfalso,
-      exact turn_bound_ne_zero_of_right_move j.2 (le_zero_iff_eq.mp hn) }
+      exact turn_bound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hn) }
   end
 | s (n+1) 0 hn hm :=
   begin
     dsimp [pgame.of_aux],
     fsplit, refl, refl,
     { intro i, dsimp at i, exfalso,
-      exact turn_bound_ne_zero_of_left_move i.2 (le_zero_iff_eq.mp hm) },
+      exact turn_bound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hm) },
     { intro j, dsimp at j, exfalso,
-      exact turn_bound_ne_zero_of_right_move j.2 (le_zero_iff_eq.mp hm) }
+      exact turn_bound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hm) }
   end
 | s (n+1) (m+1) hn hm :=
   begin
@@ -157,7 +157,7 @@ def relabelling_move_left_aux (n : ℕ) {s : S} (h : turn_bound s ≤ n)
 begin
   induction n,
   { have t' := (left_moves_of_aux 0 h) t,
-    exfalso, exact turn_bound_ne_zero_of_left_move t'.2 (le_zero_iff_eq.mp h), },
+    exfalso, exact turn_bound_ne_zero_of_left_move t'.2 (nonpos_iff_eq_zero.mp h), },
   { refl },
 end
 /--
@@ -187,7 +187,7 @@ def relabelling_move_right_aux (n : ℕ) {s : S} (h : turn_bound s ≤ n)
 begin
   induction n,
   { have t' := (right_moves_of_aux 0 h) t,
-    exfalso, exact turn_bound_ne_zero_of_right_move t'.2 (le_zero_iff_eq.mp h), },
+    exfalso, exact turn_bound_ne_zero_of_right_move t'.2 (nonpos_iff_eq_zero.mp h), },
   { refl },
 end
 /--
@@ -223,12 +223,12 @@ instance short_of_aux : Π (n : ℕ) {s : S} (h : turn_bound s ≤ n), short (of
   (λ i, begin
     have i := (left_moves_of_aux _ _).to_fun i,
     exfalso,
-    exact turn_bound_ne_zero_of_left_move i.2 (le_zero_iff_eq.mp h),
+    exact turn_bound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp h),
   end)
   (λ j, begin
     have j := (right_moves_of_aux _ _).to_fun j,
     exfalso,
-    exact turn_bound_ne_zero_of_right_move j.2 (le_zero_iff_eq.mp h),
+    exact turn_bound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp h),
   end)
 | (n+1) s h :=
   short.mk'
diff --git a/src/set_theory/ordinal.lean b/src/set_theory/ordinal.lean
index ec257975ec9c8..03b681761860a 100644
--- a/src/set_theory/ordinal.lean
+++ b/src/set_theory/ordinal.lean
@@ -734,16 +734,16 @@ quotient.sound ⟨⟨empty_equiv_pempty.symm, λ _ _, iff.rfl⟩⟩
 
 @[simp] theorem card_zero : card 0 = 0 := rfl
 
-theorem zero_le (o : ordinal) : 0 ≤ o :=
+protected theorem zero_le (o : ordinal) : 0 ≤ o :=
 induction_on o $ λ α r _,
 ⟨⟨⟨embedding.of_not_nonempty $ λ ⟨a⟩, a.elim,
   λ a, a.elim⟩, λ a, a.elim⟩⟩
 
-@[simp] theorem le_zero {o : ordinal} : o ≤ 0 ↔ o = 0 :=
-by simp only [le_antisymm_iff, zero_le, and_true]
+@[simp] protected theorem le_zero {o : ordinal} : o ≤ 0 ↔ o = 0 :=
+by simp only [le_antisymm_iff, ordinal.zero_le, and_true]
 
-theorem pos_iff_ne_zero {o : ordinal} : 0 < o ↔ o ≠ 0 :=
-by simp only [lt_iff_le_and_ne, zero_le, true_and, ne.def, eq_comm]
+protected theorem pos_iff_ne_zero {o : ordinal} : 0 < o ↔ o ≠ 0 :=
+by simp only [lt_iff_le_and_ne, ordinal.zero_le, true_and, ne.def, eq_comm]
 
 instance : has_one ordinal :=
 ⟨⟦⟨punit, empty_relation, by apply_instance⟩⟧⟩
@@ -953,7 +953,7 @@ induction_on c $ λ β s _,
   end⟩⟩
 
 theorem le_add_right (a b : ordinal) : a ≤ a + b :=
-by simpa only [add_zero] using add_le_add_left (zero_le b) a
+by simpa only [add_zero] using add_le_add_left (ordinal.zero_le b) a
 
 theorem add_le_add_right {a b : ordinal} : a ≤ b → ∀ c, a + c ≤ b + c :=
 induction_on a $ λ α₁ r₁ hr₁, induction_on b $ λ α₂ r₂ hr₂ ⟨⟨⟨f, fo⟩, fi⟩⟩ c,
@@ -967,7 +967,7 @@ induction_on c $ λ β s hs, (@type_le' _ _ _ _
 end⟩⟩
 
 theorem le_add_left (a b : ordinal) : a ≤ b + a :=
-by simpa only [zero_add] using add_le_add_right (zero_le b) a
+by simpa only [zero_add] using add_le_add_right (ordinal.zero_le b) a
 
 theorem lt_succ_self (o : ordinal.{u}) : o < succ o :=
 induction_on o $ λ α r _, ⟨⟨⟨⟨λ x, sum.inl x, λ _ _, sum.inl.inj⟩,
diff --git a/src/set_theory/ordinal_arithmetic.lean b/src/set_theory/ordinal_arithmetic.lean
index 0ca44c40fa746..8d9e6d59ba629 100644
--- a/src/set_theory/ordinal_arithmetic.lean
+++ b/src/set_theory/ordinal_arithmetic.lean
@@ -104,10 +104,10 @@ theorem one_le_iff_pos {o : ordinal} : 1 ≤ o ↔ 0 < o :=
 by rw [← succ_zero, succ_le]
 
 theorem one_le_iff_ne_zero {o : ordinal} : 1 ≤ o ↔ o ≠ 0 :=
-by rw [one_le_iff_pos, pos_iff_ne_zero]
+by rw [one_le_iff_pos, ordinal.pos_iff_ne_zero]
 
 theorem succ_pos (o : ordinal) : 0 < succ o :=
-lt_of_le_of_lt (zero_le _) (lt_succ_self _)
+lt_of_le_of_lt (ordinal.zero_le _) (lt_succ_self _)
 
 theorem succ_ne_zero (o : ordinal) : succ o ≠ 0 :=
 ne_of_gt $ succ_pos o
@@ -150,7 +150,7 @@ by simp only [le_antisymm_iff, add_le_add_iff_right]
 @[simp] theorem card_eq_zero {o} : card o = 0 ↔ o = 0 :=
 ⟨induction_on o $ λ α r _ h, begin
   refine le_antisymm (le_of_not_lt $
-    λ hn, ne_zero_iff_nonempty.2 _ h) (zero_le _),
+    λ hn, ne_zero_iff_nonempty.2 _ h) (ordinal.zero_le _),
   rw [← succ_le, succ_zero] at hn, cases hn with f,
   exact ⟨f punit.star⟩
 end, λ e, by simp only [e, card_zero]⟩
@@ -168,7 +168,7 @@ 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 _, ne.symm $ ordinal.one_ne_zero⟩
+lt_iff_le_and_ne.2 ⟨ordinal.zero_le _, ne.symm $ ordinal.one_ne_zero⟩
 
 /-! ### The predecessor of an ordinal -/
 
@@ -258,7 +258,7 @@ and_congr (not_congr $ by simpa only [lift_zero] using @lift_inj o 0)
       rw [← e, lift_lt] at h; exact H a' h⟩
 
 theorem is_limit.pos {o : ordinal} (h : is_limit o) : 0 < o :=
-lt_of_le_of_ne (zero_le _) h.1.symm
+lt_of_le_of_ne (ordinal.zero_le _) h.1.symm
 
 theorem is_limit.one_lt {o : ordinal} (h : is_limit o) : 1 < o :=
 by simpa only [succ_zero] using h.2 _ h.pos
@@ -341,7 +341,7 @@ not_iff_not.1 $ by simpa only [exists_prop, not_exists, not_and, not_lt] using H
 
 theorem is_normal.lt_iff {f} (H : is_normal f) {a b} : f a < f b ↔ a < b :=
 strict_mono.lt_iff_lt $ λ a b,
-limit_rec_on b (not.elim (not_lt_of_le $ zero_le _))
+limit_rec_on b (not.elim (not_lt_of_le $ ordinal.zero_le _))
   (λ b IH h, (lt_or_eq_of_le (lt_succ.1 h)).elim
     (λ h, lt_trans (IH h) (H.1 _))
     (λ e, e ▸ H.1 _))
@@ -355,7 +355,7 @@ theorem is_normal.inj {f} (H : is_normal f) {a b} : f a = f b ↔ a = b :=
 by simp only [le_antisymm_iff, H.le_iff]
 
 theorem is_normal.le_self {f} (H : is_normal f) (a) : a ≤ f a :=
-limit_rec_on a (zero_le _)
+limit_rec_on a (ordinal.zero_le _)
   (λ a IH, succ_le.2 $ lt_of_le_of_lt IH (H.1 _))
   (λ a l IH, (limit_le l).2 $ λ b h,
     le_trans (IH b h) $ H.le_iff.2 $ le_of_lt h)
@@ -369,7 +369,7 @@ theorem is_normal.le_set {f} (H : is_normal f) (p : ordinal → Prop)
   revert H₂, apply limit_rec_on S,
   { intro H₂,
      cases p0 with x px,
-     have := le_zero.1 ((H₂ _).1 (zero_le _) _ px),
+     have := ordinal.le_zero.1 ((H₂ _).1 (ordinal.zero_le _) _ px),
      rw this at px, exact h _ px },
   { intros S _ H₂,
     rcases not_ball.1 (mt (H₂ S).2 $ not_le_of_lt $ lt_succ_self _) with ⟨a, h₁, h₂⟩,
@@ -399,7 +399,7 @@ theorem is_normal.trans {f g} (H₁ : is_normal f) (H₂ : is_normal g) :
 
 theorem is_normal.is_limit {f} (H : is_normal f) {o} (l : is_limit o) :
   is_limit (f o) :=
-⟨ne_of_gt $ lt_of_le_of_lt (zero_le _) $ H.lt_iff.2 l.pos,
+⟨ne_of_gt $ lt_of_le_of_lt (ordinal.zero_le _) $ H.lt_iff.2 l.pos,
 λ a h, let ⟨b, h₁, h₂⟩ := (H.limit_lt l).1 h in
   lt_of_le_of_lt (succ_le.2 h₂) (H.lt_iff.2 h₁)⟩
 
@@ -474,14 +474,14 @@ end (le_add_sub _ _)
 by simpa only [zero_add] using add_sub_cancel 0 a
 
 @[simp] theorem zero_sub (a : ordinal) : 0 - a = 0 :=
-by rw ← le_zero; apply sub_le_self
+by rw ← ordinal.le_zero; apply sub_le_self
 
 @[simp] theorem sub_self (a : ordinal) : a - a = 0 :=
 by simpa only [add_zero] using add_sub_cancel a 0
 
 theorem sub_eq_zero_iff_le {a b : ordinal} : a - b = 0 ↔ a ≤ b :=
 ⟨λ h, by simpa only [h, add_zero] using le_add_sub a b,
- λ h, by rwa [← le_zero, sub_le, add_zero]⟩
+ λ h, by rwa [← ordinal.le_zero, sub_le, add_zero]⟩
 
 theorem sub_sub (a b c : ordinal) : a - b - c = a - (b + c) :=
 eq_of_forall_ge_iff $ λ d, by rw [sub_le, sub_le, sub_le, add_assoc]
@@ -661,7 +661,7 @@ theorem mul_pos {a b : ordinal} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b :=
 by simpa only [mul_zero] using mul_lt_mul_of_pos_left h₂ h₁
 
 theorem mul_ne_zero {a b : ordinal} : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=
-by simpa only [pos_iff_ne_zero] using mul_pos
+by simpa only [ordinal.pos_iff_ne_zero] using mul_pos
 
 theorem le_of_mul_le_mul_left {a b c : ordinal}
   (h : c * a ≤ c * b) (h0 : 0 < c) : a ≤ b :=
@@ -688,7 +688,7 @@ end
 protected lemma div_aux (a b : ordinal.{u}) (h : b ≠ 0) : set.nonempty {o | a < b * succ o} :=
 ⟨a, succ_le.1 $
   by simpa only [succ_zero, one_mul]
-    using mul_le_mul_right (succ a) (succ_le.2 (pos_iff_ne_zero.2 h))⟩
+    using mul_le_mul_right (succ a) (succ_le.2 (ordinal.pos_iff_ne_zero.2 h))⟩
 
 /-- `a / b` is the unique ordinal `o` satisfying
   `a = b * o + o'` with `o' < b`. -/
@@ -719,7 +719,7 @@ theorem le_div {a b c : ordinal} (c0 : c ≠ 0) :
   a ≤ b / c ↔ c * a ≤ b :=
 begin
   apply limit_rec_on a,
-  { simp only [mul_zero, zero_le] },
+  { simp only [mul_zero, ordinal.zero_le] },
   { intros, rw [succ_le, lt_div c0] },
   { simp only [mul_le_of_limit, limit_le, iff_self, forall_true_iff] {contextual := tt} }
 end
@@ -729,18 +729,18 @@ theorem div_lt {a b c : ordinal} (b0 : b ≠ 0) :
 lt_iff_lt_of_le_iff_le $ le_div b0
 
 theorem div_le_of_le_mul {a b c : ordinal} (h : a ≤ b * c) : a / b ≤ c :=
-if b0 : b = 0 then by simp only [b0, div_zero, zero_le] else
+if b0 : b = 0 then by simp only [b0, div_zero, ordinal.zero_le] else
 (div_le b0).2 $ lt_of_le_of_lt h $
-mul_lt_mul_of_pos_left (lt_succ_self _) (pos_iff_ne_zero.2 b0)
+mul_lt_mul_of_pos_left (lt_succ_self _) (ordinal.pos_iff_ne_zero.2 b0)
 
 theorem mul_lt_of_lt_div {a b c : ordinal} : a < b / c → c * a < b :=
 lt_imp_lt_of_le_imp_le div_le_of_le_mul
 
 @[simp] theorem zero_div (a : ordinal) : 0 / a = 0 :=
-le_zero.1 $ div_le_of_le_mul $ zero_le _
+ordinal.le_zero.1 $ div_le_of_le_mul $ ordinal.zero_le _
 
 theorem mul_div_le (a b : ordinal) : b * (a / b) ≤ a :=
-if b0 : b = 0 then by simp only [b0, zero_mul, zero_le] else (le_div b0).1 (le_refl _)
+if b0 : b = 0 then by simp only [b0, zero_mul, ordinal.zero_le] else (le_div b0).1 (le_refl _)
 
 theorem mul_add_div (a) {b : ordinal} (b0 : b ≠ 0) (c) : (b * a + c) / b = a + c / b :=
 begin
@@ -753,7 +753,7 @@ begin
 end
 
 theorem div_eq_zero_of_lt {a b : ordinal} (h : a < b) : a / b = 0 :=
-by rw [← le_zero, div_le $ pos_iff_ne_zero.1 $ lt_of_le_of_lt (zero_le _) h];
+by rw [← ordinal.le_zero, div_le $ ordinal.pos_iff_ne_zero.1 $ lt_of_le_of_lt (ordinal.zero_le _) h];
    simpa only [succ_zero, mul_one] using h
 
 @[simp] theorem mul_div_cancel (a) {b : ordinal} (b0 : b ≠ 0) : b * a / b = a :=
@@ -777,7 +777,7 @@ begin
     { rw [h', add_zero] at h, right, exact ⟨h', h⟩ },
       left, rw [←add_sub_cancel a b], apply sub_is_limit h,
       suffices : a + 0 < a + b, simpa only [add_zero],
-      rwa [add_lt_add_iff_left, pos_iff_ne_zero] },
+      rwa [add_lt_add_iff_left, ordinal.pos_iff_ne_zero] },
   rcases h with h|⟨rfl, h⟩, exact add_is_limit a h, simpa only [add_zero]
 end
 
@@ -982,13 +982,13 @@ begin
   { exact h0 },
   { intros b IH, rw [power_succ],
     exact mul_pos IH a0 },
-  { exact λ b l _, (lt_power_of_limit (pos_iff_ne_zero.1 a0) l).2
+  { exact λ b l _, (lt_power_of_limit (ordinal.pos_iff_ne_zero.1 a0) l).2
       ⟨0, l.pos, h0⟩ },
 end
 
 theorem power_ne_zero {a : ordinal} (b)
   (a0 : a ≠ 0) : a ^ b ≠ 0 :=
-pos_iff_ne_zero.1 $ power_pos b $ pos_iff_ne_zero.2 a0
+ordinal.pos_iff_ne_zero.1 $ power_pos b $ ordinal.pos_iff_ne_zero.2 a0
 
 theorem power_is_normal {a : ordinal} (h : 1 < a) : is_normal ((^) a) :=
 have a0 : 0 < a, from lt_trans zero_lt_one h,
@@ -1036,13 +1036,13 @@ begin
   by_cases a0 : a = 0,
   { subst a, by_cases c0 : c = 0,
     { subst c, simp only [power_zero] },
-    { simp only [zero_power c0, zero_le] } },
+    { simp only [zero_power c0, ordinal.zero_le] } },
   { apply limit_rec_on c,
     { simp only [power_zero] },
     { intros c IH, simpa only [power_succ] using mul_le_mul IH ab },
     { exact λ c l IH, (power_le_of_limit a0 l).2
         (λ b' h, le_trans (IH _ h) (power_le_power_right
-          (lt_of_lt_of_le (pos_iff_ne_zero.2 a0) ab) (le_of_lt h))) } }
+          (lt_of_lt_of_le (ordinal.pos_iff_ne_zero.2 a0) ab) (le_of_lt h))) } }
 end
 
 theorem le_power_self {a : ordinal} (b) (a1 : 1 < a) : b ≤ a ^ b :=
@@ -1053,7 +1053,7 @@ theorem power_lt_power_left_of_succ {a b c : ordinal}
 by rw [power_succ, power_succ]; exact
 lt_of_le_of_lt
   (mul_le_mul_right _ $ power_le_power_left _ $ le_of_lt ab)
-  (mul_lt_mul_of_pos_left ab (power_pos _ (lt_of_le_of_lt (zero_le _) ab)))
+  (mul_lt_mul_of_pos_left ab (power_pos _ (lt_of_le_of_lt (ordinal.zero_le _) ab)))
 
 theorem power_add (a b c : ordinal) : a ^ (b + c) = a ^ b * a ^ c :=
 begin
@@ -1061,7 +1061,7 @@ begin
   { subst a,
     by_cases c0 : c = 0, {simp only [c0, add_zero, power_zero, mul_one]},
     have : b+c ≠ 0 := ne_of_gt (lt_of_lt_of_le
-      (pos_iff_ne_zero.2 c0) (le_add_left _ _)),
+      (ordinal.pos_iff_ne_zero.2 c0) (le_add_left _ _)),
     simp only [zero_power c0, zero_power this, mul_zero] },
   cases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with a1 a1,
   { subst a1, simp only [one_power, mul_one] },
@@ -1073,7 +1073,7 @@ begin
     refine eq_of_forall_ge_iff (λ d, (((power_is_normal a1).trans
       (add_is_normal b)).limit_le l).trans _),
     simp only [IH] {contextual := tt},
-    exact (((mul_is_normal $ power_pos b (pos_iff_ne_zero.2 a0)).trans
+    exact (((mul_is_normal $ power_pos b (ordinal.pos_iff_ne_zero.2 a0)).trans
       (power_is_normal a1)).limit_le l).symm }
 end
 
@@ -1103,7 +1103,7 @@ begin
     rw [mul_succ, power_add, IH, power_succ] },
   { intros c l IH,
     refine eq_of_forall_ge_iff (λ d, (((power_is_normal a1).trans
-      (mul_is_normal (pos_iff_ne_zero.2 b0))).limit_le l).trans _),
+      (mul_is_normal (ordinal.pos_iff_ne_zero.2 b0))).limit_le l).trans _),
     simp only [IH] {contextual := tt},
     exact (power_le_of_limit (power_ne_zero _ a0) l).symm }
 end
@@ -1126,7 +1126,7 @@ by simp only [log, dif_pos b1]
 
 @[simp] theorem log_zero (b : ordinal) : log b 0 = 0 :=
 if b1 : 1 < b then
-  by rw [log_def b1, ← le_zero, pred_le];
+  by rw [log_def b1, ← ordinal.le_zero, pred_le];
      apply omin_le; change 0<b^succ 0;
      rw [succ_zero, power_one];
      exact lt_trans zero_lt_one b1
@@ -1149,7 +1149,7 @@ end
 theorem lt_power_succ_log {b : ordinal} (b1 : 1 < b) (x : ordinal) :
   x < b ^ succ (log b x) :=
 begin
-  cases lt_or_eq_of_le (zero_le x) with x0 x0,
+  cases lt_or_eq_of_le (ordinal.zero_le x) with x0 x0,
   { rw [succ_log_def b1 x0], exact omin_mem {o | x < b^o} _ },
   { subst x, apply power_pos _ (lt_trans zero_lt_one b1) }
 end
@@ -1180,17 +1180,17 @@ lt_iff_lt_of_le_iff_le (le_log b1 x0)
 
 theorem log_le_log (b) {x y : ordinal} (xy : x ≤ y) :
   log b x ≤ log b y :=
-if x0 : x = 0 then by simp only [x0, log_zero, zero_le] else
-have x0 : 0 < x, from pos_iff_ne_zero.2 x0,
+if x0 : x = 0 then by simp only [x0, log_zero, ordinal.zero_le] else
+have x0 : 0 < x, from ordinal.pos_iff_ne_zero.2 x0,
 if b1 : 1 < b then
   (le_log b1 (lt_of_lt_of_le x0 xy)).2 $ le_trans (power_log_le _ x0) xy
-else by simp only [log_not_one_lt b1, zero_le]
+else by simp only [log_not_one_lt b1, ordinal.zero_le]
 
 theorem log_le_self (b x : ordinal) : log b x ≤ x :=
-if x0 : x = 0 then by simp only [x0, log_zero, zero_le] else
+if x0 : x = 0 then by simp only [x0, log_zero, ordinal.zero_le] else
 if b1 : 1 < b then
-  le_trans (le_power_self _ b1) (power_log_le b (pos_iff_ne_zero.2 x0))
-else by simp only [log_not_one_lt b1, zero_le]
+  le_trans (le_power_self _ b1) (power_log_le b (ordinal.pos_iff_ne_zero.2 x0))
+else by simp only [log_not_one_lt b1, ordinal.zero_le]
 
 /-! ### The Cantor normal form -/
 
@@ -1198,7 +1198,7 @@ theorem CNF_aux {b o : ordinal} (b0 : b ≠ 0) (o0 : o ≠ 0) :
   o % b ^ log b o < o :=
 lt_of_lt_of_le
   (mod_lt _ $ power_ne_zero _ b0)
-  (power_log_le _ $ pos_iff_ne_zero.2 o0)
+  (power_log_le _ $ ordinal.pos_iff_ne_zero.2 o0)
 
 /-- Proving properties of ordinals by induction over their Cantor normal form. -/
 @[elab_as_eliminator] noncomputable def CNF_rec {b : ordinal} (b0 : b ≠ 0)
@@ -1262,7 +1262,7 @@ begin
     refine ⟨⟨le_refl _, λ p m, _⟩, λ p m, _⟩,
     { exact le_trans (IH₁ p m) (log_le_log _ $ le_of_lt H) },
     { refine lt_of_le_of_lt (IH₁ p m) ((log_lt b1 _).2 _),
-      { rw pos_iff_ne_zero, intro e,
+      { rw ordinal.pos_iff_ne_zero, intro e,
         rw e at m, simpa only [CNF_zero] using m },
       { exact mod_lt _ (power_ne_zero _ b0) } } },
   { by_cases o0 : o = 0,
@@ -1424,7 +1424,7 @@ theorem omega_le {o : ordinal.{u}} : omega ≤ o ↔ ∀ n : ℕ, (n : ordinal)
    by rw [e, ← succ_le]; exact H (n+1)⟩
 
 theorem nat_lt_limit {o} (h : is_limit o) : ∀ n : ℕ, (n : ordinal) < o
-| 0     := lt_of_le_of_ne (zero_le o) h.1.symm
+| 0     := lt_of_le_of_ne (ordinal.zero_le o) h.1.symm
 | (n+1) := h.2 _ (nat_lt_limit n)
 
 theorem omega_le_of_is_limit {o} (h : is_limit o) : omega ≤ o :=
@@ -1460,7 +1460,7 @@ begin
       (le_of_lt $ lt_sub.1 $ nat_lt_limit (sub_is_limit l hx) _) },
   { rcases h with ⟨a0, b, rfl⟩,
     refine mul_is_limit_left omega_is_limit
-      (pos_iff_ne_zero.2 $ mt _ a0),
+      (ordinal.pos_iff_ne_zero.2 $ mt _ a0),
     intro e, simp only [e, mul_zero] }
 end
 
@@ -1475,7 +1475,7 @@ theorem add_omega_power {a b : ordinal} (h : a < omega ^ b) : a + omega ^ b = om
 begin
   refine le_antisymm _ (le_add_left _ _),
   revert h, apply limit_rec_on b,
-  { intro h, rw [power_zero, ← succ_zero, lt_succ, le_zero] at h,
+  { intro h, rw [power_zero, ← succ_zero, lt_succ, ordinal.le_zero] at h,
     rw [h, zero_add] },
   { intros b _ h, rw [power_succ] at h,
     rcases (lt_mul_of_limit omega_is_limit).1 h with ⟨x, xo, ax⟩,
@@ -1627,7 +1627,7 @@ begin
   { rwa le_antisymm (H.nfp_le_fp (le_refl _) aa) (le_nfp_self _ _) },
   rcases zero_or_succ_or_limit (nfp f a) with e|⟨b, e⟩|l,
   { refine @le_trans _ _ _ (f a) _ (H.le_iff.2 _) (iterate_le_nfp f a 1),
-    simp only [e, zero_le] },
+    simp only [e, ordinal.zero_le] },
   { have : f b < nfp f a := H.lt_nfp.2 (by simp only [e, lt_succ_self]),
     rw [e, lt_succ] at this,
     have ab : a ≤ b,
@@ -1687,7 +1687,7 @@ theorem is_normal.fp_iff_deriv {f} (H : is_normal f)
   { intros h₁,
     refine ⟨0, le_antisymm h₁ _⟩,
     rw deriv_zero,
-    exact H.nfp_le_fp (zero_le _) ha },
+    exact H.nfp_le_fp (ordinal.zero_le _) ha },
   { intros o IH h₁,
     cases le_or_lt a (deriv f o), {exact IH h},
     refine ⟨succ o, le_antisymm h₁ _⟩,
diff --git a/src/set_theory/ordinal_notation.lean b/src/set_theory/ordinal_notation.lean
index c51d6d58361d1..3adbb35589c0c 100644
--- a/src/set_theory/ordinal_notation.lean
+++ b/src/set_theory/ordinal_notation.lean
@@ -175,7 +175,7 @@ by cases h with _ _ _ _ eb _ h₁ h₂ h₃; exact h₃
 
 theorem NF_below_zero : ∀ {o}, NF_below o 0 ↔ o = 0
 | 0            := ⟨λ _, rfl, λ _, NF_below.zero⟩
-| (oadd e n a) := ⟨λ h, (not_le_of_lt h.lt).elim (zero_le _),
+| (oadd e n a) := ⟨λ h, (not_le_of_lt h.lt).elim (ordinal.zero_le _),
                    λ e, e.symm ▸ NF_below.zero⟩
 
 theorem NF.zero_of_zero {e n a} (h : NF (oadd e n a)) (e0 : e = 0) : a = 0 :=
@@ -674,7 +674,7 @@ begin
   cases le_or_lt ω (repr e) with h h,
   { apply le_trans (mul_le_mul_left _ $ le_of_lt $ lt_succ_self _),
     rw [succ, add_mul_succ _ (one_add_of_omega_le h), ← succ,
-        succ_le, mul_lt_mul_iff_left (pos_iff_ne_zero.2 e0)],
+        succ_le, mul_lt_mul_iff_left (ordinal.pos_iff_ne_zero.2 e0)],
     exact omega_is_limit.2 _ l },
   { refine le_trans (le_of_lt $ mul_lt_omega (omega_is_limit.2 _ h) l) _,
     simpa using mul_le_mul_right ω (one_le_iff_ne_zero.2 e0) }
@@ -712,7 +712,7 @@ begin
     { rw power_mul, exact IH.1 k0 } },
   refine ⟨λ_, _, _⟩,
   { rw [RR, ← power_mul _ _ (succ k.succ)],
-    have e0 := pos_iff_ne_zero.2 e0,
+    have e0 := ordinal.pos_iff_ne_zero.2 e0,
     have rr0 := lt_of_lt_of_le e0 (le_add_left _ _),
     apply add_lt_omega_power,
     { simp [power_mul, ω0, power_add, mul_assoc],
@@ -762,7 +762,7 @@ begin
       cases NF_repr_split' e₂ with _ r₂,
       by_cases m = 0; simp [power_def, power, e₁, h, r₁, e₂, r₂, -nat.cast_succ],
       rw [power_add, power_mul, power_omega _ (nat_lt_omega _)],
-      simpa using nat_cast_lt.2 (nat.succ_lt_succ $ nat.pos_iff_ne_zero.2 h) } },
+      simpa using nat_cast_lt.2 (nat.succ_lt_succ $ pos_iff_ne_zero.2 h) } },
   { haveI := N₁.fst, haveI := N₁.snd,
     cases N₁.of_dvd_omega (split_dvd e₁) with a00 ad,
     have al := split_add_lt e₁,
diff --git a/src/topology/algebra/infinite_sum.lean b/src/topology/algebra/infinite_sum.lean
index 5f659d01e70e7..46948cea4be7d 100644
--- a/src/topology/algebra/infinite_sum.lean
+++ b/src/topology/algebra/infinite_sum.lean
@@ -761,7 +761,7 @@ lemma has_sum_zero_iff : has_sum f 0 ↔ ∀ x, f x = 0 :=
 begin
   refine ⟨_, λ h, _⟩,
   { contrapose!,
-    exact λ ⟨x, hx⟩ h, irrefl _ (lt_of_lt_of_le (zero_lt_iff_ne_zero.2 hx) (le_has_sum' h x)) },
+    exact λ ⟨x, hx⟩ h, irrefl _ (lt_of_lt_of_le (pos_iff_ne_zero.2 hx) (le_has_sum' h x)) },
   { convert has_sum_zero,
     exact funext h }
 end
diff --git a/src/topology/instances/ennreal.lean b/src/topology/instances/ennreal.lean
index 6897853c2a8fe..67ff29a58fbbb 100644
--- a/src/topology/instances/ennreal.lean
+++ b/src/topology/instances/ennreal.lean
@@ -229,7 +229,7 @@ protected lemma tendsto_mul (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : b ≠ 0 ∨ a ≠
 have ht : ∀b:ennreal, b ≠ 0 → tendsto (λp:ennreal×ennreal, p.1 * p.2) (𝓝 ((⊤:ennreal), b)) (𝓝 ⊤),
 begin
   refine assume b hb, tendsto_nhds_top_iff_nnreal.2 $ assume n, _,
-  rcases lt_iff_exists_nnreal_btwn.1 (zero_lt_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩,
+  rcases lt_iff_exists_nnreal_btwn.1 (pos_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩,
   replace hε : 0 < ε, from coe_pos.1 hε,
   filter_upwards [prod_mem_nhds_sets (lt_mem_nhds $ @coe_lt_top (n / ε)) (lt_mem_nhds hεb)],
   rintros ⟨a₁, a₂⟩ ⟨h₁, h₂⟩,
@@ -402,7 +402,7 @@ begin
   { simp only [not_forall] at hs,
     rcases hs with ⟨x, hx, hx0⟩,
     have s₁ : Sup s ≠ 0 :=
-      zero_lt_iff_ne_zero.1 (lt_of_lt_of_le (zero_lt_iff_ne_zero.2 hx0) (le_Sup hx)),
+      pos_iff_ne_zero.1 (lt_of_lt_of_le (pos_iff_ne_zero.2 hx0) (le_Sup hx)),
     have : Sup ((λb, a * b) '' s) = a * Sup s :=
       is_lub.Sup_eq (is_lub_of_is_lub_of_tendsto
         (assume x _ y _ h, canonically_ordered_semiring.mul_le_mul (le_refl _) h)
diff --git a/src/topology/metric_space/antilipschitz.lean b/src/topology/metric_space/antilipschitz.lean
index 556d0e0752596..0a720176cc78b 100644
--- a/src/topology/metric_space/antilipschitz.lean
+++ b/src/topology/metric_space/antilipschitz.lean
@@ -42,7 +42,7 @@ lemma antilipschitz_with.mul_le_dist [metric_space α] [metric_space β] {K : 
 begin
   by_cases hK : K = 0, by simp [hK, dist_nonneg],
   rw [nnreal.coe_inv, ← div_eq_inv_mul],
-  rw div_le_iff' (nnreal.coe_pos.2 $ zero_lt_iff_ne_zero.2 hK),
+  rw div_le_iff' (nnreal.coe_pos.2 $ pos_iff_ne_zero.2 hK),
   exact hf.le_mul_dist x y
 end
 
diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean
index 66bb65c175a29..4572a62ecd7f9 100644
--- a/src/topology/metric_space/emetric_space.lean
+++ b/src/topology/metric_space/emetric_space.lean
@@ -114,7 +114,7 @@ iff.intro (assume h, eq_of_edist_eq_zero (h.symm))
           (assume : x = y, this ▸ (edist_self _).symm)
 
 theorem edist_le_zero {x y : α} : (edist x y ≤ 0) ↔ x = y :=
-le_zero_iff_eq.trans edist_eq_zero
+nonpos_iff_eq_zero.trans edist_eq_zero
 
 /-- Triangle inequality for the extended distance -/
 theorem edist_triangle_left (x y z : α) : edist x y ≤ edist z x + edist z y :=
@@ -713,7 +713,7 @@ diam_le_iff_forall_edist_le.2 h
 
 /-- The diameter of a subsingleton vanishes. -/
 lemma diam_subsingleton (hs : s.subsingleton) : diam s = 0 :=
-le_zero_iff_eq.1 $ diam_le_of_forall_edist_le $
+nonpos_iff_eq_zero.1 $ diam_le_of_forall_edist_le $
 λ x hx y hy, (hs hx hy).symm ▸ edist_self y ▸ le_refl _
 
 /-- The diameter of the empty set vanishes -/
@@ -732,7 +732,7 @@ begin
   have := not_congr (@diam_eq_zero_iff _ _ s),
   dunfold set.subsingleton at this,
   push_neg at this,
-  simpa only [zero_lt_iff_ne_zero, exists_prop] using this
+  simpa only [pos_iff_ne_zero, exists_prop] using this
 end
 
 lemma diam_insert : diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s) :=
diff --git a/src/topology/metric_space/gluing.lean b/src/topology/metric_space/gluing.lean
index 8d6ae28faf350..30b5b1d7e2ba2 100644
--- a/src/topology/metric_space/gluing.lean
+++ b/src/topology/metric_space/gluing.lean
@@ -408,7 +408,7 @@ lemma inductive_limit_dist_eq_dist (I : ∀n, isometry (f n))
 begin
   induction m with m hm,
   { assume hx hy,
-    have A : max x.1 y.1 = 0, { rw [le_zero_iff_eq.1 hx, le_zero_iff_eq.1 hy], simp },
+    have A : max x.1 y.1 = 0, { rw [nonpos_iff_eq_zero.1 hx, nonpos_iff_eq_zero.1 hy], simp },
     unfold inductive_limit_dist,
     congr; simp only [A] },
   { assume hx hy,
diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean
index 619c260d1abda..91d952148d530 100644
--- a/src/topology/metric_space/hausdorff_distance.lean
+++ b/src/topology/metric_space/hausdorff_distance.lean
@@ -58,7 +58,7 @@ Inf_le ((mem_image _ _ _).2 ⟨y, h, by refl⟩)
 
 /-- If a point `x` belongs to `s`, then its edist to `s` vanishes -/
 lemma inf_edist_zero_of_mem (h : x ∈ s) : inf_edist x s = 0 :=
-le_zero_iff_eq.1 $ @edist_self _ _ x ▸ inf_edist_le_edist_of_mem h
+nonpos_iff_eq_zero.1 $ @edist_self _ _ x ▸ inf_edist_le_edist_of_mem h
 
 /-- The edist is monotonous with respect to inclusion -/
 lemma inf_edist_le_inf_edist_of_subset (h : s ⊆ t) : inf_edist x t ≤ inf_edist x s :=
@@ -298,7 +298,7 @@ end
 lemma Hausdorff_edist_self_closure : Hausdorff_edist s (closure s) = 0 :=
 begin
   erw ← le_bot_iff,
-  simp only [Hausdorff_edist, inf_edist_closure, -le_zero_iff_eq, and_imp,
+  simp only [Hausdorff_edist, inf_edist_closure, -nonpos_iff_eq_zero, and_imp,
     set.mem_image, Sup_le_iff, exists_imp_distrib, sup_le_iff,
     set.ball_image_iff, ennreal.bot_eq_zero, -mem_image],
   simp only [inf_edist_zero_of_mem, mem_closure_iff_inf_edist_zero, le_refl, and_self,
diff --git a/test/library_search/nat.lean b/test/library_search/nat.lean
index a8f8b1f6604bc..2f88dfda03f36 100644
--- a/test/library_search/nat.lean
+++ b/test/library_search/nat.lean
@@ -74,7 +74,7 @@ by library_search -- Says: `exact nat.mul_div_left a h`
 example (a b : ℕ) (h : b ≠ 0) : (a * b) / b = a :=
 begin
   success_if_fail { library_search },
-  library_search [nat.pos_iff_ne_zero.mpr],
+  library_search [pos_iff_ne_zero.mpr],
 end
 
 end test.library_search