suffix theorems with _of_wellFounded{LT/GT} and add deprecations

Author: SnirBroshi

Mathlib/Data/Finset/Sort.lean

@@ -263,8 +263,8 @@ theorem orderEmbOfFin_singleton (a : α) (i : Fin 1) :
 the increasing bijection `orderEmbOfFin s h`. -/
 theorem orderEmbOfFin_unique {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin k → α}
     (hfs : ∀ x, f x ∈ s) (hmono : StrictMono f) : f = s.orderEmbOfFin h := by
-  rw [← hmono.range_inj (s.orderEmbOfFin h).strictMono, range_orderEmbOfFin, ← Set.image_univ,
-    ← coe_univ, ← coe_image, coe_inj]
+  rw [← hmono.range_inj_of_wellFoundedLT (s.orderEmbOfFin h).strictMono, range_orderEmbOfFin,
+    ← Set.image_univ, ← coe_univ, ← coe_image, coe_inj]
   refine eq_of_subset_of_card_le (fun x hx => ?_) ?_
   · rcases mem_image.1 hx with ⟨x, _, rfl⟩
     exact hfs x

Mathlib/Order/Hom/Set.lean

@@ -155,9 +155,13 @@ theorem orderIsoOfSurjective_self_symm_apply (b : β) :
 end StrictMono
 
 /-- Two order embeddings on a well-order are equal provided that their ranges are equal. -/
-lemma OrderEmbedding.range_inj [LinearOrder α] [WellFoundedLT α] [Preorder β] {f g : α ↪o β} :
-    Set.range f = Set.range g ↔ f = g := by
-  rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]
+@[to_dual]
+lemma OrderEmbedding.range_inj_of_wellFoundedLT [LinearOrder α] [WellFoundedLT α] [Preorder β]
+    {f g : α ↪o β} : Set.range f = Set.range g ↔ f = g := by
+  rw [f.strictMono.range_inj_of_wellFoundedLT g.strictMono, DFunLike.coe_fn_eq]
+
+@[deprecated (since := "2026-05-15")]
+alias OrderEmbedding.range_inj := OrderEmbedding.range_inj_of_wellFoundedLT
 
 namespace OrderIso
 
@@ -168,7 +172,8 @@ instance subsingleton_of_wellFoundedLT [LinearOrder α] [WellFoundedLT α] [Preo
     Subsingleton (α ≃o β) := by
   refine ⟨fun f g ↦ ?_⟩
   rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
-    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
+    ← OrderEmbedding.range_inj_of_wellFoundedLT, coe_toOrderEmbedding, coe_toOrderEmbedding,
+    range_eq, range_eq]
 
 instance subsingleton_of_wellFoundedLT' [LinearOrder β] [WellFoundedLT β] [Preorder α] :
     Subsingleton (α ≃o β) := by

Mathlib/Order/WellFounded.lean

@@ -189,8 +189,8 @@ theorem WellFounded.min_le (h : WellFounded ((· < ·) : β → β → Prop))
     {x : β} {s : Set β} (hx : x ∈ s) : h.min s ⟨x, hx⟩ ≤ x :=
   not_lt.1 <| h.not_lt_min _ hx
 
-@[to_dual range_injOn_strictMono_of_wellFoundedGT]
-theorem Set.range_injOn_strictMono [WellFoundedLT β] :
+@[to_dual]
+theorem Set.range_injOn_strictMono_of_wellFoundedLT [WellFoundedLT β] :
     Set.InjOn Set.range { f : β → γ | StrictMono f } := by
   intro f hf g hg hfg
   ext a
@@ -207,20 +207,32 @@ theorem Set.range_injOn_strictMono [WellFoundedLT β] :
     rw [IH c this] at hc
     cases (hg.injective hc).not_lt this
 
-@[to_dual range_injOn_strictAnti_of_wellFoundedLT]
-theorem Set.range_injOn_strictAnti [WellFoundedGT β] :
+@[deprecated (since := "2026-05-15")]
+alias Set.range_injOn_strictMono := Set.range_injOn_strictMono_of_wellFoundedLT
+
+@[to_dual]
+theorem Set.range_injOn_strictAnti_of_wellFoundedGT [WellFoundedGT β] :
     Set.InjOn Set.range { f : β → γ | StrictAnti f } :=
-  fun _ hf _ hg ↦ Set.range_injOn_strictMono (β := βᵒᵈ) hf.dual hg.dual
+  fun _ hf _ hg ↦ Set.range_injOn_strictMono_of_wellFoundedLT (β := βᵒᵈ) hf.dual hg.dual
+
+@[deprecated (since := "2026-05-15")]
+alias Set.range_injOn_strictAnti := Set.range_injOn_strictAnti_of_wellFoundedGT
 
-@[to_dual range_inj_of_wellFoundedGT]
-theorem StrictMono.range_inj [WellFoundedLT β] {f g : β → γ}
+@[to_dual]
+theorem StrictMono.range_inj_of_wellFoundedLT [WellFoundedLT β] {f g : β → γ}
     (hf : StrictMono f) (hg : StrictMono g) : Set.range f = Set.range g ↔ f = g :=
-  Set.range_injOn_strictMono.eq_iff hf hg
+  Set.range_injOn_strictMono_of_wellFoundedLT.eq_iff hf hg
+
+@[deprecated (since := "2026-05-15")]
+alias StrictMono.range_inj := StrictMono.range_inj_of_wellFoundedLT
 
-@[to_dual range_inj_of_wellFoundedLT]
-theorem StrictAnti.range_inj [WellFoundedGT β] {f g : β → γ}
+@[to_dual]
+theorem StrictAnti.range_inj_of_wellFoundedGT [WellFoundedGT β] {f g : β → γ}
     (hf : StrictAnti f) (hg : StrictAnti g) : Set.range f = Set.range g ↔ f = g :=
-  Set.range_injOn_strictAnti.eq_iff hf hg
+  Set.range_injOn_strictAnti_of_wellFoundedGT.eq_iff hf hg
+
+@[deprecated (since := "2026-05-15")]
+alias StrictAnti.range_inj := StrictAnti.range_inj_of_wellFoundedGT
 
 /-- A strictly monotone function `f` on a well-order satisfies `x ≤ f x` for all `x`. -/
 @[to_dual le_id

Mathlib/SetTheory/Ordinal/Enum.lean

@@ -123,7 +123,7 @@ theorem eq_enumOrd (f : Ordinal → Ordinal) (hs : ¬ BddAbove s) :
   · rintro rfl
     exact ⟨enumOrd_strictMono hs, range_enumOrd hs⟩
   · rintro ⟨h₁, h₂⟩
-    rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]
+    rwa [← (enumOrd_strictMono hs).range_inj_of_wellFoundedLT h₁, range_enumOrd hs, eq_comm]
 
 theorem enumOrd_range {f : Ordinal → Ordinal} (hf : StrictMono f) : enumOrd (range f) = f :=
   (eq_enumOrd _ hf.not_bddAbove_range_of_wellFoundedLT).2 ⟨hf, rfl⟩