fix(*): remove usages of ge/gt (#3808)

These were not caught by the old `ge_or_gt` linter, but they will be caught by the new (upcoming) `ge_or_gt` linter.
The `nolint` flags are not yet removed, this will happen in a later PR.
Renamings:
```
char_is_prime_of_ge_two -> char_is_prime_of_two_le
dist_eq_sub_of_ge -> dist_eq_sub_of_le_right
gt_of_mul_lt_mul_neg_right -> lt_of_mul_lt_mul_neg_right
```

Author: fpvandoorn

scripts/nolints.txt

@@ -1791,7 +1791,7 @@ apply_nolint tactic.interactive.solve_mvar doc_blame
 apply_nolint tactic.interactive.unify_with_instance doc_blame
 
 -- tactic/monotonicity/lemmas.lean
-apply_nolint gt_of_mul_lt_mul_neg_right ge_or_gt
+apply_nolint lt_of_mul_lt_mul_neg_right ge_or_gt
 
 -- tactic/norm_num.lean
 apply_nolint norm_num.derive doc_blame
@@ -2110,4 +2110,4 @@ apply_nolint uniform_space.completion.map₂ doc_blame
 
 -- topology/uniform_space/uniform_embedding.lean
 apply_nolint uniform_embedding doc_blame
-apply_nolint uniform_inducing doc_blame
+apply_nolint uniform_inducing doc_blame

src/algebra/char_p.lean

@@ -214,7 +214,7 @@ assume hp : p = 1,
 have ( 1 : α) = 0, by simpa using (cast_eq_zero_iff α p 1).mpr (hp ▸ dvd_refl p),
 absurd this one_ne_zero
 
-theorem char_is_prime_of_ge_two (p : ℕ) [hc : char_p α p] (hp : p ≥ 2) : nat.prime p :=
+theorem char_is_prime_of_two_le (p : ℕ) [hc : char_p α p] (hp : 2 ≤ p) : nat.prime p :=
 suffices ∀d ∣ p, d = 1 ∨ d = p, from ⟨hp, this⟩,
 assume (d : ℕ) (hdvd : ∃ e, p = d * e),
 let ⟨e, hmul⟩ := hdvd in
@@ -236,7 +236,7 @@ theorem char_is_prime_or_zero (p : ℕ) [hc : char_p α p] : nat.prime p ∨ p =
 match p, hc with
 | 0,     _  := or.inr rfl
 | 1,     hc := absurd (eq.refl (1 : ℕ)) (@char_ne_one α _ (1 : ℕ) hc)
-| (m+2), hc := or.inl (@char_is_prime_of_ge_two α _ (m+2) hc (nat.le_add_left 2 m))
+| (m+2), hc := or.inl (@char_is_prime_of_two_le α _ (m+2) hc (nat.le_add_left 2 m))
 end
 
 lemma char_is_prime_of_pos (p : ℕ) [h : fact (0 < p)] [char_p α p] : fact p.prime :=

src/algebra/order_functions.lean

@@ -181,17 +181,17 @@ calc  abs a
     ≤ b : by { apply abs_le_of_le_of_neg_le; assumption }
 ... ≤ abs b : le_abs_self _
 
-lemma min_le_add_of_nonneg_right {a b : α} (hb : b ≥ 0) : min a b ≤ a + b :=
+lemma min_le_add_of_nonneg_right {a b : α} (hb : 0 ≤ b) : min a b ≤ a + b :=
 calc
   min a b ≤ a     : by apply min_le_left
       ... ≤ a + b : le_add_of_nonneg_right hb
 
-lemma min_le_add_of_nonneg_left {a b : α} (ha : a ≥ 0) : min a b ≤ a + b :=
+lemma min_le_add_of_nonneg_left {a b : α} (ha : 0 ≤ a) : min a b ≤ a + b :=
 calc
   min a b ≤ b     : by apply min_le_right
       ... ≤ a + b : le_add_of_nonneg_left ha
 
-lemma max_le_add_of_nonneg {a b : α} (ha : a ≥ 0) (hb : b ≥ 0) : max a b ≤ a + b :=
+lemma max_le_add_of_nonneg {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : max a b ≤ a + b :=
 max_le_iff.2 (by split; simpa)
 
 lemma max_zero_sub_eq_self (a : α) : max a 0 - max (-a) 0 = a :=

src/data/nat/basic.lean

@@ -113,7 +113,7 @@ theorem le_mul_self : Π (n : ℕ), n ≤ n * n
 | 0     := le_refl _
 | (n+1) := let t := mul_le_mul_left (n+1) (succ_pos n) in by simp at t; exact t
 
-theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
+theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : 0 < m) (H : n * m = k * m) : n = k :=
 by rw [mul_comm n m, mul_comm k m] at H; exact eq_of_mul_eq_mul_left Hm H
 
 theorem one_add (n : ℕ) : 1 + n = succ n := by simp [add_comm]

src/data/nat/dist.lean

@@ -35,11 +35,11 @@ begin rw [h, dist_self] end
 theorem dist_eq_sub_of_le {n m : ℕ} (h : n ≤ m) : dist n m = m - n :=
 begin rw [dist.def, sub_eq_zero_of_le h, zero_add] end
 
-theorem dist_eq_sub_of_ge {n m : ℕ} (h : n ≥ m) : dist n m = n - m :=
+theorem dist_eq_sub_of_le_right {n m : ℕ} (h : m ≤ n) : dist n m = n - m :=
 begin rw [dist_comm], apply dist_eq_sub_of_le h end
 
 theorem dist_zero_right (n : ℕ) : dist n 0 = n :=
-eq.trans (dist_eq_sub_of_ge (zero_le n)) (nat.sub_zero n)
+eq.trans (dist_eq_sub_of_le_right (zero_le n)) (nat.sub_zero n)
 
 theorem dist_zero_left (n : ℕ) : dist 0 n = n :=
 eq.trans (dist_eq_sub_of_le (zero_le n)) (nat.sub_zero n)
@@ -87,7 +87,7 @@ or.elim (lt_or_ge i j)
   (assume : i < j,
     by rw [max_eq_right_of_lt this, min_eq_left_of_lt this, dist_eq_sub_of_lt this])
   (assume : i ≥ j,
-    by rw [max_eq_left this , min_eq_right this, dist_eq_sub_of_ge this])
+    by rw [max_eq_left this , min_eq_right this, dist_eq_sub_of_le_right this])
 -/
 
 theorem dist_succ_succ {i j : nat} : dist (succ i) (succ j) = dist i j :=
@@ -99,6 +99,6 @@ assume hne, nat.lt_by_cases
      begin rw [dist_eq_sub_of_le (le_of_lt this)], apply nat.sub_pos_of_lt this end)
   (assume : i = j, by contradiction)
   (assume : i > j,
-     begin rw [dist_eq_sub_of_ge (le_of_lt this)], apply nat.sub_pos_of_lt this end)
+     begin rw [dist_eq_sub_of_le_right (le_of_lt this)], apply nat.sub_pos_of_lt this end)
 
 end nat

src/data/num/lemmas.lean

@@ -97,7 +97,7 @@ theorem cmp_swap (m) : ∀n, (cmp m n).swap = cmp n m :=
 by induction m with m IH m IH; intro n;
    cases n with n n; try {unfold cmp}; try {refl}; rw ←IH; cases cmp m n; refl
 
-theorem cmp_to_nat : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℕ) < n) (m = n) ((m:ℕ) > n) : Prop)
+theorem cmp_to_nat : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℕ) < n) (m = n) ((n:ℕ) < m) : Prop)
 | 1        1        := rfl
 | (bit0 a) 1        := let h : (1:ℕ) ≤ a := to_nat_pos a in add_le_add h h
 | (bit1 a) 1        := nat.succ_lt_succ $ to_nat_pos $ bit0 a
@@ -227,7 +227,7 @@ theorem mul_to_nat : ∀ m n, ((m * n : num) : ℕ) = m * n
 | (pos p) 0       := rfl
 | (pos p) (pos q) := pos_num.mul_to_nat _ _
 
-theorem cmp_to_nat : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℕ) < n) (m = n) ((m:ℕ) > n) : Prop)
+theorem cmp_to_nat : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℕ) < n) (m = n) ((n:ℕ) < m) : Prop)
 | 0       0       := rfl
 | 0       (pos b) := to_nat_pos _
 | (pos a) 0       := to_nat_pos _
@@ -517,7 +517,7 @@ end num
 namespace pos_num
 open num
 
-theorem pred_to_nat {n : pos_num} (h : n > 1) : (pred n : ℕ) = nat.pred n :=
+theorem pred_to_nat {n : pos_num} (h : 1 < n) : (pred n : ℕ) = nat.pred n :=
 begin
   unfold pred,
   have := pred'_to_nat n,
@@ -950,7 +950,7 @@ of_int_cast n
 | (n : ℕ) := to_int_inj.1 $ by simp [znum.of_int']
 | -[1+ n] := to_int_inj.1 $ by simp [znum.of_int']
 
-theorem cmp_to_int : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℤ) < n) (m = n) ((m:ℤ) > n) : Prop)
+theorem cmp_to_int : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℤ) < n) (m = n) ((n:ℤ) < m) : Prop)
 | 0       0       := rfl
 | (pos a) (pos b) := begin
     have := pos_num.cmp_to_nat a b; revert this; dsimp [cmp];

src/data/padics/padic_numbers.lean

@@ -95,7 +95,7 @@ def stationary_point {f : padic_seq p} (hf : ¬ f ≈ 0) : ℕ :=
 classical.some $ stationary hf
 
 lemma stationary_point_spec {f : padic_seq p} (hf : ¬ f ≈ 0) :
-  ∀ {m n}, m ≥ stationary_point hf → n ≥ stationary_point hf →
+  ∀ {m n}, stationary_point hf ≤ m → stationary_point hf ≤ n →
     padic_norm p (f n) = padic_norm p (f m) :=
 classical.some_spec $ stationary hf
 
@@ -147,7 +147,7 @@ lemma not_lim_zero_const_of_nonzero {q : ℚ} (hq : q ≠ 0) : ¬ lim_zero (cons
 lemma not_equiv_zero_const_of_nonzero {q : ℚ} (hq : q ≠ 0) : ¬ (const (padic_norm p) q) ≈ 0 :=
 λ h : lim_zero (const (padic_norm p) q - 0), not_lim_zero_const_of_nonzero hq $ by simpa using h
 
-lemma norm_nonneg (f : padic_seq p) : f.norm ≥ 0 :=
+lemma norm_nonneg (f : padic_seq p) : 0 ≤ f.norm :=
 if hf : f ≈ 0 then by simp [hf, norm]
 else by simp [norm, hf, padic_norm.nonneg]
 
@@ -265,22 +265,22 @@ by simp [h1, norm, hp.one_lt]
 
 private lemma norm_eq_of_equiv_aux {f g : padic_seq p} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) (hfg : f ≈ g)
   (h : padic_norm p (f (stationary_point hf)) ≠ padic_norm p (g (stationary_point hg)))
-  (hgt : padic_norm p (f (stationary_point hf)) > padic_norm p (g (stationary_point hg))) :
+  (hlt : padic_norm p (g (stationary_point hg)) < padic_norm p (f (stationary_point hf))) :
   false :=
 begin
-  have hpn : padic_norm p (f (stationary_point hf)) - padic_norm p (g (stationary_point hg)) > 0,
-    from sub_pos_of_lt hgt,
+  have hpn : 0 < padic_norm p (f (stationary_point hf)) - padic_norm p (g (stationary_point hg)),
+    from sub_pos_of_lt hlt,
   cases hfg _ hpn with N hN,
   let i := max N (max (stationary_point hf) (stationary_point hg)),
-  have hi : i ≥ N, from le_max_left _ _,
+  have hi : N ≤ i, from le_max_left _ _,
   have hN' := hN _ hi,
-  padic_index_simp [N, hf, hg] at hN' h hgt,
+  padic_index_simp [N, hf, hg] at hN' h hlt,
   have hpne : padic_norm p (f i) ≠ padic_norm p (-(g i)),
     by rwa [ ←padic_norm.neg p (g i)] at h,
   let hpnem := add_eq_max_of_ne p hpne,
   have hpeq : padic_norm p ((f - g) i) = max (padic_norm p (f i)) (padic_norm p (g i)),
   { rwa padic_norm.neg at hpnem },
-  rw [hpeq, max_eq_left_of_lt hgt] at hN',
+  rw [hpeq, max_eq_left_of_lt hlt] at hN',
   have : padic_norm p (f i) < padic_norm p (f i),
   { apply lt_of_lt_of_le hN', apply sub_le_self, apply padic_norm.nonneg },
   exact lt_irrefl _ this
@@ -290,13 +290,13 @@ private lemma norm_eq_of_equiv {f g : padic_seq p} (hf : ¬ f ≈ 0) (hg : ¬ g
   padic_norm p (f (stationary_point hf)) = padic_norm p (g (stationary_point hg)) :=
 begin
   by_contradiction h,
-  cases (decidable.em (padic_norm p (f (stationary_point hf)) >
-          padic_norm p (g (stationary_point hg))))
-      with hgt hngt,
-  { exact norm_eq_of_equiv_aux hf hg hfg h hgt },
+  cases (decidable.em (padic_norm p (g (stationary_point hg)) <
+          padic_norm p (f (stationary_point hf))))
+      with hlt hnlt,
+  { exact norm_eq_of_equiv_aux hf hg hfg h hlt },
   { apply norm_eq_of_equiv_aux hg hf (setoid.symm hfg) (ne.symm h),
     apply lt_of_le_of_ne,
-    apply le_of_not_gt hngt,
+    apply le_of_not_gt hnlt,
     apply h }
 end
 
@@ -501,28 +501,28 @@ section embedding
 open padic_seq
 variables {p : ℕ} [fact p.prime]
 
-lemma defn (f : padic_seq p) {ε : ℚ} (hε : ε > 0) : ∃ N, ∀ i ≥ N, padic_norm_e (⟦f⟧ - f i) < ε :=
+lemma defn (f : padic_seq p) {ε : ℚ} (hε : 0 < ε) : ∃ N, ∀ i ≥ N, padic_norm_e (⟦f⟧ - f i) < ε :=
 begin
   simp only [padic.cast_eq_of_rat],
   change ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε,
   by_contradiction h,
   cases cauchy₂ f hε with N hN,
-  have : ∀ N, ∃ i ≥ N, (f - const _ (f i)).norm ≥ ε,
+  have : ∀ N, ∃ i ≥ N, ε ≤ (f - const _ (f i)).norm,
     by simpa [not_forall] using h,
   rcases this N with ⟨i, hi, hge⟩,
   have hne : ¬ (f - const (padic_norm p) (f i)) ≈ 0,
   { intro h, unfold padic_seq.norm at hge; split_ifs at hge, exact not_lt_of_ge hge hε },
   unfold padic_seq.norm at hge; split_ifs at hge,
   apply not_le_of_gt _ hge,
-  cases decidable.em ((stationary_point hne) ≥ N) with hgen hngen,
+  cases decidable.em (N ≤ stationary_point hne) with hgen hngen,
   { apply hN; assumption },
   { have := stationary_point_spec hne (le_refl _) (le_of_not_le hngen),
     rw ←this,
     apply hN,
     apply le_refl, assumption }
 end
 
-protected lemma nonneg (q : ℚ_[p]) : padic_norm_e q ≥ 0 :=
+protected lemma nonneg (q : ℚ_[p]) : 0 ≤ padic_norm_e q :=
 quotient.induction_on q $ norm_nonneg
 
 lemma zero_def : (0 : ℚ_[p]) = ⟦0⟧ := rfl
@@ -595,7 +595,7 @@ namespace padic
 section complete
 open padic_seq padic
 
-theorem rat_dense' {p : ℕ} [fact p.prime] (q : ℚ_[p]) {ε : ℚ} (hε : ε > 0) :
+theorem rat_dense' {p : ℕ} [fact p.prime] (q : ℚ_[p]) {ε : ℚ} (hε : 0 < ε) :
   ∃ r : ℚ, padic_norm_e (q - r) < ε :=
 quotient.induction_on q $ λ q',
   have ∃ N, ∀ m n ≥ N, padic_norm p (q' m - q' n) < ε, from cauchy₂ _ hε,
@@ -609,7 +609,7 @@ quotient.induction_on q $ λ q',
       { simp only [padic_seq.norm, dif_neg hne'],
         change padic_norm p (q' _ - q' _) < ε,
         have := stationary_point_spec hne',
-        cases decidable.em (N ≥ stationary_point hne') with hle hle,
+        cases decidable.em (stationary_point hne' ≤ N) with hle hle,
         { have := eq.symm (this (le_refl _) hle),
           simp at this, simpa [this] },
         { apply hN,
@@ -619,7 +619,7 @@ quotient.induction_on q $ λ q',
 variables {p : ℕ} [fact p.prime] (f : cau_seq _ (@padic_norm_e p _))
 open classical
 
-private lemma div_nat_pos (n : ℕ) : (1 / ((n + 1): ℚ)) > 0 :=
+private lemma div_nat_pos (n : ℕ) : 0 < (1 / ((n + 1): ℚ)) :=
 div_pos zero_lt_one (by exact_mod_cast succ_pos _)
 
 def lim_seq : ℕ → ℚ := λ n, classical.some (rat_dense' (f n) (div_nat_pos n))
@@ -638,7 +638,7 @@ end
 
 lemma exi_rat_seq_conv_cauchy : is_cau_seq (padic_norm p) (lim_seq f) :=
 assume ε hε,
-have hε3 : ε / 3 > 0, from div_pos hε (by norm_num),
+have hε3 : 0 < ε / 3, from div_pos hε (by norm_num),
 let ⟨N, hN⟩ := exi_rat_seq_conv f hε3,
     ⟨N2, hN2⟩ := f.cauchy₂ hε3 in
 begin
@@ -677,8 +677,8 @@ private def lim : ℚ_[p] := ⟦lim' f⟧
 theorem complete' : ∃ q : ℚ_[p], ∀ ε > 0, ∃ N, ∀ i ≥ N, padic_norm_e (q - f i) < ε :=
 ⟨ lim f,
   λ ε hε,
-  let ⟨N, hN⟩ := exi_rat_seq_conv f (show ε / 2 > 0, from div_pos hε (by norm_num)),
-      ⟨N2, hN2⟩ := padic_norm_e.defn (lim' f) (show ε / 2 > 0, from div_pos hε (by norm_num)) in
+  let ⟨N, hN⟩ := exi_rat_seq_conv f (show 0 < ε / 2, from div_pos hε (by norm_num)),
+      ⟨N2, hN2⟩ := padic_norm_e.defn (lim' f) (show 0 < ε / 2, from div_pos hε (by norm_num)) in
   begin
     existsi max N N2,
     intros i hi,
@@ -730,7 +730,7 @@ instance : is_absolute_value (λ a : ℚ_[p], ∥a∥) :=
   abv_add := norm_add_le,
   abv_mul := by simp [has_norm.norm, padic_norm_e.mul'] }
 
-theorem rat_dense {p : ℕ} {hp : fact p.prime} (q : ℚ_[p]) {ε : ℝ} (hε : ε > 0) :
+theorem rat_dense {p : ℕ} {hp : fact p.prime} (q : ℚ_[p]) {ε : ℝ} (hε : 0 < ε) :
         ∃ r : ℚ, ∥q - r∥ < ε :=
 let ⟨ε', hε'l, hε'r⟩ := exists_rat_btwn hε,
     ⟨r, hr⟩ := rat_dense' q (by simpa using hε'l)  in
@@ -858,7 +858,7 @@ begin
   exact_mod_cast hN i hi
 end
 
-lemma padic_norm_e_lim_le {f : cau_seq ℚ_[p] norm} {a : ℝ} (ha : a > 0)
+lemma padic_norm_e_lim_le {f : cau_seq ℚ_[p] norm} {a : ℝ} (ha : 0 < a)
       (hf : ∀ i, ∥f i∥ ≤ a) : ∥f.lim∥ ≤ a :=
 let ⟨N, hN⟩ := setoid.symm (cau_seq.equiv_lim f) _ ha in
 calc ∥f.lim∥ = ∥f.lim - f N + f N∥ : by simp

src/data/polynomial/degree/basic.lean

@@ -76,7 +76,7 @@ lemma degree_eq_iff_nat_degree_eq {p : polynomial R} {n : ℕ} (hp : p ≠ 0) :
   p.degree = n ↔ p.nat_degree = n :=
 by rw [degree_eq_nat_degree hp, with_bot.coe_eq_coe]
 
-lemma degree_eq_iff_nat_degree_eq_of_pos {p : polynomial R} {n : ℕ} (hn : n > 0) :
+lemma degree_eq_iff_nat_degree_eq_of_pos {p : polynomial R} {n : ℕ} (hn : 0 < n) :
   p.degree = n ↔ p.nat_degree = n :=
 begin
   split,

src/data/real/basic.lean

@@ -153,7 +153,7 @@ noncomputable instance decidable_lt (a b : ℝ) : decidable (a < b) := by apply_
 noncomputable instance decidable_le (a b : ℝ) : decidable (a ≤ b) := by apply_instance
 noncomputable instance decidable_eq (a b : ℝ) : decidable (a = b) := by apply_instance
 
-lemma le_of_forall_epsilon_le {a b : real} (h : ∀ε, ε > 0 → a ≤ b + ε) : a ≤ b :=
+lemma le_of_forall_epsilon_le {a b : real} (h : ∀ε, 0 < ε → a ≤ b + ε) : a ≤ b :=
 le_of_forall_le_of_dense $ assume x hxb,
 calc  a ≤ b + (x - b) : h (x-b) $ sub_pos.2 hxb
     ... = x : by rw [add_comm]; simp

src/data/real/cau_seq.lean

@@ -169,7 +169,7 @@ variables {α : Type*} [discrete_linear_ordered_field α]
   {β : Type*} [ring β] {abv : β → α} [is_absolute_value abv] {f : ℕ → β}
 
 @[nolint ge_or_gt] -- see Note [nolint_ge]
-theorem cauchy₂ (hf : is_cau_seq abv f) {ε : α} (ε0 : ε > 0) :
+theorem cauchy₂ (hf : is_cau_seq abv f) {ε : α} (ε0 : 0 < ε) :
   ∃ i, ∀ j k ≥ i, abv (f j - f k) < ε :=
 begin
   refine (hf _ (half_pos ε0)).imp (λ i hi j k ij ik, _),
@@ -179,7 +179,7 @@ begin
 end
 
 @[nolint ge_or_gt] -- see Note [nolint_ge]
-theorem cauchy₃ (hf : is_cau_seq abv f) {ε : α} (ε0 : ε > 0) :
+theorem cauchy₃ (hf : is_cau_seq abv f) {ε : α} (ε0 : 0 < ε) :
   ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε :=
 let ⟨i, H⟩ := hf.cauchy₂ ε0 in ⟨i, λ j ij k jk, H _ _ (le_trans ij jk) ij⟩
 
@@ -209,7 +209,7 @@ theorem is_cau (f : cau_seq β abv) : is_cau_seq abv f := f.2
 
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem cauchy (f : cau_seq β abv) :
-  ∀ {ε}, ε > 0 → ∃ i, ∀ j ≥ i, abv (f j - f i) < ε := f.2
+  ∀ {ε}, 0 < ε → ∃ i, ∀ j ≥ i, abv (f j - f i) < ε := f.2
 
 /-- Given a Cauchy sequence `f`, create a Cauchy sequence from a sequence `g` with
 the same values as `f`. -/
@@ -219,11 +219,11 @@ def of_eq (f : cau_seq β abv) (g : ℕ → β) (e : ∀ i, f i = g i) : cau_seq
 variable [is_absolute_value abv]
 
 @[nolint ge_or_gt] -- see Note [nolint_ge]
-theorem cauchy₂ (f : cau_seq β abv) {ε} : ε > 0 →
+theorem cauchy₂ (f : cau_seq β abv) {ε} : 0 < ε →
   ∃ i, ∀ j k ≥ i, abv (f j - f k) < ε := f.2.cauchy₂
 
 @[nolint ge_or_gt] -- see Note [nolint_ge]
-theorem cauchy₃ (f : cau_seq β abv) {ε} : ε > 0 →
+theorem cauchy₃ (f : cau_seq β abv) {ε} : 0 < ε →
   ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε := f.2.cauchy₃
 
 theorem bounded (f : cau_seq β abv) : ∃ r, ∀ i, abv (f i) < r :=
@@ -424,7 +424,7 @@ have hg' : ¬ lim_zero g, by simpa using (show ¬ lim_zero (g - 0), from hg),
 begin
   rcases abv_pos_of_not_lim_zero hf' with ⟨a1, ha1, N1, hN1⟩,
   rcases abv_pos_of_not_lim_zero hg' with ⟨a2, ha2, N2, hN2⟩,
-  have : a1 * a2 > 0, from mul_pos ha1 ha2,
+  have : 0 < a1 * a2, from mul_pos ha1 ha2,
   cases hlz _ this with N hN,
   let i := max N (max N1 N2),
   have hN' := hN i (le_max_left _ _),
@@ -456,12 +456,12 @@ variables {β : Type*} [integral_domain β] (abv : β → α) [is_absolute_value
 
 lemma one_not_equiv_zero : ¬ (const abv 1) ≈ (const abv 0) :=
 assume h,
-have ∀ ε > 0, ∃ i, ∀ k, k ≥ i → abv (1 - 0) < ε, from h,
+have ∀ ε > 0, ∃ i, ∀ k, i ≤ k → abv (1 - 0) < ε, from h,
 have h1 : abv 1 ≤ 0, from le_of_not_gt $
-  assume h2 : abv 1 > 0,
+  assume h2 : 0 < abv 1,
   exists.elim (this _ h2) $ λ i hi,
     lt_irrefl (abv 1) $ by simpa using hi _ (le_refl _),
-have h2 : abv 1 ≥ 0, from is_absolute_value.abv_nonneg _ _,
+have h2 : 0 ≤ abv 1, from is_absolute_value.abv_nonneg _ _,
 have abv 1 = 0, from le_antisymm h1 h2,
 have (1 : β) = 0, from (is_absolute_value.abv_eq_zero abv).1 this,
 absurd this one_ne_zero