chore(Order): use new ge/gt naming convention - Part 1 (leanprover-community#24775)

This is the first PR in a sequence of PRs to apply the new naming convention for order lemmas.

This PR changes some lemmas that have multiple occurences of `lt` or `le` in their name, and where `<` and `≤` have their arguments swapped in some places. Then those occurrences of `<` and `≤` are referred to as `gt` and `ge`.

Names that will be changed by a follow up PR are `Ne.lt_or_lt`, `Ne.not_le_or_not_le`, `LT.lt.not_le` & friends, 

The first commit is an automatic replacement of lemma names. The second commit adds deprecations for the renamed lemmas. Later commits are manual fixes. This should make it easy to review.

Author: JovanGerb

Archive/Imo/Imo1959Q2.lean

@@ -37,7 +37,7 @@ variable {x A : ℝ}
 
 theorem isGood_iff : IsGood x A ↔
     sqrt (2 * x - 1) + 1 + |sqrt (2 * x - 1) - 1| = A * sqrt 2 ∧ 1 / 2 ≤ x := by
-  cases le_or_lt (1 / 2) x with
+  cases le_or_gt (1 / 2) x with
   | inl hx =>
     have hx' : 0 ≤ 2 * x - 1 := by linarith
     have h₁ : x + sqrt (2 * x - 1) = (sqrt (2 * x - 1) + 1) ^ 2 / 2 := by
@@ -85,7 +85,7 @@ theorem IsGood.sqrt_two_lt_iff_one_lt (h : IsGood x A) : sqrt 2 < A ↔ 1 < x :=
   ⟨fun hA ↦ not_le.1 fun hx ↦ hA.ne' <| h.eq_sqrt_two_iff_le_one.2 hx, h.sqrt_two_lt_of_one_lt⟩
 
 theorem IsGood.sqrt_two_le (h : IsGood x A) : sqrt 2 ≤ A :=
-  (le_or_lt x 1).elim (fun hx ↦ (h.eq_sqrt_two_iff_le_one.2 hx).ge) fun hx ↦
+  (le_or_gt x 1).elim (fun hx ↦ (h.eq_sqrt_two_iff_le_one.2 hx).ge) fun hx ↦
     (h.sqrt_two_lt_of_one_lt hx).le
 
 theorem isGood_iff_of_sqrt_two_lt (hA : sqrt 2 < A) : IsGood x A ↔ x = (A / 2) ^ 2 + 1 / 2 := by

Archive/Imo/Imo1960Q2.lean

@@ -42,7 +42,7 @@ theorem isGood_iff {x} : IsGood x ↔ x ∈ Ico (-1/2) (45/8) \ {0} := by
   -- First, note that the denominator is equal to zero at `x = 0`, hence it's not a solution.
   rcases eq_or_ne x 0 with rfl | hx
   · simp [isGood_iff']
-  cases lt_or_le x (-1/2) with
+  cases lt_or_ge x (-1/2) with
   | inl hx2 =>
     -- Next, if `x < -1/2`, then the square root is undefined.
     have : 2 * x + 1 < 0 := by linarith

Archive/Imo/Imo1986Q5.lean

@@ -61,7 +61,7 @@ theorem map_of_lt_two (hx : x < 2) : f x = 2 / (2 - x) := by
     rw [hf.map_add_rev, hf.map_eq_zero, tsub_add_cancel_of_le hx.le]
 
 theorem map_eq (x : ℝ≥0) : f x = 2 / (2 - x) :=
-  match lt_or_le x 2 with
+  match lt_or_ge x 2 with
   | .inl hx => hf.map_of_lt_two hx
   | .inr hx => by rwa [tsub_eq_zero_of_le hx, div_zero, hf.map_eq_zero]
 
@@ -75,7 +75,7 @@ theorem isGood_iff {f : ℝ≥0 → ℝ≥0} : IsGood f ↔ f = fun x ↦ 2 / (2
   case map_ne_zero => intro x hx; simpa [tsub_eq_zero_iff_le]
   case map_add_rev =>
     intro x y
-    cases lt_or_le y 2 with
+    cases lt_or_ge y 2 with
     | inl hy =>
       have hy' : 2 - y ≠ 0 := (tsub_pos_of_lt hy).ne'
       rw [div_mul_div_comm, tsub_mul, mul_assoc, div_mul_cancel₀ _ hy', mul_comm x,

Archive/Imo/Imo1988Q6.lean

@@ -68,7 +68,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   -- First of all, we may assume that x ≤ y.
   -- We justify this using H_symm.
   wlog hxy : x ≤ y
-  · rw [H_symm] at h₀; apply this y x h₀ B C base _ _ _ _ _ _ (le_of_not_le hxy); assumption'
+  · rw [H_symm] at h₀; apply this y x h₀ B C base _ _ _ _ _ _ (le_of_not_ge hxy); assumption'
   -- In fact, we can easily deal with the case x = y.
   by_cases x_eq_y : x = y
   · subst x_eq_y; exact H_diag h₀

Archive/Imo/Imo2015Q6.lean

@@ -127,7 +127,7 @@ include ha hbN
 lemma b_pos : 0 < b := by
   by_contra! h; rw [nonpos_iff_eq_zero] at h; subst h
   replace hbN : ∀ t, #(pool a t) = 0 := fun t ↦ by
-    obtain h | h := le_or_lt t N
+    obtain h | h := le_or_gt t N
     · have : #(pool a t) ≤ #(pool a N) := monotone_card_pool ha h
       rwa [hbN _ le_rfl, nonpos_iff_eq_zero] at this
     · exact hbN _ h.le

Archive/Imo/Imo2024Q6.lean

@@ -203,7 +203,7 @@ lemma apply_fExample_add_apply_of_fract_le {x y : ℚ} (h : Int.fract y ≤ Int.
 
 lemma aquaesulian_fExample : Aquaesulian fExample := by
   intro x y
-  rcases lt_or_le (Int.fract x) (Int.fract y) with h | h
+  rcases lt_or_ge (Int.fract x) (Int.fract y) with h | h
   · rw [add_comm (fExample x), add_comm x]
     exact .inr (apply_fExample_add_apply_of_fract_le h.le)
   · exact .inl (apply_fExample_add_apply_of_fract_le h)

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -122,7 +122,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
         rintro x ⟨rfl | _⟩ y ⟨rfl | _⟩ _
         · apply (irrefl _ ‹j < j›).elim
         · exfalso
-          apply not_le_of_lt (_root_.trans ‹i < j› ‹j < y›) (le_max_of_eq ‹y ∈ t› ‹t.max = i›)
+          apply not_le_of_gt (_root_.trans ‹i < j› ‹j < y›) (le_max_of_eq ‹y ∈ t› ‹t.max = i›)
         · first
           | apply lt_of_le_of_lt _ ‹f i < f j›
           | apply lt_of_lt_of_le ‹f j < f i› _
@@ -133,7 +133,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
       -- Finally show that this new subsequence is one longer than the old one.
       · rw [card_insert_of_notMem, ht₂]
         intro
-        apply not_le_of_lt ‹i < j› (le_max_of_eq ‹j ∈ t› ‹t.max = i›)
+        apply not_le_of_gt ‹i < j› (le_max_of_eq ‹j ∈ t› ‹t.max = i›)
   -- Finished both goals!
   -- Now that we have uniqueness of each label, it remains to do some counting to finish off.
   -- Suppose all the labels are small.
@@ -158,7 +158,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
     -- Need to get `a_i ≤ r`, here phrased as: there is some `a < r` with `a+1 = a_i`.
     exact ⟨⟨(ab i).1 - 1, by omega⟩, (ab i).2 - 1, by omega⟩
   -- To get our contradiction, it suffices to prove `n ≤ r * s`
-  apply not_le_of_lt hn
+  apply not_le_of_gt hn
   -- Which follows from considering the cardinalities of the subset above, since `ab` is injective.
   simpa [ran, Nat.succ_injective, card_image_of_injective, ‹Injective ab›] using card_le_card this
 

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -38,7 +38,7 @@ theorem Ico_lemma {α} [LinearOrder α] {x₁ x₂ y₁ y₂ z₁ z₂ w : α} (
   simp only [not_and, not_lt, mem_Ico] at hw
   refine ⟨max x₁ (min w y₂), ?_, ?_, ?_⟩
   · simp [le_refl, lt_trans h₁ (lt_trans hy h₂), h₂]
-  · simp +contextual [hw, lt_irrefl, not_le_of_lt h₁]
+  · simp +contextual [hw, lt_irrefl, not_le_of_gt h₁]
   · simp [hw.2.1, hw.2.2, hz₁, lt_of_lt_of_le h₁ hz₂]
 
 /-- A (hyper)-cube (in standard orientation) is a vector `b` consisting of the bottom-left point
@@ -190,7 +190,7 @@ theorem shiftUp_bottom_subset_bottoms (hc : (cs i).xm ≠ 1) :
     intro j; exact side_subset h (hps j)
   rw [← h.2, mem_iUnion] at this; rcases this with ⟨i', hi'⟩
   rw [mem_iUnion]; use i'; refine ⟨?_, fun j => hi' j.succ⟩
-  have : i ≠ i' := by rintro rfl; apply not_le_of_lt (hi' 0).2; rw [hp0]; rfl
+  have : i ≠ i' := by rintro rfl; apply not_le_of_gt (hi' 0).2; rw [hp0]; rfl
   have := h.1 this
   rw [onFun, comp_apply, comp_apply, toSet_disjoint, exists_fin_succ] at this
   rcases this with (h0 | ⟨j, hj⟩)
@@ -290,7 +290,7 @@ theorem nontrivial_bcubes : (bcubes cs c).Nontrivial := by
   have h2i' : i' ∈ bcubes cs c := ⟨hi'.1.symm, v.2.1 i' hi'.1.symm ⟨tail p, hi'.2, hp.2⟩⟩
   refine ⟨i, h2i, i', h2i', ?_⟩
   rintro rfl
-  apply not_le_of_lt (hi'.2 ⟨1, Nat.le_of_succ_le_succ h.three_le⟩).2
+  apply not_le_of_gt (hi'.2 ⟨1, Nat.le_of_succ_le_succ h.three_le⟩).2
   simp only [tail, Cube.tail, p]
   rw [if_pos, add_le_add_iff_right]
   · exact (hi.2 _).1

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -334,7 +334,7 @@ include hG in
 theorem friendship_theorem [Nonempty V] : ExistsPolitician G := by
   by_contra npG
   rcases hG.isRegularOf_not_existsPolitician npG with ⟨d, dreg⟩
-  rcases lt_or_le d 3 with dle2 | dge3
+  rcases lt_or_ge d 3 with dle2 | dge3
   · exact npG (hG.existsPolitician_of_degree_le_two dreg (Nat.lt_succ_iff.mp dle2))
   · exact hG.false_of_three_le_degree dreg dge3
 

Counterexamples/AharoniKorman.lean

@@ -490,16 +490,16 @@ lemma not_apply_lt : ¬ f x < x := f.not_lt_of_eq (by simp)
 lemma not_lt_apply : ¬ x < f x := f.not_lt_of_eq (by simp)
 
 lemma le_apply_of_le (hC : IsChain (· ≤ ·) C) (hy : y ∈ C) (hx : y ≤ x) : y ≤ f x :=
-  hC.le_of_not_lt (f.mem x) hy fun hxy ↦ f.not_apply_lt (hxy.trans_le hx)
+  hC.le_of_not_gt (f.mem x) hy fun hxy ↦ f.not_apply_lt (hxy.trans_le hx)
 
 lemma apply_le_of_le (hC : IsChain (· ≤ ·) C) (hy : y ∈ C) (hx : x ≤ y) : f x ≤ y :=
-  hC.le_of_not_lt hy (f.mem x) fun hxy ↦ f.not_lt_apply (hx.trans_lt hxy)
+  hC.le_of_not_gt hy (f.mem x) fun hxy ↦ f.not_lt_apply (hx.trans_lt hxy)
 
 lemma lt_apply_of_lt (hC : IsChain (· ≤ ·) C) (hy : y ∈ C) (hx : y < x) : y < f x :=
-  hC.lt_of_not_le (f.mem x) hy fun hxy ↦ f.not_apply_lt (hxy.trans_lt hx)
+  hC.lt_of_not_ge (f.mem x) hy fun hxy ↦ f.not_apply_lt (hxy.trans_lt hx)
 
 lemma apply_lt_of_lt (hC : IsChain (· ≤ ·) C) (hy : y ∈ C) (hx : x < y) : f x < y :=
-  hC.lt_of_not_le hy (f.mem x) fun hxy ↦ f.not_lt_apply (hx.trans_le hxy)
+  hC.lt_of_not_ge hy (f.mem x) fun hxy ↦ f.not_lt_apply (hx.trans_le hxy)
 
 lemma apply_mem_Icc_of_mem_Icc (hC : IsChain (· ≤ ·) C) (hy : y ∈ C) (hz : z ∈ C)
     (hx : x ∈ Set.Icc y z) : f x ∈ Set.Icc y z :=
@@ -788,7 +788,7 @@ theorem apply_eq_of_line_eq (f : SpinalMap C) {n : ℕ} (hC : IsChain (· ≤ ·
     (h₁l : lo ≤ x) (h₂l : lo ≤ y) (h₁h : x ≤ hi) (h₂h : y ≤ hi) :
     f x = f y := by
   wlog hxy : (ofHollom y).1 ≤ (ofHollom x).1 generalizing x y
-  · exact (this h.symm h₂l h₁l h₂h h₁h (le_of_not_le hxy)).symm
+  · exact (this h.symm h₂l h₁l h₂h h₁h (le_of_not_ge hxy)).symm
   have hx : x ∈ level n := ordConnected_level.out hlo.2 hhi.2 ⟨h₁l, h₁h⟩
   have hy : y ∈ level n := ordConnected_level.out hlo.2 hhi.2 ⟨h₂l, h₂h⟩
   induction hx using induction_on_level with | h x₁ y₁ =>
@@ -896,7 +896,7 @@ lemma x0y0_mem (h : (C ∩ level (n + 1)).Nonempty) :
 lemma x0y0_min (z : ℕ × ℕ) (hC : IsChain (· ≤ ·) C) (h : embed (n + 1) z ∈ C) :
     embed (n + 1) (x0y0 n C) ≤ embed (n + 1) z := by
   have : (C ∩ level (n + 1)).Nonempty := ⟨_, h, by simp [level_eq_range]⟩
-  refine hC.le_of_not_lt h (x0y0_mem this) ?_
+  refine hC.le_of_not_gt h (x0y0_mem this) ?_
   rw [x0y0, dif_pos this, OrderEmbedding.lt_iff_lt]
   exact wellFounded_lt.not_lt_min {x | embed (n + 1) x ∈ C} ?_ h
 
@@ -1061,7 +1061,7 @@ theorem not_S_hits_next (f : SpinalMap C) (hC : IsChain (· ≤ ·) C)
       -- Then we have `(a, b, n + 1) ≤ j`...
       have hj' : h(a, b, n + 1) ≤ j := by
         induction hjCn.2 using induction_on_level with | h c d =>
-        apply hC.le_of_not_lt hjCn.1 hp.1 ?_
+        apply hC.le_of_not_gt hjCn.1 hp.1 ?_
         intro h
         have : c + d < a + b := add_lt_add_of_lt h
         simp only [toHollom_le_toHollom_iff_fixed_right] at hj
@@ -1082,7 +1082,7 @@ theorem not_S_hits_next (f : SpinalMap C) (hC : IsChain (· ≤ ·) C)
       -- The left case is exactly symmetric
       have hj' : h(a, b, n + 1) ≤ j := by
         induction hjCn.2 using induction_on_level with | h c d =>
-        apply hC.le_of_not_lt hjCn.1 hp.1 ?_
+        apply hC.le_of_not_gt hjCn.1 hp.1 ?_
         intro h
         have : c + d < a + b := add_lt_add_of_lt h
         simp only [toHollom_le_toHollom_iff_fixed_right] at hj