chore(*): fix some ge_or_gt lint issues (#2945)

Also rename a few definitions:

* `ge_of_forall_ge_sub` : `le_of_forall_sub_le`;
* `power_series.order_ge_nat` : `power_series.nat_le_order`;
* `power_series.order_ge`: `power_series.le_order`;

src/algebra/ordered_field.lean

@@ -322,7 +322,7 @@ begin
   apply one_div_pos_of_pos he
 end
 
-lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a ∧ c > 0 :=
+lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a ∧ 0 < c :=
 begin
   apply exists.intro ((a - b) / (1 + 1)),
   split,
@@ -340,7 +340,7 @@ begin
   exact div_pos_of_pos_of_pos (sub_pos_of_lt h) two_pos
 end
 
-lemma ge_of_forall_ge_sub {a b : α} (h : ∀ ε : α, ε > 0 → a ≥ b - ε) : a ≥ b :=
+lemma le_of_forall_sub_le {a b : α} (h : ∀ ε > 0, b - ε ≤ a) : b ≤ a :=
 begin
   apply le_of_not_gt,
   intro hb,

src/algebra/ordered_group.lean

@@ -42,7 +42,7 @@ lemma add_le_add' (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
 le_trans (add_le_add_right' h₁) (add_le_add_left' h₂)
 
 lemma le_add_of_nonneg_right' (h : 0 ≤ b) : a ≤ a + b :=
-have a + b ≥ a + 0, from add_le_add_left' h,
+have a + 0 ≤ a + b, from add_le_add_left' h,
 by rwa add_zero at this
 
 lemma le_add_of_nonneg_left' (h : 0 ≤ b) : a ≤ b + a :=
@@ -452,11 +452,11 @@ end
 lemma add_le_add {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
 le_trans (add_le_add_right h₁ c) (add_le_add_left h₂ b)
 
-lemma le_add_of_nonneg_right (h : b ≥ 0) : a ≤ a + b :=
-have a + b ≥ a + 0, from add_le_add_left h a,
+lemma le_add_of_nonneg_right (h : 0 ≤ b) : a ≤ a + b :=
+have a + 0 ≤ a + b, from add_le_add_left h a,
 by rwa add_zero at this
 
-lemma le_add_of_nonneg_left (h : b ≥ 0) : a ≤ b + a :=
+lemma le_add_of_nonneg_left (h : 0 ≤ b) : a ≤ b + a :=
 have 0 + a ≤ b + a, from add_le_add_right h a,
 by rwa zero_add at this
 
@@ -469,11 +469,11 @@ lt_of_le_of_lt (add_le_add_right h₁ c) (add_lt_add_left h₂ b)
 lemma add_lt_add_of_lt_of_le (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d :=
 lt_of_lt_of_le (add_lt_add_right h₁ c) (add_le_add_left h₂ b)
 
-lemma lt_add_of_pos_right (a : α) {b : α} (h : b > 0) : a < a + b :=
+lemma lt_add_of_pos_right (a : α) {b : α} (h : 0 < b) : a < a + b :=
 have a + 0 < a + b, from add_lt_add_left h a,
 by rwa [add_zero] at this
 
-lemma lt_add_of_pos_left (a : α) {b : α} (h : b > 0) : a < b + a :=
+lemma lt_add_of_pos_left (a : α) {b : α} (h : 0 < b) : a < b + a :=
 have 0 + a < b + a, from add_lt_add_right h a,
 by rwa [zero_add] at this
 
@@ -1077,13 +1077,13 @@ add_lt_add_of_le_of_lt hab (neg_lt_neg hcd)
 lemma sub_lt_sub_of_lt_of_le (hab : a < b) (hcd : c ≤ d) : a - d < b - c :=
 add_lt_add_of_lt_of_le hab (neg_le_neg hcd)
 
-lemma sub_le_self (a : α) {b : α} (h : b ≥ 0) : a - b ≤ a :=
+lemma sub_le_self (a : α) {b : α} (h : 0 ≤ b) : a - b ≤ a :=
 calc
   a - b = a + -b : rfl
     ... ≤ a + 0  : add_le_add_left (neg_nonpos_of_nonneg h) _
     ... = a      : by rw add_zero
 
-lemma sub_lt_self (a : α) {b : α} (h : b > 0) : a - b < a :=
+lemma sub_lt_self (a : α) {b : α} (h : 0 < b) : a - b < a :=
 calc
   a - b = a + -b : rfl
     ... < a + 0  : add_lt_add_left (neg_neg_of_pos h) _
@@ -1362,11 +1362,11 @@ by rw [min_neg_neg, neg_neg]
 
 def abs (a : α) : α := max a (-a)
 
-lemma abs_of_nonneg {a : α} (h : a ≥ 0) : abs a = a :=
+lemma abs_of_nonneg {a : α} (h : 0 ≤ a) : abs a = a :=
 have h' : -a ≤ a, from le_trans (neg_nonpos_of_nonneg h) h,
 max_eq_left h'
 
-lemma abs_of_pos {a : α} (h : a > 0) : abs a = a :=
+lemma abs_of_pos {a : α} (h : 0 < a) : abs a = a :=
 abs_of_nonneg (le_of_lt h)
 
 lemma abs_of_nonpos {a : α} (h : a ≤ 0) : abs a = -a :=
@@ -1382,10 +1382,10 @@ abs_of_nonneg (le_refl _)
 lemma abs_neg (a : α) : abs (-a) = abs a :=
 begin unfold abs, rw [max_comm, neg_neg] end
 
-lemma abs_pos_of_pos {a : α} (h : a > 0) : abs a > 0 :=
+lemma abs_pos_of_pos {a : α} (h : 0 < a) : 0 < abs a :=
 by rwa (abs_of_pos h)
 
-lemma abs_pos_of_neg {a : α} (h : a < 0) : abs a > 0 :=
+lemma abs_pos_of_neg {a : α} (h : a < 0) : 0 < abs a :=
 abs_neg a ▸ abs_pos_of_pos (neg_pos_of_neg h)
 
 lemma abs_sub (a b : α) : abs (a - b) = abs (b - a) :=
@@ -1399,15 +1399,15 @@ assume ha, h (eq.symm ha ▸ abs_zero)
 lemma eq_zero_of_neg_eq {a : α} (h : -a = a) : a = 0 :=
 match lt_trichotomy a 0 with
 | or.inl h₁ :=
-  have a > 0, from h ▸ neg_pos_of_neg h₁,
+  have 0 < a, from h ▸ neg_pos_of_neg h₁,
   absurd h₁ (lt_asymm this)
 | or.inr (or.inl h₁) := h₁
 | or.inr (or.inr h₁) :=
   have a < 0, from h ▸ neg_neg_of_pos h₁,
   absurd h₁ (lt_asymm this)
 end
 
-lemma abs_nonneg (a : α) : abs a ≥ 0 :=
+lemma abs_nonneg (a : α) : 0 ≤ abs a :=
 or.elim (le_total 0 a)
   (assume h : 0 ≤ a, by rwa (abs_of_nonneg h))
   (assume h : a ≤ 0, calc
@@ -1435,7 +1435,7 @@ lemma eq_of_abs_sub_eq_zero {a b : α} (h : abs (a - b) = 0) : a = b :=
 have a - b = 0, from eq_zero_of_abs_eq_zero h,
 show a = b, from eq_of_sub_eq_zero this
 
-lemma abs_pos_of_ne_zero {a : α} (h : a ≠ 0) : abs a > 0 :=
+lemma abs_pos_of_ne_zero {a : α} (h : a ≠ 0) : 0 < abs a :=
 or.elim (lt_or_gt_of_ne h) abs_pos_of_neg abs_pos_of_pos
 
 lemma abs_by_cases (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) : P (abs a) :=
@@ -1449,14 +1449,14 @@ abs_by_cases (λ x : α, x ≤ b) h1 h2
 lemma abs_lt_of_lt_of_neg_lt {a b : α} (h1 : a < b) (h2 : -a < b) : abs a < b :=
 abs_by_cases (λ x : α, x < b) h1 h2
 
-private lemma aux1 {a b : α} (h1 : a + b ≥ 0) (h2 : a ≥ 0) : abs (a + b) ≤ abs a + abs b :=
+private lemma aux1 {a b : α} (h1 : 0 ≤ a + b) (h2 : 0 ≤ a) : abs (a + b) ≤ abs a + abs b :=
 decidable.by_cases
-  (assume h3 : b ≥ 0, calc
+  (assume h3 : 0 ≤ b, calc
     abs (a + b) ≤ abs (a + b)   : by apply le_refl
             ... = a + b         : by rw (abs_of_nonneg h1)
             ... = abs a + b     : by rw (abs_of_nonneg h2)
             ... = abs a + abs b : by rw (abs_of_nonneg h3))
- (assume h3 : ¬ b ≥ 0,
+ (assume h3 : ¬ 0 ≤ b,
   have h4 : b ≤ 0, from le_of_lt (lt_of_not_ge h3),
   calc
     abs (a + b) = a + b         : by rw (abs_of_nonneg h1)
@@ -1465,7 +1465,7 @@ decidable.by_cases
             ... ≤ abs a + -b    : add_le_add_left (neg_nonneg_of_nonpos h4) _
             ... = abs a + abs b : by rw (abs_of_nonpos h4))
 
-private lemma aux2 {a b : α} (h1 : a + b ≥ 0) : abs (a + b) ≤ abs a + abs b :=
+private lemma aux2 {a b : α} (h1 : 0 ≤ a + b) : abs (a + b) ≤ abs a + abs b :=
 or.elim (le_total b 0)
  (assume h2 : b ≤ 0,
   have h3 : ¬ a < 0, from
@@ -1493,8 +1493,8 @@ or.elim (le_total 0 (a + b))
   (assume h2 : 0 ≤ a + b, aux2 h2)
   (assume h2 : a + b ≤ 0,
    have h3 : -a + -b = -(a + b), by rw neg_add,
-   have h4 : -(a + b) ≥ 0, from neg_nonneg_of_nonpos h2,
-   have h5   : -a + -b ≥ 0, begin rw [← h3] at h4, exact h4 end,
+   have h4 : 0 ≤ -(a + b), from neg_nonneg_of_nonpos h2,
+   have h5   : 0 ≤ -a + -b, begin rw [← h3] at h4, exact h4 end,
    calc
       abs (a + b) = abs (-a + -b)   : by rw [← abs_neg, neg_add]
               ... ≤ abs (-a) + abs (-b) : aux2 h5

src/analysis/normed_space/basic.lean

@@ -195,6 +195,7 @@ calc
   ... ≤ ∥g∥ + ∥h - g∥  : norm_add_le _ _
   ... < ∥g∥ + r : by { apply add_lt_add_left, rw ← dist_eq_norm, exact H }
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem normed_group.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
   tendsto f l (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in l, ∥ f x ∥ < ε :=
 metric.tendsto_nhds.trans $ by simp only [dist_zero_right]

src/data/complex/exponential.lean

@@ -208,6 +208,7 @@ begin
     (λ _ _, rfl),
 end
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma cauchy_product {a b : ℕ → β}
   (ha : is_cau_seq abs (λ m, (range m).sum (λ n, abv (a n))))
   (hb : is_cau_seq abv (λ m, (range m).sum b)) (ε : α) (ε0 : 0 < ε) :

src/data/real/pi.lean

@@ -19,11 +19,11 @@ lemma sqrt_two_add_series_zero : sqrt_two_add_series x 0 = x := by simp
 lemma sqrt_two_add_series_one : sqrt_two_add_series 0 1 = sqrt 2 := by simp
 lemma sqrt_two_add_series_two : sqrt_two_add_series 0 2 = sqrt (2 + sqrt 2) := by simp
 
-lemma sqrt_two_add_series_zero_nonneg : ∀(n : ℕ), sqrt_two_add_series 0 n ≥ 0
+lemma sqrt_two_add_series_zero_nonneg : ∀(n : ℕ), 0 ≤ sqrt_two_add_series 0 n
 | 0     := le_refl 0
 | (n+1) := sqrt_nonneg _
 
-lemma sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) : ∀(n : ℕ), sqrt_two_add_series x n ≥ 0
+lemma sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) : ∀(n : ℕ), 0 ≤ sqrt_two_add_series x n
 | 0     := h
 | (n+1) := sqrt_nonneg _
 
@@ -122,9 +122,9 @@ by { transitivity cos (pi / 2 ^ 5), congr, norm_num, simp }
 lemma sin_pi_div_thirty_two : sin (pi / 32) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2 :=
 by { transitivity sin (pi / 2 ^ 5), congr, norm_num, simp }
 
-lemma pi_gt_sqrt_two_add_series (n : ℕ) : pi > 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) :=
+lemma pi_gt_sqrt_two_add_series (n : ℕ) : 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) < pi :=
 begin
-  have : pi > sqrt (2 - sqrt_two_add_series 0 n) / 2 * 2 ^ (n+2),
+  have : sqrt (2 - sqrt_two_add_series 0 n) / 2 * 2 ^ (n+2) < pi,
   { apply mul_lt_of_lt_div, apply pow_pos, norm_num,
     rw [←sin_pi_over_two_pow_succ], apply sin_lt, apply div_pos pi_pos, apply pow_pos, norm_num },
   apply lt_of_le_of_lt (le_of_eq _) this,

src/group_theory/order_of_element.lean

@@ -79,6 +79,7 @@ have a ^ (i - j) = 1,
   by simp [sub_eq_add_neg, gpow_add, gpow_neg, a_eq],
 ⟨i - j, sub_ne_zero.mpr ne, this⟩
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma exists_pow_eq_one (a : α) : ∃i > 0, a ^ i = 1 :=
 let ⟨i, hi, eq⟩ := exists_gpow_eq_one a in
 begin
@@ -279,9 +280,12 @@ section cyclic
 
 local attribute [instance] set_fintype
 
+/-- A group is called *cyclic* if it is generated by a single element. -/
 class is_cyclic (α : Type*) [group α] : Prop :=
 (exists_generator [] : ∃ g : α, ∀ x, x ∈ gpowers g)
 
+/-- A cyclic group is always commutative. This is not an `instance` because often we have a better
+proof of `comm_group`. -/
 def is_cyclic.comm_group [hg : group α] [is_cyclic α] : comm_group α :=
 { mul_comm := λ x y, show x * y = y * x,
     from let ⟨g, hg⟩ := is_cyclic.exists_generator α in

src/measure_theory/integration.lean

@@ -692,7 +692,7 @@ lemma monotone_lintegral (α : Type*) [measure_space α] :
 
 lemma lintegral_eq_nnreal (f : α → ennreal) :
   (∫⁻ a, f a) =
-    (⨆ (s : α →ₛ nnreal) (hf : f ≥ s.map (coe : nnreal → ennreal)),
+    (⨆ (s : α →ₛ nnreal) (hf : ⇑(s.map (coe : nnreal → ennreal)) ≤ f),
       (s.map (coe : nnreal → ennreal)).integral) :=
 begin
   let c : nnreal → ennreal := coe,

src/number_theory/dioph.lean

@@ -751,17 +751,17 @@ localized "infix ` D/ `:80 := dioph.div_dioph" in dioph
 omit df dg
 open pell
 
-theorem pell_dioph : dioph (λv:vector3 ℕ 4, ∃ h : v &0 > 1,
+theorem pell_dioph : dioph (λv:vector3 ℕ 4, ∃ h : 1 < v &0,
   xn h (v &1) = v &2 ∧ yn h (v &1) = v &3) :=
 have dioph {v : vector3 ℕ 4 |
-v &0 > 1 ∧ v &1 ≤ v &3 ∧
+1 < v &0 ∧ v &1 ≤ v &3 ∧
 (v &2 = 1 ∧ v &3 = 0 ∨
 ∃ (u w s t b : ℕ),
   v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
   u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
   s * s - (b * b - 1) * t * t = 1 ∧
-  b > 1 ∧ (b ≡ 1 [MOD 4 * v &3]) ∧ (b ≡ v &0 [MOD u]) ∧
-  w > 0 ∧ v &3 * v &3 ∣ w ∧
+  1 < b ∧ (b ≡ 1 [MOD 4 * v &3]) ∧ (b ≡ v &0 [MOD u]) ∧
+  0 < w ∧ v &3 * v &3 ∣ w ∧
   (s ≡ v &2 [MOD u]) ∧
   (t ≡ v &1 [MOD 4 * v &3]))}, from
 D.1 D< D&0 D∧ D&1 D≤ D&3 D∧
@@ -776,18 +776,18 @@ D.1 D< D&0 D∧ D&1 D≤ D&3 D∧
   (D≡ (D&1) (D&6) (D.4 D* D&8)))),
 dioph.ext this $ λv, matiyasevic.symm
 
-theorem xn_dioph : dioph_pfun (λv:vector3 ℕ 2, ⟨v &0 > 1, λh, xn h (v &1)⟩) :=
-have dioph (λv:vector3 ℕ 3, ∃ y, ∃ h : v &1 > 1, xn h (v &2) = v &0 ∧ yn h (v &2) = y), from
+theorem xn_dioph : dioph_pfun (λv:vector3 ℕ 2, ⟨1 < v &0, λh, xn h (v &1)⟩) :=
+have dioph (λv:vector3 ℕ 3, ∃ y, ∃ h : 1 < v &1, xn h (v &2) = v &0 ∧ yn h (v &2) = y), from
 let D_pell := @reindex_dioph _ (fin2 4) _ pell_dioph [&2, &3, &1, &0] in D∃3 D_pell,
 (dioph_pfun_vec _).2 $ dioph.ext this $ λv, ⟨λ⟨y, h, xe, ye⟩, ⟨h, xe⟩, λ⟨h, xe⟩, ⟨_, h, xe, rfl⟩⟩
 
 include df dg
 theorem pow_dioph : dioph_fn (λv, f v ^ g v) :=
 have dioph {v : vector3 ℕ 3 |
-v &2 = 0 ∧ v &0 = 1 ∨ v &2 > 0 ∧
-(v &1 = 0 ∧ v &0 = 0 ∨ v &1 > 0 ∧
+v &2 = 0 ∧ v &0 = 1 ∨ 0 < v &2 ∧
+(v &1 = 0 ∧ v &0 = 0 ∨ 0 < v &1 ∧
 ∃ (w a t z x y : ℕ),
-  (∃ (a1 : a > 1), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
+  (∃ (a1 : 1 < a), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
   (x ≡ y * (a - v &1) + v &0 [MOD t]) ∧
   2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
   v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧