fix(analysis/measure_theory): fix build

leanprover-community · Jan 5, 2019 · 40fa9ad · 40fa9ad
1 parent 93a330e
commit 40fa9ad
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/analysis/measure_theory/lebesgue_measure.lean b/analysis/measure_theory/lebesgue_measure.lean
@@ -183,7 +183,8 @@ le_infi $ λ a, le_infi $ λ b, le_infi $ λ h, begin
   cases le_total a c with hac hca; cases le_total b c with hbc hcb;
     simp [*, -sub_eq_add_neg, sub_add_sub_cancel'];
     rw [← ennreal.coe_add, ennreal.coe_le_coe],
-  { simp [*, nnreal.of_real_add_of_real, -sub_eq_add_neg, sub_add_sub_cancel'] },
+  { simp [*, -nnreal.of_real_add, nnreal.of_real_add_of_real,
+      -sub_eq_add_neg, sub_add_sub_cancel'] },
   { rw nnreal.of_real_of_nonpos,
     { simp },
     exact sub_nonpos.2 (le_trans hbc hca) }

diff --git a/data/real/nnreal.lean b/data/real/nnreal.lean
@@ -268,6 +268,10 @@ of_real_lt_of_real_iff'.trans (and_iff_left h)
   nnreal.of_real (r + p) = nnreal.of_real r + nnreal.of_real p :=
 nnreal.eq $ by simp [nnreal.of_real, hr, hp, add_nonneg]
 
+lemma of_real_add_of_real {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :
+  nnreal.of_real r + nnreal.of_real p = nnreal.of_real (r + p) :=
+(of_real_add hr hp).symm
+
 lemma of_real_le_of_real {r p : ℝ} (h : r ≤ p) : nnreal.of_real r ≤ nnreal.of_real p :=
 nnreal.coe_le.2 $ max_le_max h $ le_refl _