feat(Order/WellFounded): Generalize StrictMono.id_le (#16706)

This PR does the following:
- We merge `StrictMono.id_le` with its previously existing proof for a well-founded linear order, and use the `WellFoundedLT` typeclass rather than having a `WellFounded (· < ·)` argument. 
- We rename `eq_strictMono_iff_eq_range` to the more idiomatic `StrictMono.range_inj` and golf it slightly by using `Set.InjOn`. 
- We prove order duals of these theorems.

Mathlib/Data/Nat/Nth.lean

@@ -8,6 +8,7 @@ import Mathlib.Data.Nat.Count
 import Mathlib.Data.Nat.SuccPred
 import Mathlib.Order.Interval.Set.Monotone
 import Mathlib.Order.OrderIsoNat
+import Mathlib.Order.WellFounded
 
 /-!
 # The `n`th Number Satisfying a Predicate

Mathlib/Order/Hom/Set.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin
 import Mathlib.Order.Hom.Basic
 import Mathlib.Logic.Equiv.Set
 import Mathlib.Data.Set.Image
+import Mathlib.Order.WellFounded
 
 /-!
 # Order homomorphisms and sets
@@ -119,6 +120,11 @@ 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 α] [PartialOrder β] {f g : α ↪o β} :
+    Set.range f = Set.range g ↔ f = g := by
+  rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]
+
 section BooleanAlgebra
 
 variable (α) [BooleanAlgebra α]

Mathlib/Order/Monotone/Basic.lean

@@ -1014,9 +1014,6 @@ theorem Antitone.ne_of_lt_of_lt_int {f : ℤ → α} (hf : Antitone f) (n : ℤ)
   rintro rfl
   exact (hf.reflect_lt h2).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h1)
 
-theorem StrictMono.id_le {φ : ℕ → ℕ} (h : StrictMono φ) : ∀ n, n ≤ φ n := fun n ↦
-  Nat.recOn n (Nat.zero_le _) fun n hn ↦ Nat.succ_le_of_lt (hn.trans_lt <| h <| Nat.lt_succ_self n)
-
 end Preorder
 
 theorem Subtype.mono_coe [Preorder α] (t : Set α) : Monotone ((↑) : Subtype t → α) :=

Mathlib/Order/WellFounded.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro
 -/
-import Mathlib.Data.Set.Basic
+import Mathlib.Data.Set.Function
 
 /-!
 # Well-founded relations
@@ -119,48 +119,76 @@ protected theorem lt_succ_iff {r : α → α → Prop} [wo : IsWellOrder α r] {
     exact hy
   rintro (hy | rfl); (· exact _root_.trans hy (wo.wf.lt_succ h)); exact wo.wf.lt_succ h
 
+end WellFounded
+
 section LinearOrder
 
 variable [LinearOrder β] [PartialOrder γ]
 
-theorem min_le (h : WellFounded ((· < ·) : β → β → Prop)) {x : β} {s : Set β} (hx : x ∈ s)
-    (hne : s.Nonempty := ⟨x, hx⟩) : h.min s hne ≤ x :=
+theorem WellFounded.min_le (h : WellFounded ((· < ·) : β → β → Prop))
+    {x : β} {s : Set β} (hx : x ∈ s) (hne : s.Nonempty := ⟨x, hx⟩) : h.min s hne ≤ x :=
   not_lt.1 <| h.not_lt_min _ _ hx
 
-private theorem eq_strictMono_iff_eq_range_aux {f g : β → γ} (hf : StrictMono f)
-    (hg : StrictMono g) (hfg : Set.range f = Set.range g) {b : β} (H : ∀ a < b, f a = g a) :
-    f b ≤ g b := by
-  obtain ⟨c, hc⟩ : g b ∈ Set.range f := by
-    rw [hfg]
-    exact Set.mem_range_self b
+private theorem range_injOn_strictMono_aux {f g : β → γ} (hf : StrictMono f) (hg : StrictMono g)
+    (hfg : Set.range f = Set.range g) {b : β} (H : ∀ a < b, f a = g a) : f b ≤ g b := by
+  obtain ⟨c, hc⟩ : g b ∈ Set.range f := hfg ▸ Set.mem_range_self b
   rcases lt_or_le c b with hcb | hbc
-  · rw [H c hcb] at hc
-    rw [hg.injective hc] at hcb
-    exact hcb.false.elim
-  · rw [← hc]
-    exact hf.monotone hbc
-
-theorem eq_strictMono_iff_eq_range (h : WellFounded ((· < ·) : β → β → Prop))
+  · rw [H c hcb, hg.injective.eq_iff] at hc
+    exact (hc.not_lt hcb).elim
+  · rwa [← hc, hf.le_iff_le]
+
+theorem Set.range_injOn_strictMono [WellFoundedLT β] :
+    Set.InjOn Set.range { f : β → γ | StrictMono f } := by
+  intro f hf g hg hfg
+  ext a
+  apply WellFoundedLT.induction a
+  exact fun b IH => (range_injOn_strictMono_aux hf hg hfg IH).antisymm
+    (range_injOn_strictMono_aux hg hf hfg.symm fun a hab => (IH a hab).symm)
+
+theorem Set.range_injOn_strictAnti [WellFoundedGT β] :
+    Set.InjOn Set.range { f : β → γ | StrictAnti f } :=
+  fun _ hf _ hg ↦ Set.range_injOn_strictMono (β := βᵒᵈ) hf.dual hg.dual
+
+theorem StrictMono.range_inj [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
+
+theorem StrictAnti.range_inj [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
+
+@[deprecated StrictMono.range_inj (since := "2024-09-11")]
+theorem WellFounded.eq_strictMono_iff_eq_range (h : WellFounded ((· < ·) : β → β → Prop))
     {f g : β → γ} (hf : StrictMono f) (hg : StrictMono g) :
     Set.range f = Set.range g ↔ f = g :=
-  ⟨fun hfg => by
-    funext a
-    apply h.induction a
-    exact fun b H =>
-      le_antisymm (eq_strictMono_iff_eq_range_aux hf hg hfg H)
-        (eq_strictMono_iff_eq_range_aux hg hf hfg.symm fun a hab => (H a hab).symm),
-    congr_arg _⟩
-
-theorem self_le_of_strictMono (h : WellFounded ((· < ·) : β → β → Prop))
+  @StrictMono.range_inj β γ _ _ ⟨h⟩ f g hf hg
+
+/-- A strictly monotone function `f` on a well-order satisfies `x ≤ f x` for all `x`. -/
+theorem StrictMono.id_le [WellFoundedLT β] {f : β → β} (hf : StrictMono f) : id ≤ f := by
+  rw [Pi.le_def]
+  by_contra! H
+  obtain ⟨m, hm, hm'⟩ := wellFounded_lt.has_min _ H
+  exact hm' _ (hf hm) hm
+
+theorem StrictMono.le_apply [WellFoundedLT β] {f : β → β} (hf : StrictMono f) {x} : x ≤ f x :=
+  hf.id_le x
+
+/-- A strictly monotone function `f` on a cowell-order satisfies `f x ≤ x` for all `x`. -/
+theorem StrictMono.le_id [WellFoundedGT β] {f : β → β} (hf : StrictMono f) : f ≤ id :=
+  StrictMono.id_le (β := βᵒᵈ) hf.dual
+
+theorem StrictMono.apply_le [WellFoundedGT β] {f : β → β} (hf : StrictMono f) {x} : f x ≤ x :=
+  StrictMono.le_apply (β := βᵒᵈ) hf.dual
+
+@[deprecated StrictMono.le_apply (since := "2024-09-11")]
+theorem WellFounded.self_le_of_strictMono (h : WellFounded ((· < ·) : β → β → Prop))
     {f : β → β} (hf : StrictMono f) : ∀ n, n ≤ f n := by
   by_contra! h₁
   have h₂ := h.min_mem _ h₁
   exact h.not_lt_min _ h₁ (hf h₂) h₂
 
 end LinearOrder
 
-end WellFounded
-
 namespace Function
 
 variable (f : α → β)

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -384,8 +384,18 @@ theorem IsNormal.le_iff {f} (H : IsNormal f) {a b} : f a ≤ f b ↔ a ≤ b :=
 theorem IsNormal.inj {f} (H : IsNormal f) {a b} : f a = f b ↔ a = b := by
   simp only [le_antisymm_iff, H.le_iff]
 
+theorem IsNormal.id_le {f} (H : IsNormal f) : id ≤ f :=
+  H.strictMono.id_le
+
+theorem IsNormal.le_apply {f} (H : IsNormal f) {a} : a ≤ f a :=
+  H.strictMono.le_apply
+
+@[deprecated IsNormal.le_apply (since := "2024-09-11")]
 theorem IsNormal.self_le {f} (H : IsNormal f) (a) : a ≤ f a :=
-  lt_wf.self_le_of_strictMono H.strictMono a
+  H.strictMono.le_apply
+
+theorem IsNormal.le_iff_eq {f} (H : IsNormal f) {a} : f a ≤ a ↔ f a = a :=
+  H.le_apply.le_iff_eq
 
 theorem IsNormal.le_set {f o} (H : IsNormal f) (p : Set Ordinal) (p0 : p.Nonempty) (b)
     (H₂ : ∀ o, b ≤ o ↔ ∀ a ∈ p, a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f a ≤ o :=
@@ -421,9 +431,6 @@ theorem IsNormal.isLimit {f} (H : IsNormal f) {o} (l : IsLimit o) : IsLimit (f o
     let ⟨_b, h₁, h₂⟩ := (H.limit_lt l).1 h
     (succ_le_of_lt h₂).trans_lt (H.lt_iff.2 h₁)⟩
 
-theorem IsNormal.le_iff_eq {f} (H : IsNormal f) {a} : f a ≤ a ↔ f a = a :=
-  (H.self_le a).le_iff_eq
-
 theorem add_le_of_limit {a b c : Ordinal} (h : IsLimit b) : a + b ≤ c ↔ ∀ b' < b, a + b' ≤ c :=
   ⟨fun h b' l => (add_le_add_left l.le _).trans h, fun H =>
     le_of_not_lt <| by
@@ -2110,10 +2117,8 @@ theorem enumOrd_surjective (hS : Unbounded (· < ·) S) : ∀ s ∈ S, ∃ a, en
       rcases flip exists_lt_of_lt_csSup ha ⟨0, this⟩ with ⟨b, hb, hab⟩
       exact (enumOrd_strictMono hS hab).trans_le hb
     · by_contra! h
-      exact
-        (le_csSup ⟨s, fun a => (lt_wf.self_le_of_strictMono (enumOrd_strictMono hS) a).trans⟩
-              (enumOrd_succ_le hS hs h)).not_lt
-          (lt_succ _)⟩
+      exact (le_csSup ⟨s, fun a => ((enumOrd_strictMono hS).id_le a).trans⟩
+        (enumOrd_succ_le hS hs h)).not_lt (lt_succ _)⟩
 
 /-- An order isomorphism between an unbounded set of ordinals and the ordinals. -/
 def enumOrdOrderIso (hS : Unbounded (· < ·) S) : Ordinal ≃o S :=
@@ -2130,7 +2135,7 @@ theorem eq_enumOrd (f : Ordinal → Ordinal) (hS : Unbounded (· < ·) S) :
     StrictMono f ∧ range f = S ↔ f = enumOrd S := by
   constructor
   · rintro ⟨h₁, h₂⟩
-    rwa [← lt_wf.eq_strictMono_iff_eq_range h₁ (enumOrd_strictMono hS), range_enumOrd hS]
+    rwa [← h₁.range_inj (enumOrd_strictMono hS), range_enumOrd hS]
   · rintro rfl
     exact ⟨enumOrd_strictMono hS, range_enumOrd hS⟩
 

Mathlib/SetTheory/Ordinal/Exponential.lean

@@ -151,7 +151,7 @@ theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b := b
   rwa [opow_le_opow_iff_right a1, one_le_iff_pos]
 
 theorem right_le_opow {a : Ordinal} (b : Ordinal) (a1 : 1 < a) : b ≤ a ^ b :=
-  (opow_isNormal a1).self_le _
+  (opow_isNormal a1).id_le _
 
 theorem opow_lt_opow_left_of_succ {a b c : Ordinal} (ab : a < b) : a ^ succ c < b ^ succ c := by
   rw [opow_succ, opow_succ]

Mathlib/SetTheory/Ordinal/FixedPoint.lean

@@ -88,7 +88,7 @@ theorem apply_lt_nfpFamily_iff [Nonempty ι] (H : ∀ i, IsNormal (f i)) {a b} :
   · intro h
     exact lt_nfpFamily.2 <|
       let ⟨l, hl⟩ := Ordinal.lt_iSup.1 <| h <| Classical.arbitrary ι
-      ⟨l, ((H _).self_le b).trans_lt hl⟩
+      ⟨l, (H _).le_apply.trans_lt hl⟩
   · exact apply_lt_nfpFamily H
 
 theorem nfpFamily_le_apply [Nonempty ι] (H : ∀ i, IsNormal (f i)) {a b} :
@@ -110,13 +110,13 @@ theorem nfpFamily_fp {i} (H : IsNormal (f i)) (a) :
   rw [nfpFamily, H.map_iSup]
   apply le_antisymm <;> refine Ordinal.iSup_le fun l => ?_
   · exact Ordinal.le_iSup _ (i::l)
-  · exact (H.self_le _).trans (Ordinal.le_iSup _ _)
+  · exact H.le_apply.trans (Ordinal.le_iSup _ _)
 
 theorem apply_le_nfpFamily [hι : Nonempty ι] {f : ι → Ordinal → Ordinal} (H : ∀ i, IsNormal (f i))
     {a b} : (∀ i, f i b ≤ nfpFamily.{u, v} f a) ↔ b ≤ nfpFamily.{u, v} f a := by
   refine ⟨fun h => ?_, fun h i => ?_⟩
   · cases' hι with i
-    exact ((H i).self_le b).trans (h i)
+    exact (H i).le_apply.trans (h i)
   rw [← nfpFamily_fp (H i)]
   exact (H i).monotone h
 
@@ -177,7 +177,7 @@ theorem le_iff_derivFamily (H : ∀ i, IsNormal (f i)) {a} :
     (∀ i, f i a ≤ a) ↔ ∃ o, derivFamily.{u, v} f o = a :=
   ⟨fun ha => by
     suffices ∀ (o) (_ : a ≤ derivFamily.{u, v} f o), ∃ o, derivFamily.{u, v} f o = a from
-      this a ((derivFamily_isNormal _).self_le _)
+      this a (derivFamily_isNormal _).le_apply
     intro o
     induction' o using limitRecOn with o IH o l IH
     · intro h₁
@@ -292,7 +292,7 @@ theorem apply_le_nfpBFamily (ho : o ≠ 0) (H : ∀ i hi, IsNormal (f i hi)) {a
     (∀ i hi, f i hi b ≤ nfpBFamily.{u, v} o f a) ↔ b ≤ nfpBFamily.{u, v} o f a := by
   refine ⟨fun h => ?_, fun h i hi => ?_⟩
   · have ho' : 0 < o := Ordinal.pos_iff_ne_zero.2 ho
-    exact ((H 0 ho').self_le b).trans (h 0 ho')
+    exact (H 0 ho').le_apply.trans (h 0 ho')
   · rw [← nfpBFamily_fp (H i hi)]
     exact (H i hi).monotone h
 
@@ -438,7 +438,7 @@ theorem IsNormal.nfp_fp {f} (H : IsNormal f) : ∀ a, f (nfp f a) = nfp f a :=
   @nfpFamily_fp Unit (fun _ => f) Unit.unit H
 
 theorem IsNormal.apply_le_nfp {f} (H : IsNormal f) {a b} : f b ≤ nfp f a ↔ b ≤ nfp f a :=
-  ⟨le_trans (H.self_le _), fun h => by simpa only [H.nfp_fp] using H.le_iff.2 h⟩
+  ⟨H.le_apply.trans, fun h => by simpa only [H.nfp_fp] using H.le_iff.2 h⟩
 
 theorem nfp_eq_self {f : Ordinal → Ordinal} {a} (h : f a = a) : nfp f a = a :=
   nfpFamily_eq_self fun _ => h

Mathlib/SetTheory/Ordinal/Principal.lean

@@ -75,7 +75,7 @@ theorem Principal.iterate_lt {a o : Ordinal} (hao : a < o) (ho : Principal op o)
 
 theorem op_eq_self_of_principal {a o : Ordinal.{u}} (hao : a < o) (H : IsNormal (op a))
     (ho : Principal op o) (ho' : IsLimit o) : op a o = o := by
-  refine le_antisymm ?_ (H.self_le _)
+  apply H.le_apply.antisymm'
   rw [← IsNormal.bsup_eq.{u, u} H ho', bsup_le_iff]
   exact fun b hbo => (ho hao hbo).le