From 3f46aebe1bc3f97b5bcaf0a28faee8b94cb31985 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 25 May 2023 17:40:59 -0500
Subject: [PATCH 1/3] feat(data/real/basic): add `real.supr_nonneg` etc

Motivated by lemmas from the sphere eversion project
---
 src/data/real/basic.lean | 28 +++++++++++++++++++++++-----
 1 file changed, 23 insertions(+), 5 deletions(-)

diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
index 4009cb9258435..e49337037358d 100644
--- a/src/data/real/basic.lean
+++ b/src/data/real/basic.lean
@@ -600,7 +600,7 @@ lemma infi_of_not_bdd_below  {α : Sort*} {f : α → ℝ} (hf : ¬ bdd_below (s
 
 /--
 As `0` is the default value for `real.Sup` of the empty set or sets which are not bounded above, it
-suffices to show that `S` is bounded below by `0` to show that `0 ≤ Inf S`.
+suffices to show that `S` is bounded below by `0` to show that `0 ≤ Sup S`.
 -/
 lemma Sup_nonneg (S : set ℝ) (hS : ∀ x ∈ S, (0:ℝ) ≤ x) : 0 ≤ Sup S :=
 begin
@@ -610,15 +610,33 @@ begin
 end
 
 /--
-As `0` is the default value for `real.Sup` of the empty set, it suffices to show that `S` is
-bounded above by `0` to show that `Sup S ≤ 0`.
+As `0` is the default value for `real.Sup` of the empty set or sets which are not bounded above, it
+suffices to show that `f i` is nonnegative to show that `0 ≤ ⨆ i, f i`.
 -/
-lemma Sup_nonpos (S : set ℝ) (hS : ∀ x ∈ S, x ≤ (0:ℝ)) : Sup S ≤ 0 :=
+lemma supr_nonneg {ι : Sort*} {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i :=
+Sup_nonneg _ $ set.forall_range_iff.2 hf
+
+/--
+As `0` is the default value for `real.Sup` of the empty set or sets which are not bounded above, it
+suffices to show that all elements of `S` are bounded by a nonnagative number to show that `Sup S`
+is bounded by this number.
+-/
+lemma Sup_le {S : set ℝ} {a : ℝ} (hS : ∀ x ∈ S, x ≤ a) (ha : 0 ≤ a) : Sup S ≤ a :=
 begin
   rcases S.eq_empty_or_nonempty with rfl | hS₂,
-  exacts [Sup_empty.le, cSup_le hS₂ hS],
+  exacts [Sup_empty.trans_le ha, cSup_le hS₂ hS],
 end
 
+lemma supr_le {ι : Sort*} {f : ι → ℝ} {a : ℝ} (hS : ∀ i, f i ≤ a) (ha : 0 ≤ a) : (⨆ i, f i) ≤ a :=
+Sup_le (set.forall_range_iff.2 hS) ha
+
+/--
+As `0` is the default value for `real.Sup` of the empty set, it suffices to show that `S` is
+bounded above by `0` to show that `Sup S ≤ 0`.
+-/
+lemma Sup_nonpos (S : set ℝ) (hS : ∀ x ∈ S, x ≤ (0:ℝ)) : Sup S ≤ 0 :=
+Sup_le hS le_rfl
+
 /--
 As `0` is the default value for `real.Inf` of the empty set, it suffices to show that `S` is
 bounded below by `0` to show that `0 ≤ Inf S`.

From a94eced5d03628c7278b4aafb41733ab47af7ba0 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 25 May 2023 18:27:15 -0500
Subject: [PATCH 2/3] Fix

---
 src/analysis/normed_space/pi_Lp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index dc735f9d255b2..0bef44493cc40 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -267,7 +267,7 @@ lemma supr_edist_ne_top_aux {ι : Type*} [finite ι] {α : ι → Type*} [Π i,
 begin
   casesI nonempty_fintype ι,
   obtain ⟨M, hM⟩ := fintype.exists_le (λ i, (⟨dist (f i) (g i), dist_nonneg⟩ : ℝ≥0)),
-  refine ne_of_lt ((supr_le $ λ i, _).trans_lt (@ennreal.coe_lt_top M)),
+  refine ne_of_lt ((_root_.supr_le $ λ i, _).trans_lt (@ennreal.coe_lt_top M)),
   simp only [edist, pseudo_metric_space.edist_dist, ennreal.of_real_eq_coe_nnreal dist_nonneg],
   exact_mod_cast hM i,
 end

From 9271baa9549eccbf0a489b0cb599d16a325be87d Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 25 May 2023 19:28:03 -0500
Subject: [PATCH 3/3] Protect new lemmas

---
 src/analysis/normed_space/pi_Lp.lean |  2 +-
 src/data/real/basic.lean             | 11 ++++++-----
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index 0bef44493cc40..dc735f9d255b2 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -267,7 +267,7 @@ lemma supr_edist_ne_top_aux {ι : Type*} [finite ι] {α : ι → Type*} [Π i,
 begin
   casesI nonempty_fintype ι,
   obtain ⟨M, hM⟩ := fintype.exists_le (λ i, (⟨dist (f i) (g i), dist_nonneg⟩ : ℝ≥0)),
-  refine ne_of_lt ((_root_.supr_le $ λ i, _).trans_lt (@ennreal.coe_lt_top M)),
+  refine ne_of_lt ((supr_le $ λ i, _).trans_lt (@ennreal.coe_lt_top M)),
   simp only [edist, pseudo_metric_space.edist_dist, ennreal.of_real_eq_coe_nnreal dist_nonneg],
   exact_mod_cast hM i,
 end
diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
index e49337037358d..dbddb697e0b87 100644
--- a/src/data/real/basic.lean
+++ b/src/data/real/basic.lean
@@ -613,7 +613,7 @@ end
 As `0` is the default value for `real.Sup` of the empty set or sets which are not bounded above, it
 suffices to show that `f i` is nonnegative to show that `0 ≤ ⨆ i, f i`.
 -/
-lemma supr_nonneg {ι : Sort*} {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i :=
+protected lemma supr_nonneg {ι : Sort*} {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i :=
 Sup_nonneg _ $ set.forall_range_iff.2 hf
 
 /--
@@ -621,21 +621,22 @@ As `0` is the default value for `real.Sup` of the empty set or sets which are no
 suffices to show that all elements of `S` are bounded by a nonnagative number to show that `Sup S`
 is bounded by this number.
 -/
-lemma Sup_le {S : set ℝ} {a : ℝ} (hS : ∀ x ∈ S, x ≤ a) (ha : 0 ≤ a) : Sup S ≤ a :=
+protected lemma Sup_le {S : set ℝ} {a : ℝ} (hS : ∀ x ∈ S, x ≤ a) (ha : 0 ≤ a) : Sup S ≤ a :=
 begin
   rcases S.eq_empty_or_nonempty with rfl | hS₂,
   exacts [Sup_empty.trans_le ha, cSup_le hS₂ hS],
 end
 
-lemma supr_le {ι : Sort*} {f : ι → ℝ} {a : ℝ} (hS : ∀ i, f i ≤ a) (ha : 0 ≤ a) : (⨆ i, f i) ≤ a :=
-Sup_le (set.forall_range_iff.2 hS) ha
+protected lemma supr_le {ι : Sort*} {f : ι → ℝ} {a : ℝ} (hS : ∀ i, f i ≤ a) (ha : 0 ≤ a) :
+  (⨆ i, f i) ≤ a :=
+real.Sup_le (set.forall_range_iff.2 hS) ha
 
 /--
 As `0` is the default value for `real.Sup` of the empty set, it suffices to show that `S` is
 bounded above by `0` to show that `Sup S ≤ 0`.
 -/
 lemma Sup_nonpos (S : set ℝ) (hS : ∀ x ∈ S, x ≤ (0:ℝ)) : Sup S ≤ 0 :=
-Sup_le hS le_rfl
+real.Sup_le hS le_rfl
 
 /--
 As `0` is the default value for `real.Inf` of the empty set, it suffices to show that `S` is