refactor(data/real/basic): rename for consistency

Author: digama0

analysis/real.lean

@@ -355,10 +355,4 @@ compact_of_totally_bounded_is_closed
   (real.totally_bounded_Icc a b)
   (is_closed_inter (is_closed_ge' a) (is_closed_le' b))
 
-lemma exists_supremum_real {s : set ℝ} {a b : ℝ} (ha : a ∈ s) (hb : b ∈ upper_bounds s) :
-  ∃x, is_lub s x :=
-⟨real.Sup s,
-  λ x xs, real.le_Sup s ⟨_, hb⟩ xs,
-  λ u h, real.Sup_le_ub _ ⟨_, ha⟩ h⟩
-
 end

data/real/basic.lean

@@ -333,7 +333,7 @@ theorem le_Sup (S : set ℝ) (h₂ : ∃ x, ∀ y ∈ S, y ≤ x) {x} (xS : x 
 theorem Sup_le_ub (S : set ℝ) (h₁ : ∃ x, x ∈ S) {ub} (h₂ : ∀ y ∈ S, y ≤ ub) : Sup S ≤ ub :=
 (Sup_le S h₁ ⟨_, h₂⟩).2 h₂
 
-lemma Sup_is_lub {s : set ℝ} {a b : ℝ} (ha : a ∈ s) (hb : b ∈ upper_bounds s) :
+protected lemma is_lub_Sup {s : set ℝ} {a b : ℝ} (ha : a ∈ s) (hb : b ∈ upper_bounds s) :
   is_lub s (Sup s) :=
 ⟨λ x xs, real.le_Sup s ⟨_, hb⟩ xs, 
  λ u h, real.Sup_le_ub _ ⟨_, ha⟩ h⟩

data/real/ennreal.lean

@@ -457,7 +457,7 @@ by_cases (assume h : s = ∅, ⟨0, by simp [h, is_lub, is_least, lower_bounds,
           assume ⟨r, ⟨hr₁, hr₂⟩, hr₃⟩, hr₃ ▸ hr₁⟩,
       have x ∈ of_real '' s', from s_eq ▸ hx,
       let ⟨x', hx', hx'_eq⟩ := this in
-      have is_lub s' (Sup s'), from real.Sup_is_lub ‹x' ∈ s'› $
+      have is_lub s' (Sup s'), from real.is_lub_Sup ‹x' ∈ s'› $
         (of_real_mem_upper_bounds s'_nn hr).mp $ s_eq ▸ hb,
       have 0 ≤ Sup s', from le_trans hx'.right $ this.left _ hx',
       ⟨of_real (Sup s'), by rwa [s_eq, is_lub_of_real s'_nn this]; exact ne_empty_of_mem hx'⟩)