chore(algebra/ordered_monoid): rename lemmas (#5657)

I wanted to add the alias `pos_iff_ne_zero` for `zero_lt_iff_ne_zero`, but then I saw a note already in the library to do this renaming. So I went ahead.

`le_zero_iff_eq` -> `nonpos_iff_eq_zero`
`zero_lt_iff_ne_zero` -> `pos_iff_ne_zero`
`le_one_iff_eq` -> `le_one_iff_eq_one`
`measure.le_zero_iff_eq_zero'` -> `measure.nonpos_iff_eq_zero'`

There were various specific types that had their own custom `pos_iff_ne_zero`-lemma, which caused nameclashes. Therefore:

* remove `nat.pos_iff_ne_zero`
* Prove that `cardinal` forms a `canonically_ordered_semiring`, remove various special case lemmas
* There were lemmas `cardinal.le_add_[left|right]`. Generalized them to arbitrary canonically_ordered_monoids and renamed them to `self_le_add_[left|right]` (to avoid name clashes)
* I did not provide a canonically_ordered_monoid class for ordinal, since that requires quite some work (it's true, right?)
* `protect` various lemmas in `cardinal` and `ordinal` to avoid name clashes.

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.

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),

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)

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
 

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
 

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 :=

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
 

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,

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⟩,

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

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 :=

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 :=

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),

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₄,

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 _ _

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) },

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)

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),

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
 

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
 

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,20 +129,20 @@ 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
 
 lemma gcd_fib_add_mul_self (m n : ℕ) : ∀ k, gcd (fib m) (fib (n + k * m)) = gcd (fib m) (fib n)
 | 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

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 :=

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,

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)

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 :=

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

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