style(Archive): avoid using > or ≥ (#35346)

Prefer to use < or ≤ instead.
For consistently with mathlib style; extracted from #12933.

Author: grunweg

Archive/Imo/Imo1960Q1.lean

@@ -71,7 +71,7 @@ theorem searchUpTo_step {c n} (H : SearchUpTo c n) {c' n'} (ec : c + 1 = c') (en
   obtain ⟨h₁, ⟨m, rfl⟩, h₂⟩ := id p
   by_cases h : 11 * m < c * 11; · exact H _ h p
   obtain rfl : m = c := by lia
-  rw [Nat.mul_div_cancel_left _ (by simp : 11 > 0), mul_comm] at h₂
+  rw [Nat.mul_div_cancel_left _ (by decide), mul_comm] at h₂
   refine (H' h₂).imp ?_ ?_ <;> · rintro rfl; norm_num
 
 theorem searchUpTo_end {c} (H : SearchUpTo c 1001) {n : ℕ} (ppn : ProblemPredicate n) :

Archive/Imo/Imo1988Q6.lean

@@ -226,16 +226,16 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
   · -- Show the descent step.
     intro x y hx x_lt_y _ _ z h_root _ hV₀
     constructor
-    · have hpos : z * z + x * x > 0 := by
+    · have hpos : 0 < z * z + x * x := by
         apply add_pos_of_nonneg_of_pos
         · apply mul_self_nonneg
         · apply mul_pos <;> exact mod_cast hx
       have hzx : z * z + x * x = (z * x + 1) * k := by
         rw [← sub_eq_zero, ← h_root]
         ring
       rw [hzx] at hpos
-      replace hpos : z * x + 1 > 0 := pos_of_mul_pos_left hpos (Int.natCast_nonneg k)
-      replace hpos : z * x ≥ 0 := Int.le_of_lt_add_one hpos
+      replace hpos : 0 < z * x + 1 := pos_of_mul_pos_left hpos (Int.natCast_nonneg k)
+      replace hpos : 0 ≤ z * x := Int.le_of_lt_add_one hpos
       apply nonneg_of_mul_nonneg_left hpos (mod_cast hx)
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt

Archive/Imo/Imo2005Q3.lean

@@ -24,7 +24,7 @@ and then making use of `xyz ≥ 1` to show `(x^5-x^2)/(x^3*(x^2+y^2+z^2)) ≥ (x
 
 namespace Imo2005Q3
 
-theorem key_insight (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x * y * z ≥ 1) :
+theorem key_insight (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (h : x * y * z ≥ 1) :
     (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) ≥ (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2) := by
   have key :
     (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) -
@@ -44,7 +44,7 @@ end Imo2005Q3
 
 open Imo2005Q3
 
-theorem imo2005_q3 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x * y * z ≥ 1) :
+theorem imo2005_q3 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (h : x * y * z ≥ 1) :
     (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) + (y ^ 5 - y ^ 2) / (y ^ 5 + z ^ 2 + x ^ 2) +
         (z ^ 5 - z ^ 2) / (z ^ 5 + x ^ 2 + y ^ 2) ≥
       0 := by

Archive/Imo/Imo2008Q2.lean

@@ -67,7 +67,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
     simp only [Set.mem_setOf_eq] at hs_in_W ⊢
     rcases hs_in_W with ⟨x, y, z, h₁, t, ht_gt_zero, hx_t, hy_t, hz_t⟩
     use x, y, z
-    have key_gt_zero : t ^ 2 + t + 1 > 0 := by linarith [pow_pos ht_gt_zero 2, ht_gt_zero]
+    have key_gt_zero : 0 < t ^ 2 + t + 1 := by linarith [pow_pos ht_gt_zero 2, ht_gt_zero]
     have h₂ : x ≠ 1 := by rw [hx_t]; simp [field]; linarith [key_gt_zero]
     have h₃ : y ≠ 1 := by rw [hy_t]; simp [field]; linarith [key_gt_zero]
     have h₄ : z ≠ 1 := by rw [hz_t]; linarith [key_gt_zero]

Archive/Imo/Imo2008Q3.lean

@@ -45,7 +45,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
     simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
     rw [pow_two, ← hy]; exact neg_add_cancel 1
   have hnat₂ : n ≤ p / 2 := ZMod.natAbs_valMinAbs_le y
-  have hnat₃ : p ≥ 2 * n := by lia
+  have hnat₃ : 2 * n ≤ p := by lia
   set k : ℕ := p - 2 * n with hnat₄
   have hnat₅ : p ∣ k ^ 2 + 4 := by
     obtain ⟨x, hx⟩ := hnat₁
@@ -55,11 +55,11 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
       have hcast₂ : (n : ℤ) ^ 2 + 1 = p * x := by assumption_mod_cast
       linear_combination ((k : ℤ) + p - 2 * n) * hcast₁ + 4 * hcast₂
     assumption_mod_cast
-  have hnat₆ : k ^ 2 + 4 ≥ p := Nat.le_of_dvd (k ^ 2 + 3).succ_pos hnat₅
+  have hnat₆ : p ≤ k ^ 2 + 4 := Nat.le_of_dvd (k ^ 2 + 3).succ_pos hnat₅
   have hreal₁ : (k : ℝ) = p - 2 * n := by assumption_mod_cast
-  have hreal₂ : (p : ℝ) > 20 := by assumption_mod_cast
-  have hreal₃ : (k : ℝ) ^ 2 + 4 ≥ p := by assumption_mod_cast
-  have hreal₅ : (k : ℝ) > 4 := by
+  have hreal₂ : 20 < (p : ℝ) := by assumption_mod_cast
+  have hreal₃ : p ≤ (k : ℝ) ^ 2 + 4 := by assumption_mod_cast
+  have hreal₅ : 4 < (k : ℝ) := by
     refine lt_of_pow_lt_pow_left₀ 2 k.cast_nonneg ?_
     linarith only [hreal₂, hreal₃]
   have hreal₆ : (k : ℝ) > sqrt (2 * n) := by

Archive/Imo/Imo2008Q4.lean

@@ -34,7 +34,7 @@ end Imo2008Q4
 open Imo2008Q4
 
 set_option linter.flexible false in
-theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
+theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, 0 < f x) :
     (∀ w x y z : ℝ, 0 < w → 0 < x → 0 < y → 0 < z → w * x = y * z →
       (f w ^ 2 + f x ^ 2) / (f (y ^ 2) + f (z ^ 2)) = (w ^ 2 + x ^ 2) / (y ^ 2 + z ^ 2)) ↔
     (∀ x > 0, f x = x) ∨ ∀ x > 0, f x = 1 / x := by
@@ -64,10 +64,10 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
   -- f(a) ≠ 1/a, f(a) = a
   obtain hfb₂ := Or.resolve_left (h₃ b hb) hfb₁
   -- f(b) ≠ b, f(b) = 1/b
-  have hab : a * b > 0 := mul_pos ha hb
-  have habss : a * b = sqrt (a * b) * sqrt (a * b) := (mul_self_sqrt (le_of_lt hab)).symm
+  have hab : 0 < a * b := by positivity
+  have habss : a * b = sqrt (a * b) * sqrt (a * b) := (mul_self_sqrt hab.le).symm
   specialize H₂ a b (sqrt (a * b)) (sqrt (a * b)) ha hb (sqrt_pos.mpr hab) (sqrt_pos.mpr hab) habss
-  rw [sq_sqrt (le_of_lt hab), ← two_mul (f (a * b)), ← two_mul (a * b)] at H₂
+  rw [sq_sqrt hab.le, ← two_mul (f (a * b)), ← two_mul (a * b)] at H₂
   rw [hfa₂, hfb₂] at H₂
   have h2ab_ne_0 : 2 * (a * b) ≠ 0 := by positivity
   specialize h₃ (a * b) hab

Archive/Imo/Imo2019Q4.lean

@@ -80,7 +80,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0)
 end Imo2019Q4
 
 set_option linter.flexible false in
-theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
+theorem imo2019_q4 {k n : ℕ} (hk : 0 < k) (hn : 0 < n) :
     (k ! : ℤ) = ∏ i ∈ range n, ((2 : ℤ) ^ n - (2 : ℤ) ^ i) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2) := by
   -- The implication `←` holds.
   constructor

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -105,7 +105,7 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by
             ((hasDerivAt_const x (r : ℝ)⁻¹).mul (hasDerivAt_id' x)))).add
         ((hasDerivAt_id' x).mul ((((hasDerivAt_id' x).fun_pow 2).const_sub ((r : ℝ) ^ 2)).sqrt _))
       using 1
-    · have h₁ : (r : ℝ) ^ 2 - x ^ 2 > 0 := sub_pos_of_lt (sq_lt_sq' hx1 hx2)
+    · have h₁ : 0 < (r : ℝ) ^ 2 - x ^ 2 := sub_pos_of_lt (sq_lt_sq' hx1 hx2)
       have h : sqrt ((r : ℝ) ^ 2 - x ^ 2) ^ 3 =
           ((r : ℝ) ^ 2 - x ^ 2) * sqrt ((r : ℝ) ^ 2 - x ^ 2) := by
         rw [pow_three, ← mul_assoc, mul_self_sqrt (by positivity)]

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -321,7 +321,7 @@ theorem ballot_problem' :
       (countedSequence_finite p (q + 1)) (countedSequence_nonempty _ _)
     haveI := isProbabilityMeasure_uniformOn
       (countedSequence_finite (p + 1) q) (countedSequence_nonempty _ _)
-    have h₃ : p + 1 + (q + 1) > 0 := Nat.add_pos_left (Nat.succ_pos _) _
+    have h₃ : 0 < p + 1 + (q + 1) := Nat.add_pos_left (Nat.succ_pos _) _
     rw [← uniformOn_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _),
       first_vote_pos _ _ h₃, first_vote_neg _ _ h₃, ballot_pos, ballot_neg _ _ qp]
     rw [ENNReal.toReal_add, ENNReal.toReal_mul, ENNReal.toReal_mul, ← Nat.cast_add,