feat(order/well_founded, set_theory/ordinal_arithmetic): eq_strict_mono_iff_eq_range (#11882)

Two strict monotonic functions with well-founded domains are equal iff their ranges are. We use this to golf `eq_enum_ord`.

Author: vihdzp

src/order/well_founded.lean

@@ -116,8 +116,32 @@ end
 section linear_order
 
 variables {β : Type*} [linear_order β] (h : well_founded ((<) : β → β → Prop))
+  {γ : Type*} [partial_order γ]
+
+private theorem eq_strict_mono_iff_eq_range_aux {f g : β → γ} (hf : strict_mono f)
+  (hg : strict_mono g) (hfg : set.range f = set.range g) {b : β} (H : ∀ a < b, f a = g a) :
+  f b ≤ g b :=
+begin
+  obtain ⟨c, hc⟩ : g b ∈ set.range f := by { rw hfg, exact set.mem_range_self b },
+  cases 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 }
+end
 
 include h
+theorem eq_strict_mono_iff_eq_range {f g : β → γ} (hf : strict_mono f)
+  (hg : strict_mono g) : set.range f = set.range g ↔ f = g :=
+⟨λ hfg, begin
+  funext a,
+  apply h.induction a,
+  exact λ b H, le_antisymm
+    (eq_strict_mono_iff_eq_range_aux hf hg hfg H)
+    (eq_strict_mono_iff_eq_range_aux hg hf hfg.symm (λ a hab, (H a hab).symm))
+end, congr_arg _⟩
+
 theorem self_le_of_strict_mono {φ : β → β} (hφ : strict_mono φ) : ∀ n, n ≤ φ n :=
 by { by_contra' h₁, have h₂ := h.min_mem _ h₁, exact h.not_lt_min _ h₁ (hφ h₂) h₂ }
 

src/set_theory/ordinal_arithmetic.lean

@@ -1379,28 +1379,13 @@ theorem enum_ord_range : range (enum_ord S hS) = S :=
 by { rw range_eq_iff, exact ⟨enum_ord_mem hS, enum_ord.surjective hS⟩ }
 
 /-- A characterization of `enum_ord`: it is the unique strict monotonic function with range `S`. -/
-theorem eq_enum_ord (f : ordinal → ordinal) :
-  strict_mono f ∧ range f = S ↔ f = enum_ord S hS :=
+theorem eq_enum_ord (f : ordinal → ordinal) : strict_mono f ∧ range f = S ↔ f = enum_ord S hS :=
 begin
-  split, swap,
+  split,
+  { rintro ⟨h₁, h₂⟩,
+    rwa [←wf.eq_strict_mono_iff_eq_range h₁ (enum_ord.strict_mono hS), enum_ord_range hS] },
   { rintro rfl,
-    exact ⟨enum_ord.strict_mono hS, enum_ord_range hS⟩ },
-  rw range_eq_iff,
-  rintro ⟨h, hl, hr⟩,
-  refine funext (λ a, _),
-  apply wf.induction a,
-  refine λ b H, le_antisymm _ _,
-  { cases hr _ (enum_ord_mem hS b) with d hd,
-    rw ←hd,
-    apply h.monotone,
-    by_contra' hbd,
-    have := enum_ord.strict_mono hS hbd,
-    rw ←(H d hbd) at this,
-    exact ne_of_lt this hd },
-  rw enum_ord_def,
-  refine omin_le ⟨hl b, λ c hc, _⟩,
-  rw ←(H c hc),
-  exact h hc
+    exact ⟨enum_ord.strict_mono hS, enum_ord_range hS⟩ }
 end
 
 end