chore(data/real/basic): drop some lemmas (#8523)

Drop `real.Sup_le`, `real.lt_Sup`, `real.le_Sup`, `real.Sup_le_ub`, `real.le_Inf`, `real.Inf_lt`, `real.Inf_le`, `real.lb_le_Inf`. Use lemmas about `conditionally_complete_lattice`s instead.

Also drop unneeded assumptions in `real.lt_Inf_add_pos` and `real.add_neg_lt_Sup`.

archive/imo/imo1972_b2.lean

@@ -38,14 +38,9 @@ begin
 
   -- Show that `∥f x∥ ≤ k`.
   have hk₁ : ∀ x, ∥f x∥ ≤ k,
-  { have h : ∃ x, ∀ y ∈ S, y ≤ x,
-    { use 1,
-      intros _ hy,
-      rw set.mem_range at hy,
-      rcases hy with ⟨z, rfl⟩,
-      exact hf2 z, },
+  { have h : bdd_above S, from ⟨1, set.forall_range_iff.mpr hf2⟩,
     intro x,
-    exact real.le_Sup S h (set.mem_range_self x), },
+    exact le_cSup h (set.mem_range_self x), },
   -- Show that `2 * (∥f x∥ * ∥g y∥) ≤ 2 * k`.
   have hk₂ : ∀ x, 2 * (∥f x∥ * ∥g y∥) ≤ 2 * k,
   { intro x,
@@ -81,7 +76,7 @@ begin
       rw le_div_iff,
       { apply (mul_le_mul_left zero_lt_two).mp (hk₂ x) },
       { exact trans zero_lt_one hneg } },
-    apply real.Sup_le_ub _ h₁,
+    apply cSup_le h₁,
     rintros y' ⟨yy, rfl⟩,
     exact h₂ yy },
 
@@ -109,7 +104,7 @@ example (f g : ℝ → ℝ)
   ∥g(y)∥ ≤ 1 :=
 begin
   obtain ⟨x, hx⟩ := hf3,
-  set k := supr (λ x, ∥f x∥),
+  set k := ⨆ x, ∥f x∥,
   have h : ∀ x, ∥f x∥ ≤ k := le_csupr hf2,
   by_contradiction H, push_neg at H,
   have hgy : 0 < ∥g y∥,

src/algebra/pointwise.lean

@@ -316,6 +316,19 @@ end big_operators
 instance [has_inv α] : has_inv (set α) :=
 ⟨preimage has_inv.inv⟩
 
+@[simp, to_additive]
+lemma inv_empty [has_inv α] : (∅ : set α)⁻¹ = ∅ := rfl
+
+@[simp, to_additive]
+lemma inv_univ [has_inv α] : (univ : set α)⁻¹ = univ := rfl
+
+@[simp, to_additive]
+lemma nonempty_inv [group α] {s : set α} : s⁻¹.nonempty ↔ s.nonempty :=
+inv_involutive.surjective.nonempty_preimage
+
+@[to_additive] lemma nonempty.inv [group α] {s : set α} (h : s.nonempty) : s⁻¹.nonempty :=
+nonempty_inv.2 h
+
 @[simp, to_additive]
 lemma mem_inv [has_inv α] : a ∈ s⁻¹ ↔ a⁻¹ ∈ s := iff.rfl
 

src/analysis/normed_space/dual.lean

@@ -130,7 +130,7 @@ begin
   apply le_antisymm,
   { exact double_dual_bound 𝕜 E x },
   { rw continuous_linear_map.norm_def,
-    apply real.lb_le_Inf _ continuous_linear_map.bounds_nonempty,
+    apply le_cInf continuous_linear_map.bounds_nonempty,
     rintros c ⟨hc1, hc2⟩,
     exact norm_le_dual_bound 𝕜 x hc1 hc2 },
 end

src/analysis/normed_space/multilinear.lean

@@ -288,7 +288,7 @@ instance has_op_norm : has_norm (continuous_multilinear_map 𝕜 E G) := ⟨op_n
 
 lemma norm_def : ∥f∥ = Inf {c | 0 ≤ (c : ℝ) ∧ ∀ m, ∥f m∥ ≤ c * ∏ i, ∥m i∥} := rfl
 
--- So that invocations of `real.Inf_le` make sense: we show that the set of
+-- So that invocations of `le_cInf` make sense: we show that the set of
 -- bounds is nonempty and bounded below.
 lemma bounds_nonempty {f : continuous_multilinear_map 𝕜 E G} :
   ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ m, ∥f m∥ ≤ c * ∏ i, ∥m i∥} :=
@@ -299,7 +299,7 @@ lemma bounds_bdd_below {f : continuous_multilinear_map 𝕜 E G} :
 ⟨0, λ _ ⟨hn, _⟩, hn⟩
 
 lemma op_norm_nonneg : 0 ≤ ∥f∥ :=
-lb_le_Inf _ bounds_nonempty (λ _ ⟨hx, _⟩, hx)
+le_cInf bounds_nonempty (λ _ ⟨hx, _⟩, hx)
 
 /-- The fundamental property of the operator norm of a continuous multilinear map:
 `∥f m∥` is bounded by `∥f∥` times the product of the `∥m i∥`. -/
@@ -313,7 +313,7 @@ begin
     rw [this, norm_zero],
     exact mul_nonneg (op_norm_nonneg f) A },
   { rw [← div_le_iff hlt],
-    apply (le_Inf _ bounds_nonempty bounds_bdd_below).2,
+    apply le_cInf bounds_nonempty,
     rintro c ⟨_, hc⟩, rw [div_le_iff hlt], apply hc }
 end
 
@@ -335,11 +335,11 @@ calc
 /-- If one controls the norm of every `f x`, then one controls the norm of `f`. -/
 lemma op_norm_le_bound {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ m, ∥f m∥ ≤ M * ∏ i, ∥m i∥) :
   ∥f∥ ≤ M :=
-Inf_le _ bounds_bdd_below ⟨hMp, hM⟩
+cInf_le bounds_bdd_below ⟨hMp, hM⟩
 
 /-- The operator norm satisfies the triangle inequality. -/
 theorem op_norm_add_le : ∥f + g∥ ≤ ∥f∥ + ∥g∥ :=
-Inf_le _ bounds_bdd_below
+cInf_le bounds_bdd_below
   ⟨add_nonneg (op_norm_nonneg _) (op_norm_nonneg _), λ x, by { rw add_mul,
     exact norm_add_le_of_le (le_op_norm _ _) (le_op_norm _ _) }⟩
 

src/analysis/normed_space/normed_group_hom.lean

@@ -135,7 +135,7 @@ instance has_op_norm : has_norm (normed_group_hom V₁ V₂) := ⟨op_norm⟩
 
 lemma norm_def : ∥f∥ = Inf {c | 0 ≤ c ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥} := rfl
 
--- So that invocations of `real.Inf_le` make sense: we show that the set of
+-- So that invocations of `le_cInf` make sense: we show that the set of
 -- bounds is nonempty and bounded below.
 lemma bounds_nonempty {f : normed_group_hom V₁ V₂} :
   ∃ c, c ∈ { c | 0 ≤ c ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥ } :=
@@ -146,7 +146,7 @@ lemma bounds_bdd_below {f : normed_group_hom V₁ V₂} :
 ⟨0, λ _ ⟨hn, _⟩, hn⟩
 
 lemma op_norm_nonneg : 0 ≤ ∥f∥ :=
-real.lb_le_Inf _ bounds_nonempty (λ _ ⟨hx, _⟩, hx)
+le_cInf bounds_nonempty (λ _ ⟨hx, _⟩, hx)
 
 /-- The fundamental property of the operator norm: `∥f x∥ ≤ ∥f∥ * ∥x∥`. -/
 theorem le_op_norm (x : V₁) : ∥f x∥ ≤ ∥f∥ * ∥x∥ :=
@@ -156,7 +156,7 @@ begin
   by_cases h : ∥x∥ = 0,
   { rwa [h, mul_zero] at ⊢ hC },
   have hlt : 0 < ∥x∥ := lt_of_le_of_ne (norm_nonneg x) (ne.symm h),
-  exact  (div_le_iff hlt).mp ((real.le_Inf _ bounds_nonempty bounds_bdd_below).2 (λ c ⟨_, hc⟩,
+  exact (div_le_iff hlt).mp (le_cInf bounds_nonempty (λ c ⟨_, hc⟩,
     (div_le_iff hlt).mpr $ by { apply hc })),
 end
 
@@ -184,7 +184,7 @@ div_le_of_nonneg_of_le_mul (norm_nonneg _) f.op_norm_nonneg (le_op_norm _ _)
 /-- If one controls the norm of every `f x`, then one controls the norm of `f`. -/
 lemma op_norm_le_bound {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ x, ∥f x∥ ≤ M * ∥x∥) :
   ∥f∥ ≤ M :=
-real.Inf_le _ bounds_bdd_below ⟨hMp, hM⟩
+cInf_le bounds_bdd_below ⟨hMp, hM⟩
 
 theorem op_norm_le_of_lipschitz {f : normed_group_hom V₁ V₂} {K : ℝ≥0} (hf : lipschitz_with K f) :
   ∥f∥ ≤ K :=
@@ -244,7 +244,7 @@ instance : inhabited (normed_group_hom V₁ V₂) := ⟨0⟩
 
 /-- The norm of the `0` operator is `0`. -/
 theorem op_norm_zero : ∥(0 : normed_group_hom V₁ V₂)∥ = 0 :=
-le_antisymm (real.Inf_le _ bounds_bdd_below
+le_antisymm (cInf_le bounds_bdd_below
     ⟨ge_of_eq rfl, λ _, le_of_eq (by { rw [zero_mul], exact norm_zero })⟩)
     (op_norm_nonneg _)
 

src/analysis/normed_space/normed_group_quotient.lean

@@ -133,7 +133,7 @@ by rw [show x - y = -(y - x), by abel, quotient_norm_neg]
 lemma quotient_norm_mk_le (S : add_subgroup M) (m : M) :
   ∥mk' S m∥ ≤ ∥m∥ :=
 begin
-  apply real.Inf_le,
+  apply cInf_le,
   use 0,
   { rintros _ ⟨n, h, rfl⟩,
     apply norm_nonneg },
@@ -163,7 +163,7 @@ lemma quotient_norm_nonneg (S : add_subgroup M) : ∀ x : quotient S, 0 ≤ ∥x
 begin
   rintros ⟨m⟩,
   change 0 ≤ ∥mk' S m∥,
-  apply real.lb_le_Inf _ (image_norm_nonempty _),
+  apply le_cInf (image_norm_nonempty _),
   rintros _ ⟨n, h, rfl⟩,
   apply norm_nonneg
 end
@@ -202,7 +202,7 @@ lemma norm_mk_lt {S : add_subgroup M} (x : quotient S) {ε : ℝ} (hε : 0 < ε)
   ∃ (m : M), mk' S m = x ∧ ∥m∥ < ∥x∥ + ε :=
 begin
   obtain ⟨_, ⟨m : M, H : mk' S m = x, rfl⟩, hnorm : ∥m∥ < ∥x∥ + ε⟩ :=
-    real.lt_Inf_add_pos (bdd_below_image_norm _) (image_norm_nonempty x) hε,
+    real.lt_Inf_add_pos (image_norm_nonempty x) hε,
   subst H,
   exact ⟨m, rfl, hnorm⟩,
 end
@@ -471,11 +471,7 @@ begin
   have nonemp : ((λ m', ∥m + m'∥) '' f.ker).nonempty,
   { rw set.nonempty_image_iff,
     exact ⟨0, f.ker.zero_mem⟩ },
-  have bdd : bdd_below ((λ m', ∥m + m'∥) '' f.ker),
-  { use 0,
-    rintro _ ⟨x, hx, rfl⟩,
-    apply norm_nonneg },
-  rcases real.lt_Inf_add_pos bdd nonemp hε with
+  rcases real.lt_Inf_add_pos nonemp hε with
     ⟨_, ⟨⟨x, hx, rfl⟩, H : ∥m + x∥ < Inf ((λ (m' : M), ∥m + m'∥) '' f.ker) + ε⟩⟩,
   exact ⟨m+x, by rw [f.map_add,(normed_group_hom.mem_ker f x).mp hx, add_zero],
                by rwa hquot.norm⟩,
@@ -485,7 +481,7 @@ lemma is_quotient.norm_le {f : normed_group_hom M N} (hquot : is_quotient f) (m
   ∥f m∥ ≤ ∥m∥ :=
 begin
   rw hquot.norm,
-  apply real.Inf_le,
+  apply cInf_le,
   { use 0,
     rintros _ ⟨m', hm', rfl⟩,
     apply norm_nonneg },

src/analysis/normed_space/operator_norm.lean

@@ -195,7 +195,7 @@ instance has_op_norm : has_norm (E →L[𝕜] F) := ⟨op_norm⟩
 
 lemma norm_def : ∥f∥ = Inf {c | 0 ≤ c ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥} := rfl
 
--- So that invocations of `real.Inf_le` make sense: we show that the set of
+-- So that invocations of `le_cInf` make sense: we show that the set of
 -- bounds is nonempty and bounded below.
 lemma bounds_nonempty {f : E →L[𝕜] F} :
   ∃ c, c ∈ { c | 0 ≤ c ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥ } :=
@@ -206,7 +206,7 @@ lemma bounds_bdd_below {f : E →L[𝕜] F} :
 ⟨0, λ _ ⟨hn, _⟩, hn⟩
 
 lemma op_norm_nonneg : 0 ≤ ∥f∥ :=
-lb_le_Inf _ bounds_nonempty (λ _ ⟨hx, _⟩, hx)
+le_cInf bounds_nonempty (λ _ ⟨hx, _⟩, hx)
 
 /-- The fundamental property of the operator norm: `∥f x∥ ≤ ∥f∥ * ∥x∥`. -/
 theorem le_op_norm : ∥f x∥ ≤ ∥f∥ * ∥x∥ :=
@@ -216,7 +216,7 @@ begin
   by_cases h : ∥x∥ = 0,
   { rwa [h, mul_zero] at ⊢ hC },
   have hlt : 0 < ∥x∥ := lt_of_le_of_ne (norm_nonneg x) (ne.symm h),
-  exact  (div_le_iff hlt).mp ((real.le_Inf _ bounds_nonempty bounds_bdd_below).2 (λ c ⟨_, hc⟩,
+  exact  (div_le_iff hlt).mp (le_cInf bounds_nonempty (λ c ⟨_, hc⟩,
     (div_le_iff hlt).mpr $ by { apply hc })),
 end
 
@@ -236,7 +236,7 @@ mul_one ∥f∥ ▸ f.le_op_norm_of_le
 /-- If one controls the norm of every `A x`, then one controls the norm of `A`. -/
 lemma op_norm_le_bound {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ x, ∥f x∥ ≤ M * ∥x∥) :
   ∥f∥ ≤ M :=
-Inf_le _ bounds_bdd_below ⟨hMp, hM⟩
+cInf_le bounds_bdd_below ⟨hMp, hM⟩
 
 theorem op_norm_le_of_lipschitz {f : E →L[𝕜] F} {K : ℝ≥0} (hf : lipschitz_with K f) :
   ∥f∥ ≤ K :=
@@ -293,7 +293,7 @@ theorem op_norm_add_le : ∥f + g∥ ≤ ∥f∥ + ∥g∥ :=
 
 /-- The norm of the `0` operator is `0`. -/
 theorem op_norm_zero : ∥(0 : E →L[𝕜] F)∥ = 0 :=
-le_antisymm (real.Inf_le _ bounds_bdd_below
+le_antisymm (cInf_le bounds_bdd_below
     ⟨ge_of_eq rfl, λ _, le_of_eq (by { rw [zero_mul], exact norm_zero })⟩)
     (op_norm_nonneg _)
 
@@ -331,7 +331,7 @@ instance to_semi_normed_space {𝕜' : Type*} [normed_field 𝕜'] [semi_normed_
 
 /-- The operator norm is submultiplicative. -/
 lemma op_norm_comp_le (f : E →L[𝕜] F) : ∥h.comp f∥ ≤ ∥h∥ * ∥f∥ :=
-(Inf_le _ bounds_bdd_below
+(cInf_le bounds_bdd_below
   ⟨mul_nonneg (op_norm_nonneg _) (op_norm_nonneg _), λ x,
     by { rw mul_assoc, exact h.le_op_norm_of_le (f.le_op_norm x) } ⟩)
 
@@ -915,8 +915,8 @@ iff.intro
   (λ hn, continuous_linear_map.ext (λ x, norm_le_zero_iff.1
     (calc _ ≤ ∥f∥ * ∥x∥ : le_op_norm _ _
      ...     = _ : by rw [hn, zero_mul])))
-  (λ hf, le_antisymm (Inf_le _ bounds_bdd_below
-    ⟨ge_of_eq rfl, λ _, le_of_eq (by { rw [zero_mul, hf], exact norm_zero })⟩)
+  (λ hf, le_antisymm (cInf_le bounds_bdd_below
+    ⟨le_rfl, λ _, le_of_eq (by { rw [zero_mul, hf], exact norm_zero })⟩)
     (op_norm_nonneg _))
 
 /-- If a normed space is non-trivial, then the norm of the identity equals `1`. -/