feat(Order/Monotone/Defs): weaken hypothesis of injective_of_le_imp_le (leanprover-community#33111)

`injective_of_le_imp_le` requires `∀ x y, f x ≤ f y → x ≤ y`, but `∀ x y, f x = f y → x ≤ y` is sufficient.

Also rename the weakened`injective_of_le_imp_le` to `Function.Injective.of_eq_imp_le` and `injective_of_lt_imp_ne` to `Function.Injective.of_lt_imp_ne` to allow for dot notation.

Author: SnirBroshi

Archive/Imo/Imo1994Q1.lean

@@ -69,10 +69,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : #A = m + 1)
   by_contra! h : a k + a (rev k) < n + 1
   -- We exhibit `k+1` elements of `A` greater than `a (rev k)`
   set f : Fin (m + 1) ↪ ℕ :=
-    ⟨fun i => a i + a (rev k), by
-      apply injective_of_le_imp_le
-      intro i j hij
-      rwa [add_le_add_iff_right, a.map_rel_iff] at hij ⟩
+    ⟨fun i => a i + a (rev k), .of_eq_imp_le (a.map_rel_iff.mp <| add_right_cancel · |>.le)⟩
   -- Proof that the `f i` are greater than `a (rev k)` for `i ≤ k`
   have hf : map f (Icc 0 k) ⊆ map a.toEmbedding (Ioc (rev k) (Fin.last m)) := by
     intro x hx

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -120,7 +120,7 @@ By combining the previous two lemmas, we see that since `f` is injective, the pa
 must also be unique.
 -/
 private lemma paired_injective (hf : Injective f) : Injective (paired f) := by
-  apply injective_of_lt_imp_ne
+  apply Injective.of_lt_imp_ne
   intro i j hij q
   cases lt_or_gt_of_ne (hf.ne hij.ne)
   case inl h => exact (maxIncSequencesTo_lt hij h).ne congr($q.1)

Mathlib/Algebra/Prime/Lemmas.lean

@@ -163,7 +163,7 @@ theorem DvdNotUnit.ne [CancelCommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q
 
 theorem pow_injective_of_not_isUnit [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q)
     (hq' : q ≠ 0) : Function.Injective fun n : ℕ => q ^ n := by
-  refine injective_of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩
+  refine .of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩
   · exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')
   · exact (pow_mul_pow_sub q h.le).symm
 

Mathlib/Analysis/Convex/Basic.lean

@@ -509,7 +509,7 @@ theorem Convex.semilinear_image {s : Set E} (hs : Convex 𝕜 s) (hσ : ∀ {s t
   obtain ⟨t, rfl⟩ : ∃ t : 𝕜, σ t = b := RingHomSurjective.is_surjective ..
   refine ⟨r • x + t • y, hs hx hy (by simp_all [(@hσ 0 r).mp]) (by simp_all [(@hσ 0 t).mp])
     ?_, by simp⟩
-  apply_fun σ using injective_of_le_imp_le _ hσ.mp
+  apply_fun σ using Function.Injective.of_eq_imp_le (hσ.mp ·.le)
   simpa
 
 end SemilinearMap

Mathlib/Data/Finset/Powerset.lean

@@ -59,7 +59,7 @@ theorem powerset_mono {s t : Finset α} : powerset s ⊆ powerset t ↔ s ⊆ t
     mem_powerset.2 <| Subset.trans (mem_powerset.1 h) st⟩
 
 theorem powerset_injective : Injective (powerset : Finset α → Finset (Finset α)) :=
-  (injective_of_le_imp_le _) powerset_mono.1
+  .of_eq_imp_le (powerset_mono.1 ·.le)
 
 @[simp]
 theorem powerset_inj : powerset s = powerset t ↔ s = t :=

Mathlib/Order/Monotone/Defs.lean

@@ -318,17 +318,21 @@ theorem strictAnti_of_le_iff_le [Preorder α] [Preorder β] {f : α → β}
     (h : ∀ x y, x ≤ y ↔ f y ≤ f x) : StrictAnti f :=
   fun _ _ ↦ (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1
 
-theorem injective_of_lt_imp_ne [LinearOrder α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) :
+theorem Function.Injective.of_lt_imp_ne [LinearOrder α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) :
     Injective f := by
-  intro x y hf
-  rcases lt_trichotomy x y with (hxy | rfl | hxy)
-  · exact absurd hf <| h _ _ hxy
-  · rfl
-  · exact absurd hf.symm <| h _ _ hxy
+  grind [Injective]
 
+@[deprecated (since := "2025-12-23")]
+alias injective_of_lt_imp_ne := Function.Injective.of_lt_imp_ne
+
+theorem Function.Injective.of_eq_imp_le [PartialOrder α] {f : α → β}
+    (h : ∀ {x y}, f x = f y → x ≤ y) : f.Injective :=
+  fun _ _ hxy ↦ h hxy |>.antisymm <| h hxy.symm
+
+@[deprecated Injective.of_eq_imp_le (since := "2025-12-23")]
 theorem injective_of_le_imp_le [PartialOrder α] [Preorder β] (f : α → β)
     (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f :=
-  fun _ _ hxy ↦ (h hxy.le).antisymm (h hxy.ge)
+  .of_eq_imp_le (h ·.le)
 
 /-! ### Monotonicity under composition -/
 

Mathlib/RingTheory/Localization/Submodule.lean

@@ -113,7 +113,7 @@ variable (S)
 
 theorem coeSubmodule_injective (h : M ≤ nonZeroDivisors R) :
     Function.Injective (coeSubmodule S : Ideal R → Submodule R S) :=
-  injective_of_le_imp_le _ fun hl => (coeSubmodule_le_coeSubmodule h).mp hl
+  .of_eq_imp_le fun hl => (coeSubmodule_le_coeSubmodule h).mp hl.le
 
 theorem coeSubmodule_isPrincipal {I : Ideal R} (h : M ≤ nonZeroDivisors R) :
     (coeSubmodule S I).IsPrincipal ↔ I.IsPrincipal := by
@@ -191,7 +191,7 @@ theorem coeSubmodule_strictMono : StrictMono (coeSubmodule K : Ideal R → Submo
 variable (R K)
 
 theorem coeSubmodule_injective : Function.Injective (coeSubmodule K : Ideal R → Submodule R K) :=
-  injective_of_le_imp_le _ fun hl => coeSubmodule_le_coeSubmodule.mp hl
+  .of_eq_imp_le fun hl => coeSubmodule_le_coeSubmodule.mp hl.le
 
 @[simp]
 theorem coeSubmodule_isPrincipal {I : Ideal R} : (coeSubmodule K I).IsPrincipal ↔ I.IsPrincipal :=

Mathlib/Topology/ClopenBox.lean

@@ -86,7 +86,7 @@ lemma countable_iff_secondCountable [T2Space X]
     [TotallyDisconnectedSpace X] : Countable (Clopens X) ↔ SecondCountableTopology X := by
   refine ⟨fun h ↦ ⟨{s : Set X | IsClopen s}, ?_, ?_⟩, fun h ↦ ?_⟩
   · let f : {s : Set X | IsClopen s} → Clopens X := fun s ↦ ⟨s.1, s.2⟩
-    exact (injective_of_le_imp_le f fun a ↦ a).countable
+    exact Injective.of_eq_imp_le (f := f) (·.le) |>.countable
   · apply IsTopologicalBasis.eq_generateFrom
     exact loc_compact_Haus_tot_disc_of_zero_dim
   · have : ∀ (s : Clopens X), ∃ (t : Finset (countableBasis X)), s.1 = (SetLike.coe t).sUnion :=