From 73513580b970e93e06ab76e6f7ce16315ffdd30b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Fri, 11 Feb 2022 01:36:52 +0000
Subject: [PATCH] refactor(order/well_founded, set_theory/ordinal_arithmetic):
 Fix namespace in `self_le_of_strict_mono` (#11871)

This places `self_le_of_strict_mono` in the `well_founded` namespace. We also rename `is_normal.le_self` to `is_normal.self_le` .
---
 src/order/well_founded.lean            | 17 ++++++++++-------
 src/set_theory/ordinal_arithmetic.lean | 18 +++++++++---------
 src/set_theory/principal.lean          |  2 +-
 3 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/src/order/well_founded.lean b/src/order/well_founded.lean
index c20e8c8426abb..c2ca2e0c4b515 100644
--- a/src/order/well_founded.lean
+++ b/src/order/well_founded.lean
@@ -113,6 +113,16 @@ begin
   rintro (hy | rfl), exact trans hy (wo.wf.lt_succ h), exact wo.wf.lt_succ h
 end
 
+section linear_order
+
+variables {β : Type*} [linear_order β] (h : well_founded ((<) : β → β → Prop))
+
+include h
+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₂ }
+
+end linear_order
+
 end well_founded
 
 namespace function
@@ -159,13 +169,6 @@ not_lt.mp $ not_lt_argmin f h a
   (hs : s.nonempty := set.nonempty_of_mem ha) : f (argmin_on f h s hs) ≤ f a :=
 not_lt.mp $ not_lt_argmin_on f h s ha hs
 
-include h
-theorem well_founded.self_le_of_strict_mono {φ : β → β} (hφ : strict_mono φ) : ∀ n, n ≤ φ n :=
-begin
-  by_contra' h',
-  exact h.not_lt_min _ h' (@hφ _ (h.min _ h') (h.min_mem _ h')) (h.min_mem _ h')
-end
-
 end linear_order
 
 end function
diff --git a/src/set_theory/ordinal_arithmetic.lean b/src/set_theory/ordinal_arithmetic.lean
index f416b998a6524..058c68724dab7 100644
--- a/src/set_theory/ordinal_arithmetic.lean
+++ b/src/set_theory/ordinal_arithmetic.lean
@@ -378,8 +378,8 @@ le_iff_le_iff_lt_iff_lt.2 H.lt_iff
 theorem is_normal.inj {f} (H : is_normal f) {a b} : f a = f b ↔ a = b :=
 by simp only [le_antisymm_iff, H.le_iff]
 
-theorem is_normal.le_self {f} (H : is_normal f) (a) : a ≤ f a :=
-well_founded.self_le_of_strict_mono wf H.strict_mono a
+theorem is_normal.self_le {f} (H : is_normal f) (a) : a ≤ f a :=
+wf.self_le_of_strict_mono H.strict_mono a
 
 theorem is_normal.le_set {f} (H : is_normal f) (p : set ordinal) (p0 : p.nonempty) (b)
   (H₂ : ∀ o, b ≤ o ↔ ∀ a ∈ p, a ≤ o) {o} : f b ≤ o ↔ ∀ a ∈ p, f a ≤ o :=
@@ -418,7 +418,7 @@ theorem is_normal.is_limit {f} (H : is_normal f) {o} (l : is_limit o) :
   lt_of_le_of_lt (succ_le.2 h₂) (H.lt_iff.2 h₁)⟩
 
 theorem is_normal.le_iff_eq {f} (H : is_normal f) {a} : f a ≤ a ↔ f a = a :=
-(H.le_self a).le_iff_eq
+(H.self_le a).le_iff_eq
 
 theorem add_le_of_limit {a b c : ordinal.{u}}
   (h : is_limit b) : a + b ≤ c ↔ ∀ b' < b, a + b' ≤ c :=
@@ -1354,7 +1354,7 @@ begin
   by_contra' H,
   cases omin_mem _ H with hal har,
   apply har (omin (λ b, omin _ H ≤ enum_ord S hS b)
-    ⟨_, well_founded.self_le_of_strict_mono wf (enum_ord.strict_mono hS) _⟩),
+    ⟨_, wf.self_le_of_strict_mono (enum_ord.strict_mono hS) _⟩),
   rw enum_ord_def,
   refine le_antisymm (omin_le ⟨hal, λ b hb, _⟩) _,
   { by_contra' h,
@@ -1527,7 +1527,7 @@ begin
 end
 
 theorem le_opow_self {a : ordinal} (b) (a1 : 1 < a) : b ≤ a ^ b :=
-(opow_is_normal a1).le_self _
+(opow_is_normal a1).self_le _
 
 theorem opow_lt_opow_left_of_succ {a b c : ordinal}
   (ab : a < b) : a ^ succ c < b ^ succ c :=
@@ -2174,7 +2174,7 @@ lt_sup
 protected theorem is_normal.lt_nfp {f} (H : is_normal f) {a b} : f b < nfp f a ↔ b < nfp f a :=
 lt_sup.trans $ iff.trans
   (by exact
-   ⟨λ ⟨n, h⟩, ⟨n, lt_of_le_of_lt (H.le_self _) h⟩,
+   ⟨λ ⟨n, h⟩, ⟨n, lt_of_le_of_lt (H.self_le _) h⟩,
     λ ⟨n, h⟩, ⟨n+1, by rw iterate_succ'; exact H.lt_iff.2 h⟩⟩)
   lt_sup.symm
 
@@ -2189,7 +2189,7 @@ end
 
 theorem is_normal.nfp_fp (H : is_normal f) (a) : f (nfp f a) = nfp f a :=
 begin
-  refine le_antisymm _ (H.le_self _),
+  refine le_antisymm _ (H.self_le _),
   cases le_or_lt (f a) a with aa aa,
   { rwa le_antisymm (H.nfp_le_fp le_rfl aa) (le_nfp_self _ _) },
   rcases zero_or_succ_or_limit (nfp f a) with e|⟨b, e⟩|l,
@@ -2207,7 +2207,7 @@ begin
 end
 
 theorem is_normal.le_nfp (H : is_normal f) {a b} : f b ≤ nfp f a ↔ b ≤ nfp f a :=
-⟨le_trans (H.le_self _), λ h, by simpa only [H.nfp_fp] using H.le_iff.2 h⟩
+⟨le_trans (H.self_le _), λ h, by simpa only [H.nfp_fp] using H.le_iff.2 h⟩
 
 theorem nfp_eq_self {a} (h : f a = a) : nfp f a = a :=
 le_antisymm (sup_le.mpr $ λ i, by rw [iterate_fixed h]) (le_nfp_self f a)
@@ -2251,7 +2251,7 @@ end
 theorem is_normal.le_iff_deriv (H : is_normal f) {a} : f a ≤ a ↔ ∃ o, deriv f o = a :=
 ⟨λ ha, begin
   suffices : ∀ o (_ : a ≤ deriv f o), ∃ o, deriv f o = a,
-  from this a ((deriv_is_normal _).le_self _),
+  from this a ((deriv_is_normal _).self_le _),
   refine λ o, limit_rec_on o (λ h₁, ⟨0, le_antisymm _ h₁⟩) (λ o IH h₁, _) (λ o l IH h₁, _),
   { rw deriv_zero,
     exact H.nfp_le_fp (ordinal.zero_le _) ha },
diff --git a/src/set_theory/principal.lean b/src/set_theory/principal.lean
index 13c2ea254a4f6..6651d4068203b 100644
--- a/src/set_theory/principal.lean
+++ b/src/set_theory/principal.lean
@@ -60,7 +60,7 @@ end
 theorem op_eq_self_of_principal {op : ordinal → ordinal → ordinal} {a o : ordinal.{u}}
   (hao : a < o) (H : is_normal (op a)) (ho : principal op o) (ho' : is_limit o) : op a o = o :=
 begin
-  refine le_antisymm _ (H.le_self _),
+  refine le_antisymm _ (H.self_le _),
   rw [←is_normal.bsup_eq.{u u} H ho', bsup_le],
   exact λ b hbo, le_of_lt (ho hao hbo)
 end