feat(data/real): completeness of the (new) real numbers

algebra/group.lean

@@ -403,22 +403,14 @@ section add_comm_group
   lemma sub_sub_swap (a b c : α) : a - b - c = a - c - b :=
   by simp
 
+  lemma sub_add_sub_cancel' (a b c : α) : (a - b) + (c - a) = c - b :=
+  by rw add_comm; apply sub_add_sub_cancel
+
   lemma sub_sub_sub_cancel_left (a b c : α) : (c - a) - (c - b) = b - a :=
   by simp
 
 end add_comm_group
 
-section ordered_comm_group
-variables [ordered_comm_group α]
-
-theorem le_sub_iff_add_le {a b c : α} : a ≤ b - c ↔ a + c ≤ b :=
-by rw [add_comm]; exact ⟨add_le_of_le_sub_left, le_sub_left_of_add_le⟩
-
-theorem sub_le_iff_le_add {a b c : α} : a - c ≤ b ↔ a ≤ b + c :=
-by rw [add_comm]; exact ⟨le_add_of_sub_left_le, sub_left_le_of_le_add⟩
-
-end ordered_comm_group
-
 variables {β : Type*} [group α] [group β] {a b : α}
 
 /-- Predicate for group homomorphism. -/

algebra/ordered_field.lean

@@ -8,6 +8,11 @@ import algebra.ordered_ring algebra.field
 section linear_ordered_field
 variables {α : Type*} [linear_ordered_field α] {a b c d : α}
 
+def div_pos := @div_pos_of_pos_of_pos
+
+lemma inv_pos {a : α} : 0 < a → 0 < a⁻¹ :=
+by rw [inv_eq_one_div]; exact div_pos zero_lt_one
+
 lemma one_le_div_iff_le (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a :=
 ⟨le_of_one_le_div a hb, one_le_div_of_le a hb⟩
 
@@ -38,21 +43,31 @@ le_iff_le_iff_lt_iff_lt.1 (le_div_iff hc)
 lemma div_lt_iff_of_neg (hc : c < 0) : b / c < a ↔ a * c < b :=
 ⟨mul_lt_of_gt_div_of_neg hc, div_lt_of_mul_gt_of_neg hc⟩
 
-lemma inv_le_inv' (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
+lemma inv_le_inv (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
 by rw [inv_eq_one_div, div_le_iff ha,
        ← div_eq_inv_mul, one_le_div_iff_le hb]
 
+lemma inv_le (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a :=
+by rw [← inv_le_inv hb (inv_pos ha), division_ring.inv_inv (ne_of_gt ha)]
+
+lemma le_inv (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹ :=
+by rw [← inv_le_inv (inv_pos hb) ha, division_ring.inv_inv (ne_of_gt hb)]
+
 lemma one_div_le_one_div (ha : 0 < a) (hb : 0 < b) : 1 / a ≤ 1 / b ↔ b ≤ a :=
-by simpa [one_div_eq_inv] using inv_le_inv' ha hb
+by simpa [one_div_eq_inv] using inv_le_inv ha hb
 
 lemma inv_lt_inv (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b⁻¹ ↔ b < a :=
-le_iff_le_iff_lt_iff_lt.1 (inv_le_inv' hb ha)
+le_iff_le_iff_lt_iff_lt.1 (inv_le_inv hb ha)
+
+lemma inv_lt (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b ↔ b⁻¹ < a :=
+le_iff_le_iff_lt_iff_lt.1 (le_inv hb ha)
+
+lemma lt_inv (ha : 0 < a) (hb : 0 < b) : a < b⁻¹ ↔ b < a⁻¹ :=
+le_iff_le_iff_lt_iff_lt.1 (inv_le hb ha)
 
 lemma one_div_lt_one_div (ha : 0 < a) (hb : 0 < b) : 1 / a < 1 / b ↔ b < a :=
 le_iff_le_iff_lt_iff_lt.1 (one_div_le_one_div hb ha)
 
-def div_pos := @div_pos_of_pos_of_pos
-
 def div_nonneg := @div_nonneg_of_nonneg_of_pos
 
 lemma div_lt_div_right (hc : 0 < c) : a / c < b / c ↔ a < b :=
@@ -96,7 +111,7 @@ calc (λx, x + c) '' {r | a ≤ r ∧ r ≤ b } = (λx, x - c) ⁻¹' {r | a ≤
     congr_fun (set.image_eq_preimage_of_inverse
       (assume a, add_sub_cancel a c) (assume b, sub_add_cancel b c)) _
   ... = {r | a + c ≤ r ∧ r ≤ b + c} :
-    set.ext $ by simp [-sub_eq_add_neg, le_sub_iff_add_le, sub_le_iff_le_add]
+    set.ext $ by simp [-sub_eq_add_neg, le_sub_right_iff_add_le, sub_right_le_iff_le_add]
 
 lemma ivl_stretch (hc : 0 < c) : (λx, x * c) '' {r | a ≤ r ∧ r ≤ b } = {r | a * c ≤ r ∧ r ≤ b * c} :=
 calc (λx, x * c) '' {r | a ≤ r ∧ r ≤ b } = (λx, x / c) ⁻¹' {r | a ≤ r ∧ r ≤ b } :
@@ -119,9 +134,6 @@ instance linear_ordered_field.to_no_bot_order [linear_ordered_field α] : no_bot
 { no_bot := assume a, ⟨a + -1,
     add_lt_of_le_of_neg (le_refl _) (neg_lt_of_neg_lt $ by simp [zero_lt_one]) ⟩ }
 
-lemma inv_pos {a : α} : 0 < a → 0 < a⁻¹ :=
-by rw [inv_eq_one_div]; exact div_pos_of_pos_of_pos zero_lt_one
-
 lemma inv_lt_one {a : α} (ha : 1 < a) : a⁻¹ < 1 :=
 by rw [inv_eq_one_div]; exact div_lt_of_mul_lt_of_pos (lt_trans zero_lt_one ha) (by simp *)
 
@@ -143,8 +155,7 @@ if h : a = 0
 then by simp [h, inv_zero]
 else by rwa [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
 
-lemma inv_le_inv (hb : 0 < b) (h : b ≤ a) :
-  a⁻¹ ≤ b⁻¹ :=
+lemma inv_le_inv_of_le {a b : α} (hb : 0 < b) (h : b ≤ a) : a⁻¹ ≤ b⁻¹ :=
 begin
   rw [inv_eq_one_div, inv_eq_one_div],
   exact one_div_le_one_div_of_le hb h

algebra/ordered_group.lean

@@ -275,14 +275,14 @@ by rwa sub_self at this
 have a - b < b - b ↔ a < b, from sub_lt_sub_iff_right b,
 by rwa sub_self at this
 
-@[simp] lemma le_neg_add_iff_add_le : b ≤ -a + c ↔ a + b ≤ c :=
+lemma le_neg_add_iff_add_le : b ≤ -a + c ↔ a + b ≤ c :=
 have -a + (a + b) ≤ -a + c ↔ a + b ≤ c, from add_le_add_iff_left _,
 by rwa neg_add_cancel_left at this
 
 lemma le_sub_left_iff_add_le : b ≤ c - a ↔ a + b ≤ c :=
 by rw [sub_eq_add_neg, add_comm, le_neg_add_iff_add_le]
 
-@[simp] lemma le_sub_right_iff_add_le : a ≤ c - b ↔ a + b ≤ c :=
+lemma le_sub_right_iff_add_le : a ≤ c - b ↔ a + b ≤ c :=
 by rw [le_sub_left_iff_add_le, add_comm]
 
 @[simp] lemma neg_add_le_iff_le_add : -b + a ≤ c ↔ a ≤ b + c :=
@@ -292,7 +292,7 @@ by rwa neg_add_cancel_left at this
 lemma sub_left_le_iff_le_add : a - b ≤ c ↔ a ≤ b + c :=
 by rw [sub_eq_add_neg, add_comm, neg_add_le_iff_le_add]
 
-@[simp] lemma sub_right_le_iff_le_add : a - c ≤ b ↔ a ≤ b + c :=
+lemma sub_right_le_iff_le_add : a - c ≤ b ↔ a ≤ b + c :=
 by rw [sub_left_le_iff_le_add, add_comm]
 
 lemma neg_add_le_iff_le_add_right : -c + a ≤ b ↔ a ≤ b + c :=
@@ -307,14 +307,17 @@ by rw [neg_le_sub_iff_le_add, add_comm]
 lemma sub_le : a - b ≤ c ↔ a - c ≤ b :=
 sub_left_le_iff_le_add.trans sub_right_le_iff_le_add.symm
 
+theorem le_sub : a ≤ b - c ↔ c ≤ b - a :=
+le_sub_left_iff_add_le.trans le_sub_right_iff_add_le.symm
+
 @[simp] lemma lt_neg_add_iff_add_lt : b < -a + c ↔ a + b < c :=
 have -a + (a + b) < -a + c ↔ a + b < c, from add_lt_add_iff_left _,
 by rwa neg_add_cancel_left at this
 
 lemma lt_sub_left_iff_add_lt : b < c - a ↔ a + b < c :=
 by rw [sub_eq_add_neg, add_comm, lt_neg_add_iff_add_lt]
 
-@[simp] lemma lt_sub_right_iff_add_lt : a < c - b ↔ a + b < c :=
+lemma lt_sub_right_iff_add_lt : a < c - b ↔ a + b < c :=
 by rw [lt_sub_left_iff_add_lt, add_comm]
 
 @[simp] lemma neg_add_lt_iff_lt_add : -b + a < c ↔ a < b + c :=
@@ -324,7 +327,7 @@ by rwa neg_add_cancel_left at this
 lemma sub_left_lt_iff_lt_add : a - b < c ↔ a < b + c :=
 by rw [sub_eq_add_neg, add_comm, neg_add_lt_iff_lt_add]
 
-@[simp] lemma sub_right_lt_iff_lt_add : a - c < b ↔ a < b + c :=
+lemma sub_right_lt_iff_lt_add : a - c < b ↔ a < b + c :=
 by rw [sub_left_lt_iff_lt_add, add_comm]
 
 lemma neg_add_lt_iff_lt_add_right : -c + a < b ↔ a < b + c :=

algebra/ordered_ring.lean

@@ -99,6 +99,9 @@ le_iff_le_iff_lt_iff_lt.1 (mul_le_mul_left_of_neg h)
 @[simp] lemma mul_lt_mul_right_of_neg {a b c : α} (h : c < 0) : a * c < b * c ↔ b < a :=
 le_iff_le_iff_lt_iff_lt.1 (mul_le_mul_right_of_neg h)
 
+lemma sub_one_lt (a : α) : a - 1 < a :=
+sub_lt_iff.2 (lt_add_one a)
+
 end linear_ordered_ring
 
 set_option old_structure_cmd true

analysis/ennreal.lean

@@ -824,17 +824,18 @@ top_unique $ le_Inf $ by simp [forall_ennreal, hr] {contextual := tt}; refl
 @[simp] lemma of_real_sub_of_real (hr : 0 ≤ r) : of_real p - of_real r = of_real (p - r) :=
 match le_total p r with
 | or.inr h :=
-  have 0 ≤ p - r, from le_sub_iff_add_le.mpr $ by simp [h],
+  have 0 ≤ p - r, from le_sub_right_iff_add_le.mpr $ by simp [h],
   have eq : r + (p - r) = p, by rw [add_comm, sub_add_cancel],
   le_antisymm
     (Inf_le $ by simp [-sub_eq_add_neg, this, hr, le_trans hr h, eq, le_refl])
     (le_Inf $
-      by simp [forall_ennreal, hr, le_trans hr h, add_nonneg, -sub_eq_add_neg, this]
+      by simp [forall_ennreal, hr, le_trans hr h, add_nonneg, -sub_eq_add_neg,
+        this, sub_right_le_iff_le_add]
         {contextual := tt})
 | or.inl h :=
   begin
     rw [sub_eq_zero_of_le, of_real_of_nonpos],
-    { rw [sub_le_iff_le_add], simp [h] },
+    { rw [sub_right_le_iff_le_add], simp [h] },
     { exact of_real_le_of_real h }
   end
 end

analysis/measure_theory/lebesgue_measure.lean

@@ -42,16 +42,11 @@ le_infi $ assume a, le_infi $ assume b, le_infi $ assume hab, le_infi $ assume h
 
 lemma lebesgue_length_Ico_le_lebesgue_length_Ico {a₁ b₁ a₂ b₂ : ℝ} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) :
   lebesgue_length (Ico a₁ b₁) ≤ lebesgue_length (Ico a₂ b₂) :=
-by_cases
+(le_total b₁ a₁).elim
   (assume : b₁ ≤ a₁, by simp [Ico_eq_empty_iff.mpr this])
-  (assume : ¬ b₁ ≤ a₁,
-    have h₁ : a₁ ≤ b₁, from le_of_lt $ not_le.mp this,
+  (assume h₁ : a₁ ≤ b₁,
     have h₂ : a₂ ≤ b₂, from le_trans (le_trans ha h₁) hb,
-    have b₁ + a₂ ≤ a₁ + (b₂ - a₂) + a₂,
-      from calc b₁ + a₂ ≤ b₂ + a₁ : add_le_add hb ha
-        ... = a₁ + (b₂ - a₂) + a₂ : by rw [add_sub, sub_add_cancel, add_comm],
-    have b₁ ≤ a₁ + (b₂ - a₂), from le_of_add_le_add_right this,
-    by simp [h₁, h₂, -sub_eq_add_neg]; exact this)
+    by simp [h₁, h₂, -sub_eq_add_neg]; exact sub_le_sub hb ha)
 
 lemma lebesgue_length_subadditive {a b : ℝ} {c d : ℕ → ℝ}
   (hab : a ≤ b) (hcd : ∀i, c i ≤ d i) (habcd : Ico a b ⊆ (⋃i, Ico (c i) (d i))) :
@@ -66,8 +61,8 @@ let ⟨x, hx⟩ := exists_supremum_real ‹a ∈ M› ‹b ∈ upper_bounds M›
 have h' : is_lub ((λx, of_real (x - a)) '' M) (of_real (x - a)),
   from is_lub_of_is_lub_of_tendsto
     (assume x ⟨hx, _, _⟩ y ⟨hy, _, _⟩ h,
-      have hx : 0 ≤ x - a, by rw [le_sub_iff_add_le]; simp [hx],
-      have hy : 0 ≤ y - a, by rw [le_sub_iff_add_le]; simp [hy],
+      have hx : 0 ≤ x - a, by rw [le_sub_right_iff_add_le]; simp [hx],
+      have hy : 0 ≤ y - a, by rw [le_sub_right_iff_add_le]; simp [hy],
       by rw [ennreal.of_real_le_of_real_iff hx hy]; from sub_le_sub h (le_refl a))
     hx
     (ne_empty_iff_exists_mem.mpr ⟨a, ‹_›⟩)
@@ -154,12 +149,12 @@ outer_measure.caratheodory_is_measurable $ assume t, by_cases
     begin
       cases le_total a c with hac hca; cases le_total b c with hbc hcb;
       simp [*, max_eq_right, max_eq_left, min_eq_left, min_eq_right, le_refl,
-        -sub_eq_add_neg, add_sub_cancel'_right, add_sub],
-      { show of_real (b + b - a - a) ≤ of_real (b - a),
-        rw [ennreal.of_real_of_nonpos],
-        { apply zero_le },
-        { have : b ≤ a, from le_trans hbc hca,
-          simpa using sub_nonpos.2 (add_le_add this this) } }
+        -sub_eq_add_neg, sub_add_sub_cancel'],
+      show of_real (b - a + (b - a)) ≤ of_real (b - a),
+      rw [ennreal.of_real_of_nonpos],
+      { apply zero_le },
+      { have : b - a ≤ 0, from sub_nonpos.2 (le_trans hbc hca),
+        simpa using add_le_add this this }
     end)
   (assume h, by simp at h; from le_lebesgue_length h)
 
@@ -208,8 +203,8 @@ have hsm : ∀i j, j ≤ i → s i ≤ s j,
     from assume j, nat.cast_pos.2 $ add_pos_of_nonneg_of_pos (nat.zero_le j) zero_lt_one,
   have h₂ : (↑(j + 1) : ℝ) ≤ ↑(i + 1), from nat.cast_le.2 $ add_le_add hij (le_refl _),
   add_le_add (le_refl _) $
-  mul_le_mul (le_refl _) (inv_le_inv _ _ (h₁ j) h₂) (le_of_lt $ inv_pos $ h₁ i) $
-    by simp [le_sub_iff_add_le, -sub_eq_add_neg, le_of_lt h],
+  mul_le_mul (le_refl _) (inv_le_inv_of_le (h₁ j) h₂) (le_of_lt $ inv_pos $ h₁ i) $
+    by simp [le_sub_right_iff_add_le, -sub_eq_add_neg, le_of_lt h],
 have has : ∀i, a < s i,
   from assume i,
   have (0:ℝ) < ↑(i + 1), from nat.cast_pos.2 $ lt_add_of_le_of_pos (nat.zero_le _) zero_lt_one,

analysis/measure_theory/measurable_space.lean

@@ -441,6 +441,7 @@ lemma of_measurable_space_le_of_measurable_space_iff {m₁ m₂ : measurable_spa
   of_measurable_space m₁ ≤ of_measurable_space m₂ ↔ m₁ ≤ m₂ :=
 iff.refl _
 
+/-- The least Dynkin system containing a collection of basic sets. -/
 inductive generate_has (s : set (set α)) : set α → Prop
 | basic : ∀t∈s, generate_has t
 | empty : generate_has ∅

analysis/measure_theory/measure_space.lean

@@ -323,7 +323,7 @@ have eq₂ : ∀i, μ.measure (s 0) - (μ.measure (s 0) - μ.measure (s i)) = μ
   let ⟨r, hr, eqr, _⟩ := ennreal.lt_iff_exists_of_real.mp hfin in
   let ⟨p, hp, eqp, _⟩ := ennreal.lt_iff_exists_of_real.mp (lt_of_le_of_lt this hfin) in
   have 0 ≤ r - p,
-    by rw [le_sub_iff_add_le, zero_add, ←ennreal.of_real_le_of_real_iff hp hr, ←eqp, ←eqr];
+    by rw [le_sub_right_iff_add_le, zero_add, ←ennreal.of_real_le_of_real_iff hp hr, ←eqp, ←eqr];
     from this,
   by simp [eqr, eqp, hp, hr, this, -sub_eq_add_neg, sub_sub_self],
 calc μ.measure (⋂i, s i) = μ.measure (s 0 \ (⋃i, s 0 \ s i)) :

analysis/metric_space.lean

@@ -150,7 +150,7 @@ have d : ∀p₁ p₂ q₁ q₂:α, dist p₁ q₁ - dist p₂ q₂ ≤ dist p
     from calc dist p₁ q₁ ≤ dist p₁ p₂ + dist p₂ q₁ : dist_triangle _ _ _
       ... ≤ dist p₁ p₂ + (dist p₂ q₂ + dist q₂ q₁) : add_le_add_left (dist_triangle _ _ _) _
       ... = _ : by simp [dist_comm],
-  sub_le_iff_le_add.mpr this,
+  sub_right_le_iff_le_add.mpr this,
 have ∀{ε} {p₁ p₂ q₁ q₂ : α},
   ε > 0 → dist p₁ p₂ < ε / 2 → dist q₁ q₂ < ε / 2 → dist (dist p₁ q₁) (dist p₂ q₂) < ε,
   from assume ε p₁ p₂ q₁ q₂ hε h₁ h₂,

analysis/real.lean

@@ -567,7 +567,7 @@ lemma of_rat_mem_nonneg_iff {q : ℚ} : of_rat q ∈ nonneg ↔ 0 ≤ q :=
   of_rat_mem_nonneg⟩
 
 lemma of_rat_le {q₁ q₂ : ℚ} : of_rat q₁ ≤ of_rat q₂ ↔ q₁ ≤ q₂ :=
-by rw [le_def, of_rat_sub, of_rat_mem_nonneg_iff, le_sub_iff_add_le]; simp
+by rw [le_def, of_rat_sub, of_rat_mem_nonneg_iff, le_sub_right_iff_add_le]; simp
 
 lemma two_eq_of_rat_two : 2 = of_rat 2 := by simp [bit0, of_rat_add, of_rat_one]
 
@@ -764,7 +764,7 @@ have ∀a ∈ u ∩ of_rat '' {q : ℚ | 0 ≤ q}, a - of_rat i ∈ nonneg,
     have of_rat q ∈ v, from hiq q $ by simp [abs_of_nonneg hq, *],
     have of_rat q ∈ u ∩ v, from ⟨heq.symm ▸ hau, this⟩,
     by rwa [huv] at this,
-  heq ▸ by simp [of_rat_mem_nonneg_iff, -sub_eq_add_neg, le_sub_iff_add_le, this],
+  heq ▸ by simp [of_rat_mem_nonneg_iff, -sub_eq_add_neg, le_sub_right_iff_add_le, this],
 have r - of_rat i ∈ nonneg,
   from @mem_closure_of_continuous _ _ _ _ (λr, r - of_rat i) _ (u ∩ of_rat '' {q | 0 ≤ q}) _
     (continuous_sub continuous_id continuous_const) ‹r ∈ closure (u ∩ of_rat '' {q | 0 ≤ q})› this,

analysis/topology/topological_structures.lean

@@ -691,7 +691,8 @@ begin
       exact lt_of_add_lt_add_right this } },
   { have h : {b | abs (a + -b) < r} = {b | a - r < b} ∩ {b | b < a + r},
       from set.ext (assume b,
-        by simp [abs_lt, -sub_eq_add_neg, (sub_eq_add_neg _ _).symm, sub_lt, lt_sub_iff, and_comm]),
+        by simp [abs_lt, -sub_eq_add_neg, (sub_eq_add_neg _ _).symm,
+          sub_lt, lt_sub_iff, and_comm, sub_left_lt_iff_lt_add]),
     rw [h, ← inf_principal],
     apply le_inf _ _,
     { exact infi_le_of_le {b : α | a - r < b} (infi_le_of_le (sub_lt_self a hr) $