feat(set_theory/*): Redefine sup f as supr f (#12657)

src/data/W/cardinal.lean

@@ -68,7 +68,7 @@ calc cardinal.sum (λ a : α, m ^ #(β a))
       (λ a : α, m ^ #(β a)) :
   mul_le_mul' (le_max_left _ _) le_rfl
 ... = m : mul_eq_left.{u} (le_max_right _ _)
-  (cardinal.sup_le.2 (λ i, begin
+  (cardinal.sup_le (λ i, begin
     cases lt_omega.1 (lt_omega_iff_fintype.2 ⟨show fintype (β i), by apply_instance⟩) with n hn,
     rw [hn],
     exact power_nat_le (le_max_right _ _)

src/linear_algebra/dimension.lean

@@ -138,7 +138,7 @@ theorem dim_le {n : ℕ}
   (H : ∀ s : finset M, linear_independent R (λ i : s, (i : M)) → s.card ≤ n) :
   module.rank R M ≤ n :=
 begin
-  apply cardinal.sup_le.mpr,
+  apply cardinal.sup_le,
   rintro ⟨s, li⟩,
   exact linear_independent_bounded_of_finset_linear_independent_bounded H _ li,
 end
@@ -267,7 +267,7 @@ variables (R M)
 @[simp] lemma dim_punit : module.rank R punit = 0 :=
 begin
   apply le_bot_iff.mp,
-  apply cardinal.sup_le.mpr,
+  apply cardinal.sup_le,
   rintro ⟨s, li⟩,
   apply le_bot_iff.mpr,
   apply cardinal.mk_emptyc_iff.mpr,
@@ -792,7 +792,7 @@ begin
     apply cardinal.le_sup,
     exact ⟨set.range v, by { convert v.reindex_range.linear_independent, ext, simp }⟩,
     exact (cardinal.mk_range_eq v v.injective).ge, },
-  { apply cardinal.sup_le.mpr,
+  { apply cardinal.sup_le,
     rintro ⟨s, li⟩,
     apply linear_independent_le_basis v _ li, },
 end

src/measure_theory/card_measurable_space.lean

@@ -58,7 +58,7 @@ begin
     have D : # {j // j < i} ≤ aleph 1 := (mk_subtype_le _).trans (le_of_eq (aleph 1).mk_ord_out),
     have E : cardinal.sup.{u u}
       (λ (j : {j // j < i}), #(generate_measurable_rec s j.1)) ≤ (max (#s) 2) ^ omega.{u} :=
-    cardinal.sup_le.2 (λ ⟨j, hj⟩, IH j hj),
+    cardinal.sup_le (λ ⟨j, hj⟩, IH j hj),
     apply (mul_le_mul' D E).trans,
     rw mul_eq_max A C,
     exact max_le B le_rfl },
@@ -79,7 +79,7 @@ begin
   apply (mk_Union_le _).trans,
   rw [(aleph 1).mk_ord_out],
   refine le_trans (mul_le_mul' aleph_one_le_continuum
-    (cardinal.sup_le.2 (λ i, cardinal_generate_measurable_rec_le s i))) _,
+    (cardinal.sup_le (λ i, cardinal_generate_measurable_rec_le s i))) _,
   have := power_le_power_right (le_max_right (#s) 2),
   rw mul_eq_max omega_le_continuum (omega_le_continuum.trans this),
   exact max_le this le_rfl

src/set_theory/cardinal.lean

@@ -606,22 +606,25 @@ theorem sum_le_sum {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sum f
 /-- The indexed supremum of cardinals is the smallest cardinal above
   everything in the family. -/
 def sup {ι : Type u} (f : ι → cardinal.{max u v}) : cardinal :=
-Inf {c | ∀ i, f i ≤ c}
+Sup (set.range f)
 
-theorem nonempty_sup {ι : Type u} (f : ι → cardinal.{max u v}) : {c | ∀ i, f i ≤ c}.nonempty :=
-⟨_, le_sum f⟩
+theorem bdd_above_range {ι : Type u} (f : ι → cardinal.{max u v}) : bdd_above (set.range f) :=
+⟨_, by { rintros a ⟨i, rfl⟩, exact le_sum f i }⟩
 
 theorem le_sup {ι} (f : ι → cardinal.{max u v}) (i) : f i ≤ sup f :=
-le_cInf (nonempty_sup f) (λ b H, H i)
+le_cSup (bdd_above_range f) (mem_range_self i)
 
-theorem sup_le {ι} {f : ι → cardinal} {a} : sup f ≤ a ↔ ∀ i, f i ≤ a :=
-⟨λ h i, le_trans (le_sup _ _) h, λ h, cInf_le' h⟩
+theorem sup_le_iff {ι} {f : ι → cardinal} {a} : sup f ≤ a ↔ ∀ i, f i ≤ a :=
+(cSup_le_iff' (bdd_above_range f)).trans (by simp)
+
+theorem sup_le {ι} {f : ι → cardinal} {a} : (∀ i, f i ≤ a) → sup f ≤ a :=
+sup_le_iff.2
 
 theorem sup_le_sup {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sup f ≤ sup g :=
-sup_le.2 $ λ i, le_trans (H i) (le_sup _ _)
+sup_le $ λ i, le_trans (H i) (le_sup _ _)
 
 theorem sup_le_sum {ι} (f : ι → cardinal) : sup f ≤ sum f :=
-sup_le.2 $ le_sum _
+sup_le $ le_sum _
 
 theorem sum_le_sup {ι : Type u} (f : ι → cardinal.{u}) : sum f ≤ #ι * sup.{u u} f :=
 by rw ← sum_const'; exact sum_le_sum _ _ (le_sup _)
@@ -634,7 +637,7 @@ begin
 end
 
 theorem sup_eq_zero {ι} {f : ι → cardinal} [is_empty ι] : sup f = 0 :=
-by { rw [← nonpos_iff_eq_zero, sup_le], exact is_empty_elim }
+by { rw ←nonpos_iff_eq_zero, exact sup_le is_empty_elim }
 
 /-- The indexed product of cardinals is the cardinality of the Pi type
   (dependent product). -/
@@ -727,7 +730,7 @@ end
 
 protected lemma le_sup_iff {ι : Type v} {f : ι → cardinal.{max v w}} {c : cardinal} :
   (c ≤ sup f) ↔ (∀ b, (∀ i, f i ≤ b) → c ≤ b) :=
-⟨λ h b hb, le_trans h (sup_le.mpr hb), λ h, h _ $ λ i, le_sup f i⟩
+⟨λ h b hb, le_trans h (sup_le hb), λ h, h _ $ le_sup f⟩
 
 /-- The lift of a supremum is the supremum of the lifts. -/
 lemma lift_sup {ι : Type v} (f : ι → cardinal.{max v w}) :
@@ -736,7 +739,7 @@ begin
   apply le_antisymm,
   { rw [cardinal.le_sup_iff], intros c hc, by_contra h,
     obtain ⟨d, rfl⟩ := cardinal.lift_down (not_le.mp h).le,
-    simp only [lift_le, sup_le] at h hc,
+    simp only [lift_le, sup_le_iff] at h hc,
     exact h hc },
   { simp only [cardinal.sup_le, lift_le, le_sup, implies_true_iff] }
 end
@@ -746,7 +749,7 @@ it suffices to show that the lift of each cardinal is bounded by `t`. -/
 lemma lift_sup_le {ι : Type v} (f : ι → cardinal.{max v w})
   (t : cardinal.{max u v w}) (w : ∀ i, lift.{u} (f i) ≤ t) :
   lift.{u} (sup f) ≤ t :=
-by { rw lift_sup, exact sup_le.mpr w, }
+by { rw lift_sup, exact sup_le w }
 
 @[simp] lemma lift_sup_le_iff {ι : Type v} (f : ι → cardinal.{max v w}) (t : cardinal.{max u v w}) :
   lift.{u} (sup f) ≤ t ↔ ∀ i, lift.{u} (f i) ≤ t :=
@@ -1441,14 +1444,14 @@ by { rcases powerlt_aux h with ⟨s, rfl⟩, apply le_sup _ s }
 
 lemma powerlt_le {c₁ c₂ c₃ : cardinal} : c₁ ^< c₂ ≤ c₃ ↔ ∀(c₄ < c₂), c₁ ^ c₄ ≤ c₃ :=
 begin
-  rw [powerlt, sup_le],
+  rw [powerlt, sup_le_iff],
   split,
   { intros h c₄ hc₄, rcases powerlt_aux hc₄ with ⟨s, rfl⟩, exact h s },
   intros h s, exact h _ s.2
 end
 
 lemma powerlt_le_powerlt_left {a b c : cardinal} (h : b ≤ c) : a ^< b ≤ a ^< c :=
-by { rw [powerlt, sup_le], rintro ⟨s, hs⟩, apply le_powerlt, exact lt_of_lt_of_le hs h }
+by { rw [powerlt, sup_le_iff], exact λ ⟨s, hs⟩, le_powerlt (lt_of_lt_of_le hs h) }
 
 lemma powerlt_succ {c₁ c₂ : cardinal} (h : c₁ ≠ 0) : c₁ ^< c₂.succ = c₁ ^ c₂ :=
 begin

src/set_theory/cofinality.lean

@@ -187,7 +187,7 @@ begin
     { rwa [←typein_le_typein, typein_enum] } },
   { rcases cof_eq (<) with ⟨S, hS, hS'⟩,
     let f : S → ordinal := λ s, typein (<) s.val,
-    refine ⟨S, f, le_antisymm (lsub_le.2 (λ i, typein_lt_self i)) (le_of_forall_lt (λ a ha, _)),
+    refine ⟨S, f, le_antisymm (lsub_le (λ i, typein_lt_self i)) (le_of_forall_lt (λ a ha, _)),
       by rwa type_lt o at hS'⟩,
     rw ←type_lt o at ha,
     rcases hS (enum (<) a ha) with ⟨b, hb, hb'⟩,
@@ -350,7 +350,7 @@ begin
     ⟨embedding.of_surjective _ _⟩,
   { intro a, by_contra h,
     apply not_le_of_lt (typein_lt_type r a),
-    rw [← e', sup_le],
+    rw [← e', sup_le_iff],
     intro i,
     have h : ∀ (x : ι), r (enum r (f x) _) a, { simpa using h },
     simpa only [typein_enum] using le_of_lt ((typein_lt_typein r).2 (h i)) },
@@ -401,7 +401,7 @@ theorem sup_lt_ord {ι} (f : ι → ordinal) {c : ordinal} (H1 : #ι < c.cof)
   (H2 : ∀ i, f i < c) : sup.{u u} f < c :=
 begin
   apply lt_of_le_of_ne,
-  { rw [sup_le], exact λ i, le_of_lt (H2 i) },
+  { rw sup_le_iff, exact λ i, (H2 i).le },
   rintro h, apply not_le_of_lt H1,
   simpa [sup_ord, H2, h] using cof_sup_le.{u} f
 end