diff --git a/analysis/measure_theory/borel_space.lean b/analysis/measure_theory/borel_space.lean
index 15805b8360a9d..c4b4a1f56a52f 100644
--- a/analysis/measure_theory/borel_space.lean
+++ b/analysis/measure_theory/borel_space.lean
@@ -43,7 +43,7 @@ le_antisymm
       case generate_open.inter : s₁ s₂ _ _ hs₁ hs₂
       { exact @is_measurable.inter α (generate_from s) _ _ hs₁ hs₂ },
       case generate_open.sUnion : f hf ih {
-        rcases is_open_sUnion_countable _ f (by rwa hs) with ⟨v, hv, vf, vu⟩,
+        rcases is_open_sUnion_countable f (by rwa hs) with ⟨v, hv, vf, vu⟩,
         rw ← vu,
         exact @is_measurable.sUnion α (generate_from s) _ hv
           (λ x xv, ih _ (vf xv)) }
@@ -51,6 +51,72 @@ le_antisymm
   (generate_from_le $ assume u hu, generate_measurable.basic _ $
     show t.is_open u, by rw [hs]; exact generate_open.basic _ hu)
 
+lemma borel_eq_generate_Iio (α)
+  [topological_space α] [second_countable_topology α]
+  [linear_order α] [orderable_topology α] :
+  borel α = generate_from (range Iio) :=
+begin
+  refine le_antisymm _ (generate_from_le _),
+  { rw borel_eq_generate_from_of_subbasis (orderable_topology.topology_eq_generate_intervals α),
+    have H : ∀ a:α, is_measurable (measurable_space.generate_from (range Iio)) (Iio a) :=
+      λ a, generate_measurable.basic _ ⟨_, rfl⟩,
+    refine generate_from_le _, rintro _ ⟨a, rfl | rfl⟩; [skip, apply H],
+    by_cases h : ∃ a', ∀ b, a < b ↔ a' ≤ b,
+    { rcases h with ⟨a', ha'⟩,
+      rw (_ : {b | a < b} = -Iio a'), {exact (H _).compl _},
+      simp [set.ext_iff, ha'] },
+    { rcases is_open_Union_countable
+        (λ a' : {a' : α // a < a'}, {b | a'.1 < b})
+        (λ a', is_open_lt' _) with ⟨v, ⟨hv⟩, vu⟩,
+      simp [set.ext_iff] at vu,
+      have : {b | a < b} = ⋃ x : v, -Iio x.1.1,
+      { simp [set.ext_iff],
+        refine λ x, ⟨λ ax, _, λ ⟨a', ⟨h, av⟩, ax⟩, lt_of_lt_of_le h ax⟩,
+        rcases (vu x).2 _ with ⟨a', h₁, h₂⟩,
+        { exact ⟨a', h₁, le_of_lt h₂⟩ },
+        refine not_imp_comm.1 (λ h, _) h,
+        exact ⟨x, λ b, ⟨λ ab, le_of_not_lt (λ h', h ⟨b, ab, h'⟩),
+          lt_of_lt_of_le ax⟩⟩ },
+      rw this, resetI,
+      apply is_measurable.Union,
+      exact λ _, (H _).compl _ } },
+  { simp, rintro _ a rfl,
+    exact generate_measurable.basic _ is_open_Iio }
+end
+
+lemma borel_eq_generate_Ioi (α)
+  [topological_space α] [second_countable_topology α]
+  [linear_order α] [orderable_topology α] :
+  borel α = generate_from (range (λ a, {x | a < x})) :=
+begin
+  refine le_antisymm _ (generate_from_le _),
+  { rw borel_eq_generate_from_of_subbasis (orderable_topology.topology_eq_generate_intervals α),
+    have H : ∀ a:α, is_measurable (measurable_space.generate_from (range (λ a, {x | a < x}))) {x | a < x} :=
+      λ a, generate_measurable.basic _ ⟨_, rfl⟩,
+    refine generate_from_le _, rintro _ ⟨a, rfl | rfl⟩, {apply H},
+    by_cases h : ∃ a', ∀ b, b < a ↔ b ≤ a',
+    { rcases h with ⟨a', ha'⟩,
+      rw (_ : {b | b < a} = -{x | a' < x}), {exact (H _).compl _},
+      simp [set.ext_iff, ha'] },
+    { rcases is_open_Union_countable
+        (λ a' : {a' : α // a' < a}, {b | b < a'.1})
+        (λ a', is_open_gt' _) with ⟨v, ⟨hv⟩, vu⟩,
+      simp [set.ext_iff] at vu,
+      have : {b | b < a} = ⋃ x : v, -{b | x.1.1 < b},
+      { simp [set.ext_iff],
+        refine λ x, ⟨λ ax, _, λ ⟨a', ⟨h, av⟩, ax⟩, lt_of_le_of_lt ax h⟩,
+        rcases (vu x).2 _ with ⟨a', h₁, h₂⟩,
+        { exact ⟨a', h₁, le_of_lt h₂⟩ },
+        refine not_imp_comm.1 (λ h, _) h,
+        exact ⟨x, λ b, ⟨λ ab, le_of_not_lt (λ h', h ⟨b, ab, h'⟩),
+          λ h, lt_of_le_of_lt h ax⟩⟩ },
+      rw this, resetI,
+      apply is_measurable.Union,
+      exact λ _, (H _).compl _ } },
+  { simp, rintro _ a rfl,
+    exact generate_measurable.basic _ (is_open_lt' _) }
+end
+
 lemma borel_comap {f : α → β} {t : topological_space β} :
   @borel α (t.induced f) = (@borel β t).comap f :=
 calc @borel α (t.induced f) =
@@ -144,6 +210,56 @@ lemma is_measurable_Ico : is_measurable (Ico a b) :=
 
 end ordered_topology
 
+lemma measurable.is_lub {α} [topological_space α] [linear_order α]
+  [orderable_topology α] [second_countable_topology α]
+  {β} [measurable_space β] {ι} [encodable ι]
+  {f : ι → β → α} {g : β → α} (hf : ∀ i, measurable (f i))
+  (hg : ∀ b, is_lub {a | ∃ i, f i b = a} (g b)) :
+  measurable g :=
+begin
+  rw borel_eq_generate_Ioi α,
+  apply measurable_generate_from,
+  rintro _ ⟨a, rfl⟩,
+  have : {b | a < g b} = ⋃ i, {b | a < f i b},
+  { simp [set.ext_iff], intro b, rw [lt_is_lub_iff (hg b)],
+    exact ⟨λ ⟨_, ⟨i, rfl⟩, h⟩, ⟨i, h⟩, λ ⟨i, h⟩, ⟨_, ⟨i, rfl⟩, h⟩⟩ },
+  show is_measurable {b | a < g b}, rw this,
+  exact is_measurable.Union (λ i, hf i _
+    (is_measurable_of_is_open (is_open_lt' _)))
+end
+
+lemma measurable.is_glb {α} [topological_space α] [linear_order α]
+  [orderable_topology α] [second_countable_topology α]
+  {β} [measurable_space β] {ι} [encodable ι]
+  {f : ι → β → α} {g : β → α} (hf : ∀ i, measurable (f i))
+  (hg : ∀ b, is_glb {a | ∃ i, f i b = a} (g b)) :
+  measurable g :=
+begin
+  rw borel_eq_generate_Iio α,
+  apply measurable_generate_from,
+  rintro _ ⟨a, rfl⟩,
+  have : {b | g b < a} = ⋃ i, {b | f i b < a},
+  { simp [set.ext_iff], intro b, rw [is_glb_lt_iff (hg b)],
+    exact ⟨λ ⟨_, ⟨i, rfl⟩, h⟩, ⟨i, h⟩, λ ⟨i, h⟩, ⟨_, ⟨i, rfl⟩, h⟩⟩ },
+  show is_measurable {b | g b < a}, rw this,
+  exact is_measurable.Union (λ i, hf i _
+    (is_measurable_of_is_open (is_open_gt' _)))
+end
+
+lemma measurable.supr {α} [topological_space α] [complete_linear_order α]
+  [orderable_topology α] [second_countable_topology α]
+  {β} [measurable_space β] {ι} [encodable ι]
+  {f : ι → β → α} (hf : ∀ i, measurable (f i)) :
+  measurable (λ b, ⨆ i, f i b) :=
+measurable.is_lub hf $ λ b, is_lub_supr
+
+lemma measurable.infi {α} [topological_space α] [complete_linear_order α]
+  [orderable_topology α] [second_countable_topology α]
+  {β} [measurable_space β] {ι} [encodable ι]
+  {f : ι → β → α} (hf : ∀ i, measurable (f i)) :
+  measurable (λ b, ⨅ i, f i b) :=
+measurable.is_glb hf $ λ b, is_glb_infi
+
 end
 
 end measure_theory
diff --git a/analysis/measure_theory/integration.lean b/analysis/measure_theory/integration.lean
new file mode 100644
index 0000000000000..51b2fba65f810
--- /dev/null
+++ b/analysis/measure_theory/integration.lean
@@ -0,0 +1,427 @@
+import analysis.measure_theory.measure_space algebra.pi_instances
+noncomputable theory
+open lattice set
+local attribute [instance] classical.prop_decidable
+
+namespace measure_theory
+variables {α : Type*} [measure_space α] {β : Type*} {γ : Type*}
+
+structure {u v} simple_func' (α : Type u) [measure_space α] (β : Type v) :=
+(to_fun : α → β)
+(measurable_sn : ∀ x, is_measurable (to_fun ⁻¹' {x}))
+(finite : (set.range to_fun).finite)
+local infixr ` →ₛ `:25 := simple_func'
+
+namespace simple_func'
+
+instance has_coe_to_fun : has_coe_to_fun (α →ₛ β) := ⟨_, to_fun⟩
+
+@[extensionality] theorem ext {f g : α →ₛ β} (H : ∀ a, f a = g a) : f = g :=
+by cases f; cases g; congr; exact funext H
+
+protected def range (f : α →ₛ β) := f.finite.to_finset
+
+@[simp] theorem mem_range {f : α →ₛ β} {b} :
+  b ∈ f.range ↔ ∃ a, f a = b := finite.mem_to_finset
+
+def itg (f : α →ₛ ennreal) : ennreal :=
+f.range.sum (λ x, x * volume (f ⁻¹' {x}))
+
+def const (b : β) : α →ₛ β :=
+⟨λ a, b, λ x, is_measurable.const _,
+  finite_subset (set.finite_singleton b) $ by rintro _ ⟨a, rfl⟩; simp⟩
+
+@[simp] theorem const_apply (a : α) (b : β) : (const b : α →ₛ β) a = b := rfl
+
+lemma is_measurable_cut (p : α → β → Prop) (f : α →ₛ β)
+  (h : ∀b, is_measurable {a | p a b}) : is_measurable {a | p a (f a)} :=
+begin
+  rw (_ : {a | p a (f a)} = ⋃ b ∈ set.range f, {a | p a b} ∩ f ⁻¹' {b}),
+  { exact is_measurable.bUnion (countable_finite f.finite)
+      (λ b _, is_measurable.inter (h b) (f.measurable_sn _)) },
+  ext a, simp,
+  exact ⟨λ h, ⟨_, ⟨a, rfl⟩, h, rfl⟩, λ ⟨_, ⟨a', rfl⟩, h', e⟩, e.symm ▸ h'⟩
+end
+
+theorem preimage_measurable (f : α →ₛ β) (s) : is_measurable (f ⁻¹' s) :=
+is_measurable_cut (λ _ b, b ∈ s) f (λ b, by simp [is_measurable.const])
+
+theorem measurable [measurable_space β] (f : α →ₛ β) : measurable f :=
+λ s _, preimage_measurable f s
+
+def ite {s : set α} (hs : is_measurable s) (f g : α →ₛ β) : α →ₛ β :=
+⟨λ a, if a ∈ s then f a else g a,
+ λ x, by letI : measurable_space β := ⊤; exact
+   measurable.if hs f.measurable g.measurable _ trivial,
+ finite_subset (finite_union f.finite g.finite) begin
+   rintro _ ⟨a, rfl⟩,
+   by_cases a ∈ s; simp [h],
+   exacts [or.inl ⟨_, rfl⟩, or.inr ⟨_, rfl⟩]
+ end⟩
+
+@[simp] theorem ite_apply {s : set α} (hs : is_measurable s)
+  (f g : α →ₛ β) (a) : ite hs f g a = if a ∈ s then f a else g a := rfl
+
+def bind (f : α →ₛ β) (g : β → α →ₛ γ) : α →ₛ γ :=
+⟨λa, g (f a) a,
+ λ c, is_measurable_cut (λa b, g b a ∈ ({c} : set γ)) f (λ b, (g b).measurable_sn c),
+ finite_subset (finite_bUnion f.finite (λ b, (g b).finite)) $
+ by rintro _ ⟨a, rfl⟩; simp; exact ⟨_, ⟨a, rfl⟩, _, rfl⟩⟩
+
+@[simp] theorem bind_apply (f : α →ₛ β) (g : β → α →ₛ γ) (a) :
+  f.bind g a = g (f a) a := rfl
+
+def restrict [has_zero β] (f : α →ₛ β) (s : set α) : α →ₛ β :=
+if hs : is_measurable s then ite hs f (const 0) else const 0
+
+@[simp] theorem restrict_apply [has_zero β]
+  (f : α →ₛ β) {s : set α} (hs : is_measurable s) (a) :
+  restrict f s a = if a ∈ s then f a else 0 :=
+by unfold_coes; simp [restrict, hs]; apply ite_apply hs
+
+theorem restrict_preimage [has_zero β]
+  (f : α →ₛ β) {s : set α} (hs : is_measurable s)
+  {t : set β} (ht : (0:β) ∉ t) : restrict f s ⁻¹' t = s ∩ f ⁻¹' t :=
+by ext a; dsimp; rw [restrict_apply]; by_cases a ∈ s; simp [h, hs, ht]
+
+def map (g : β → γ) (f : α →ₛ β) : α →ₛ γ := bind f (const ∘ g)
+
+@[simp] theorem map_apply (g : β → γ) (f : α →ₛ β) (a) : f.map g a = g (f a) := rfl
+
+def seq (f : α →ₛ (β → γ)) (g : α →ₛ β) : α →ₛ γ := _
+
+def pair (f : α →ₛ β) (g : α →ₛ γ) : α →ₛ (β × γ) := _
+
+@[simp] theorem map_apply (g : β → γ) (f : α →ₛ β) (a) : f.map g a = g (f a) := rfl
+
+theorem bind_const (f : α →ₛ β) : f.bind const = f := by ext; simp
+
+lemma bind_itg (f : α →ₛ β) (g : β → α →ₛ ennreal) :
+  (f.bind g).itg = f.range.sum (λ b, (restrict (g b) (f ⁻¹' {b})).itg) :=
+_
+
+lemma map_itg (g : β → ennreal) (f : α →ₛ β) :
+  (f.map g).itg = f.range.sum (λ x, g x * volume (f ⁻¹' {x})) :=
+_
+#check (by apply_instance : canonically_ordered_monoid ℕ)
+#exit
+lemma seq_itg (f : α →ₛ (β → ennreal)) (g : α →ₛ β) :
+  (f.seq g).itg = f.range.sum (λ b,
+    g.range.sum $ λ a, b a * volume (f ⁻¹' {b} ∩ g ⁻¹' {a})) :=
+_
+
+lemma bind_sum_measure (f : α →ₛ β) (g : β → (α →ₛ ennreal)) :
+  (f.bind g).itg = ∑ b x, x * volume (f ⁻¹' {b} ∩ g b ⁻¹' {x}) :=
+_
+
+theorem coe_def (f : simple_func' α) : coe_fn f = (f.map indicator.to_fun).sum := rfl
+
+instance : add_comm_monoid (simple_func' α) :=
+by unfold simple_func'; apply_instance
+
+instance : has_mem (indicator α) (simple_func' α) :=
+by unfold simple_func'; apply_instance
+
+instance : preorder (simple_func' α) :=
+{ le := λ f g, ∀ a, f a ≤ g a,
+  le_refl := λ f a, le_refl _,
+  le_trans := λ f g h h₁ h₂ a, le_trans (h₁ a) (h₂ a) }
+
+theorem le_def {f g : simple_func' α} : f ≤ g ↔ ∀ a, f a ≤ g a := iff.rfl
+theorem coe_le_coe {f g : simple_func' α} : f ≤ g ↔ ⇑f ≤ g := iff.rfl
+
+end simple_func'
+
+structure indicator (α : Type*) [measure_space α] :=
+(height : ennreal)
+(val : set α)
+(measurable : is_measurable val)
+
+def indicator.size (I : indicator α) : ennreal :=
+I.height * volume I.val
+
+def indicator.to_fun (I : indicator α) (a : α) : ennreal :=
+if a ∈ I.val then I.height else 0
+
+instance indicator.has_coe_to_fun : has_coe_to_fun (indicator α) := ⟨_, indicator.to_fun⟩
+
+theorem indicator.to_fun_val (I : indicator α) (a : α) :
+  I a = if a ∈ I.val then I.height else 0 := rfl
+
+def simple_func (α) [measure_space α] := multiset (indicator α)
+
+namespace simple_func
+
+def itg (f : simple_func α) : ennreal := (f.map indicator.size).sum
+
+def to_fun (f : simple_func α) : α → ennreal := (f.map indicator.to_fun).sum
+
+instance has_coe_to_fun : has_coe_to_fun (simple_func α) := ⟨_, to_fun⟩
+
+theorem coe_def (f : simple_func α) : coe_fn f = (f.map indicator.to_fun).sum := rfl
+
+instance : add_comm_monoid (simple_func α) :=
+by unfold simple_func; apply_instance
+
+instance : has_mem (indicator α) (simple_func α) :=
+by unfold simple_func; apply_instance
+
+instance : preorder (simple_func α) :=
+{ le := λ f g, ∀ a, f a ≤ g a,
+  le_refl := λ f a, le_refl _,
+  le_trans := λ f g h h₁ h₂ a, le_trans (h₁ a) (h₂ a) }
+
+theorem le_def {f g : simple_func α} : f ≤ g ↔ ∀ a, f a ≤ g a := iff.rfl
+theorem coe_le_coe {f g : simple_func α} : f ≤ g ↔ ⇑f ≤ g := iff.rfl
+
+instance : setoid (simple_func α) :=
+{ r := λ f g, f.to_fun = g.to_fun,
+  iseqv := preimage_equivalence _ eq_equivalence }
+
+theorem equiv_def {f g : simple_func α} : f ≈ g ↔ ⇑f = g := iff.rfl
+
+theorem equiv_iff {f g : simple_func α} : f ≈ g ↔ ∀ x, f x = g x :=
+function.funext_iff
+
+theorem le_antisymm {f g : simple_func α}
+  (h₁ : f ≤ g) (h₂ : g ≤ f) : f ≈ g :=
+le_antisymm h₁ h₂
+
+theorem le_antisymm_iff {f g : simple_func α} :
+  f ≈ g ↔ f ≤ g ∧ g ≤ f := le_antisymm_iff
+
+@[simp] theorem coe_add (f g : simple_func α) (a) : (f + g) a = f a + g a :=
+by simp [coe_def]
+
+theorem add_congr {f₁ f₂ g₁ g₂ : simple_func α}
+  (h₁ : f₁ ≈ f₂) (h₂ : g₁ ≈ g₂) : f₁ + g₁ ≈ f₂ + g₂ :=
+by simp [equiv_iff, *] at *
+
+theorem le_of_multiset_le {f g : simple_func α}
+  (h : @has_le.le (multiset _) _ f g) : f ≤ g :=
+begin
+  rcases le_iff_exists_add.1 h with ⟨k, rfl⟩,
+  intro a, simp [ennreal.le_add_right]
+end
+
+theorem itg_zero : itg (0 : simple_func α) = 0 := rfl
+
+theorem itg_add (f g) : itg (f + g : simple_func α) = itg f + itg g :=
+by simp [itg]
+
+protected def inter (f : simple_func α) (s : set α) : simple_func α :=
+let ⟨s, hs⟩ := (if hs : is_measurable s then ⟨s, hs⟩ else ⟨_, is_measurable.empty⟩ :
+  {s:set α // is_measurable s}) in
+f.map (λ ⟨a, v, hv⟩, ⟨a, v ∩ s, hv.inter hs⟩)
+
+/-
+def refines (f g : simple_func α) : Prop :=
+∀ I₁ I₂ : indicator α, I₁ ∈ f → I₂ ∈ g →
+  I₂.val ⊆ I₁.val ∨ disjoint I₁.val I₂.val
+
+local infix ` ≼ `:50 := refines
+
+def refined (f g : simple_func α) : simple_func α :=
+(multiset.diagonal f).bind $ λ ⟨s, t⟩,
+g.inter ((s.map indicator.val).inf ∩
+  (t.map (λ I:indicator α, -I.val)).inf)
+
+theorem refined_zero (g : simple_func α) : refined 0 g = g :=
+begin
+  simp [refined],
+end
+theorem refined_equiv (f g : simple_func α) : refined f g ≈ g :=
+equiv_iff.2 $ λ a, begin
+  let s := f.filter (λ I:indicator α, a ∈ I.val),
+  let t := (by exact f) - s,
+
+end
+
+theorem refines.trans {f g h : simple_func α}
+  (h₁ : f ≼ g) (h₂ : g ≼ h) : f ≼ h :=
+_
+-/
+
+theorem preimage_measurable (f : simple_func α) : ∀ s, is_measurable (f ⁻¹' s) :=
+begin
+  refine multiset.induction_on f (λ s, is_measurable.const (0 ∈ s)) (λ I f IH s, _),
+  convert ((IH {x | I.height + x ∈ s}).inter I.measurable).union
+    ((IH s).diff I.measurable),
+  simp [ext_iff, coe_def, indicator.to_fun],
+  intro a, by_cases a ∈ I.val; simp [h]
+end
+
+theorem measurable [measurable_space ennreal] (f : simple_func α) : measurable f :=
+λ s _, preimage_measurable f s
+
+def of_fun (f : α → ennreal) : simple_func α :=
+if H : (∀ a, is_measurable (f ⁻¹' {a})) ∧ (range f).finite then
+  H.2.to_finset.1.map (λ a, ⟨a, f ⁻¹' {a}, H.1 a⟩)
+else 0
+
+theorem of_fun_val {f : α → ennreal}
+  (hf : ∀ a, is_measurable (f ⁻¹' {a})) (ff : (range f).finite) :
+  of_fun f = ff.to_finset.1.map (λ a, ⟨a, f ⁻¹' {a}, hf a⟩) :=
+dif_pos ⟨hf, ff⟩
+
+theorem of_fun_apply (f : α → ennreal)
+  (hf : ∀ a, is_measurable (f ⁻¹' {a})) (ff : (range f).finite) (a) :
+  (of_fun f : α → ennreal) a = f a :=
+begin
+  rw [of_fun_val hf ff, ← multiset.cons_erase
+    (finite.mem_to_finset.2 ⟨a, rfl⟩ : f a ∈ ff.to_finset.1)],
+  simp [coe_def],
+  suffices : ∀ (s : multiset ennreal) (_:f a ∉ s),
+    (s.map (λ a, indicator.to_fun ⟨a, f ⁻¹' {a}, hf a⟩)).sum a = 0,
+  { rw this, {simp [indicator.to_fun]},
+    exact finset.not_mem_erase (f a) _ },
+  refine λ s, multiset.induction_on s (λ _, rfl) (λ I s IH h, _),
+  rw [multiset.mem_cons, not_or_distrib] at h,
+  simp [indicator.to_fun, h.1, IH h.2]
+end
+
+theorem finite_range (f : simple_func α) : (set.range f).finite :=
+begin
+  refine multiset.induction_on f _ (λ I f IH, _),
+  { refine finite_subset (finite_singleton 0) _,
+    rintro _ ⟨a, rfl⟩, simp, refl },
+  { refine finite_subset (finite_union IH (finite_image ((+) I.height) IH)) _,
+    rintro _ ⟨a, rfl⟩,
+    by_cases a ∈ I.val; simp [coe_def, indicator.to_fun, h, -add_comm],
+    { exact or.inr ⟨_, ⟨_, rfl⟩, rfl⟩ },
+    { exact or.inl ⟨_, rfl⟩ } }
+end
+
+def lift₂ (F : ennreal → ennreal → ennreal) (f g : simple_func α) :
+  simple_func α := of_fun (λ a, F (f a) (g a))
+
+lemma lift₂_is_measurable {F : ennreal → ennreal → ennreal}
+  {f g : simple_func α} (x : ennreal) :
+  is_measurable ((λ a, F (f a) (g a)) ⁻¹' {x}) :=
+begin
+  rw (_ : ((λ a, F (f a) (g a)) ⁻¹' {x}) =
+    ⋃ (a ∈ range f) (b ∈ range g) (h : F a b = x), f ⁻¹' {a} ∩ g ⁻¹' {b}),
+  { refine is_measurable.bUnion (countable_finite (finite_range _)) (λ a ha, _),
+    refine is_measurable.bUnion (countable_finite (finite_range _)) (λ b hb, _),
+    refine is_measurable.Union_Prop (λ h,
+      (preimage_measurable _ _).inter (preimage_measurable _ _)) },
+  simp [ext_iff],
+  exact λ a, ⟨λ h, ⟨_, ⟨_, rfl⟩, _, ⟨_, rfl⟩, h, rfl, rfl⟩,
+    λ ⟨_, ⟨b, rfl⟩, _, ⟨c, rfl⟩, h, h₁, h₂⟩, by clear_; cc⟩
+end
+
+lemma lift₂_finite {F : ennreal → ennreal → ennreal}
+  {f g : simple_func α} : (set.range (λ a, F (f a) (g a))).finite :=
+finite_subset (finite_image (function.uncurry F) $
+    finite_prod (finite_range f) (finite_range g)) $
+by rintro _ ⟨a, rfl⟩;
+   exact ⟨(f a, g a), mem_prod.1 ⟨⟨a, rfl⟩, ⟨a, rfl⟩⟩, rfl⟩
+
+@[simp] theorem lift₂_val (F : ennreal → ennreal → ennreal)
+  (f g : simple_func α) : ∀ a, lift₂ F f g a = F (f a) (g a) :=
+of_fun_apply _ lift₂_is_measurable lift₂_finite
+
+instance : has_sub (simple_func α) := ⟨lift₂ has_sub.sub⟩
+
+@[simp] theorem sub_val (f g : simple_func α) (a : α) : (f - g) a = f a - g a :=
+lift₂_val _ _ _ _
+
+theorem add_sub_cancel_of_le {f g : simple_func α} (h : f ≤ g) : f + (g - f) ≈ g :=
+by simp [equiv_iff, λ x, ennreal.add_sub_cancel_of_le (h x)]
+
+theorem sub_add_cancel_of_le {f g : simple_func α} (h : f ≤ g) : g - f + f ≈ g :=
+by rw add_comm; exact add_sub_cancel_of_le h
+
+-- `simple_func` is not a `canonically_ordered_monoid` because it is not a partial order
+theorem le_iff_exists_add {s t : simple_func α} : s ≤ t ↔ ∃ u, t ≈ s + u :=
+⟨λ h, ⟨_, setoid.symm (add_sub_cancel_of_le h)⟩,
+ λ ⟨u, e⟩, le_trans (by intro; simp [ennreal.le_add_right]) (le_antisymm_iff.1 e).2⟩
+
+def itg' (f : α → ennreal) : ennreal := ∑ x, x * volume (f ⁻¹' {x})
+
+theorem itg'_eq_sum_of_subset {f : α → ennreal}
+  (s : finset ennreal) (H : set.range f ⊆ ↑s) :
+  itg' f = s.sum (λ x, x * volume (f ⁻¹' {x})) :=
+tsum_eq_sum $ λ x h,
+have f ⁻¹' {x} = ∅, from
+  eq_empty_iff_forall_not_mem.2 $
+  by rintro a (rfl | ⟨⟨⟩⟩); exact h (H ⟨a, rfl⟩),
+by simp [this]
+
+theorem itg'_eq_sum {f : α → ennreal} (hf : (set.range f).finite) :
+  itg' f = hf.to_finset.sum (λ x, x * volume (f ⁻¹' {x})) :=
+itg'_eq_sum_of_subset _ (by simp)
+
+theorem itg'_zero : itg' (λ a : α, 0) = 0 :=
+begin
+  refine (congr_arg tsum _ : _).trans tsum_zero,
+  funext x,
+  by_cases x = 0, {simp [h]},
+  suffices : (λ (a : α), (0:ennreal)) ⁻¹' {x} = ∅, {simp [this]},
+  rw eq_empty_iff_forall_not_mem,
+  rintro a (rfl | ⟨⟨⟩⟩), exact h rfl
+end
+
+theorem itg'_indicator (I : indicator α) : itg' I = I.size :=
+begin
+  refine (itg'_eq_sum_of_subset {0, I.height} _).trans _,
+  { rintro _ ⟨a, rfl⟩, unfold_coes,
+    by_cases a ∈ I.val; simp [indicator.to_fun, finset.to_set, *] },
+  by_cases h : a,
+  { simpa [indicator.size] },
+end
+
+theorem itg'_add (f g : α → ennreal) :
+  itg' (f + g) = itg' f + itg' g :=
+_
+
+theorem itg'_mono {f g : α → ennreal}
+  (h : ∀ x, f x ≤ g x) : itg' f ≤ itg' g :=
+begin
+  refine (congr_arg tsum _ : _).trans tsum_zero,
+  funext x,
+  by_cases x = 0, {simp [h]},
+  suffices : (λ (a : α), (0:ennreal)) ⁻¹' {x} = ∅, {simp [this]},
+  rw eq_empty_iff_forall_not_mem,
+  rintro a (rfl | ⟨⟨⟩⟩), exact h rfl
+end
+
+theorem itg_mono {s t : simple_func α}
+  (h : s ≤ t) : s.itg ≤ t.itg :=
+begin
+
+end
+
+end simple_func
+
+def upper_itg (f : α → ennreal) :=
+⨅ (s : simple_func α) (hf : f ≤ s), s.itg
+
+def upper_itg_def_subtype (f : α → ennreal) :
+  upper_itg f = ⨅ (s : {s : simple_func α // f ≤ s}), s.itg :=
+by simp [upper_itg, infi_subtype]
+
+local notation `∫` binders `, ` r:(scoped f, upper_itg f) := r
+
+theorem upper_itg_add_le (f g : α → ennreal) : (∫ a, f a + g a) ≤ (∫ a, f a) + (∫ a, g a) :=
+begin
+  simp [upper_itg, ennreal.add_infi, ennreal.infi_add],
+  refine λ s hf t hg, infi_le_of_le (s + t) (infi_le_of_le _ _),
+  { refine λ a, le_trans (add_le_add' (hf a) (hg a)) _, simp },
+  { simp }
+end
+
+theorem simple_itg_eq (s : multiset (indicator α)) : (s.map indicator.size).sum = ∑ i,  :=
+
+theorem upper_itg_simple (s : multiset (indicator α)) : upper_itg (s.map indicator.to_fun).sum = (s.map indicator.size).sum :=
+begin
+  refine le_antisymm (infi_le_of_le s (infi_le _ (le_refl _)))
+    (le_infi $ λ t, le_infi $ λ st, _),
+
+  simp [upper_itg, ennreal.add_infi, ennreal.infi_add],
+  refine λ s hf t hg, infi_le_of_le (s + t) (infi_le_of_le _ _),
+  { refine λ a, le_trans (add_le_add' (hf a) (hg a)) _, simp },
+  { simp }
+end
+
+end measure_theory
\ No newline at end of file
diff --git a/analysis/measure_theory/lebesgue_measure.lean b/analysis/measure_theory/lebesgue_measure.lean
index da2fa93af2b3f..92c7242a75ae8 100644
--- a/analysis/measure_theory/lebesgue_measure.lean
+++ b/analysis/measure_theory/lebesgue_measure.lean
@@ -221,29 +221,50 @@ end
 
 The outer Lebesgue measure is the completion of this measure. (TODO: proof this)
 -/
-def lebesgue : measure ℝ :=
-lebesgue_outer.to_measure $
-  calc borel ℝ = measurable_space.generate_from (⋃a:ℚ, {Iio a}) :
-      real.borel_eq_generate_from_Iio_rat
-    ... ≤ lebesgue_outer.caratheodory :
-      measurable_space.generate_from_le $ by simp [is_lebesgue_measurable_Iio] {contextual := tt}
+instance : measure_space ℝ :=
+⟨{to_outer_measure := lebesgue_outer,
+  m_Union :=
+    have borel ℝ ≤ lebesgue_outer.caratheodory,
+    by rw real.borel_eq_generate_from_Iio_rat;
+       refine measurable_space.generate_from_le _;
+       simp [is_lebesgue_measurable_Iio] {contextual := tt},
+    λ f hf, lebesgue_outer.Union_eq_of_caratheodory (λ i, this _ (hf i)),
+  trimmed := lebesgue_outer_trim }⟩
 
-@[simp] theorem lebesgue_to_outer_measure : lebesgue.to_outer_measure = lebesgue_outer :=
-(to_measure_to_outer_measure _ _).trans lebesgue_outer_trim
+@[simp] theorem lebesgue_to_outer_measure :
+  (measure_space.μ : measure ℝ).to_outer_measure = lebesgue_outer := rfl
 
-theorem lebesgue_val (s) : lebesgue s = lebesgue_outer s :=
-(congr_arg (λ m:outer_measure ℝ, m s) lebesgue_to_outer_measure : _)
+theorem real.volume_val (s) : volume s = lebesgue_outer s := rfl
+local attribute [simp] real.volume_val
 
-@[simp] lemma lebesgue_Ico {a b : ℝ} : lebesgue (Ico a b) = of_real (b - a) :=
-by simp [lebesgue_val]
+@[simp] lemma real.volume_Ico {a b : ℝ} : volume (Ico a b) = of_real (b - a) := by simp
+@[simp] lemma real.volume_Icc {a b : ℝ} : volume (Icc a b) = of_real (b - a) := by simp
+@[simp] lemma real.volume_Ioo {a b : ℝ} : volume (Ioo a b) = of_real (b - a) := by simp
+@[simp] lemma real.volume_singleton {a : ℝ} : volume ({a} : set ℝ) = 0 := by simp
 
-@[simp] lemma lebesgue_Icc {a b : ℝ} : lebesgue (Icc a b) = of_real (b - a) :=
-by simp [lebesgue_val]
+/-
+section vitali
+
+def vitali_aux_h (x : ℝ) (h : x ∈ Icc (0:ℝ) 1) :
+  ∃ y ∈ Icc (0:ℝ) 1, ∃ q:ℚ, ↑q = x - y :=
+⟨x, h, 0, by simp⟩
+
+def vitali_aux (x : ℝ) (h : x ∈ Icc (0:ℝ) 1) : ℝ :=
+classical.some (vitali_aux_h x h)
+
+theorem vitali_aux_mem (x : ℝ) (h : x ∈ Icc (0:ℝ) 1) : vitali_aux x h ∈ Icc (0:ℝ) 1 :=
+Exists.fst (classical.some_spec (vitali_aux_h x h):_)
 
-@[simp] lemma lebesgue_Ioo {a b : ℝ} : lebesgue (Ioo a b) = of_real (b - a) :=
-by simp [lebesgue_val]
+theorem vitali_aux_rel (x : ℝ) (h : x ∈ Icc (0:ℝ) 1) :
+ ∃ q:ℚ, ↑q = x - vitali_aux x h :=
+Exists.snd (classical.some_spec (vitali_aux_h x h):_)
 
-@[simp] lemma lebesgue_singleton {a : ℝ} : lebesgue {a} = 0 :=
-by simp [lebesgue_val]
+def vitali : set ℝ := {x | ∃ h, x = vitali_aux x h}
+
+theorem vitali_nonmeasurable : ¬ is_null_measurable measure_space.μ vitali :=
+sorry
+
+end vitali
+-/
 
 end measure_theory
diff --git a/analysis/measure_theory/measurable_space.lean b/analysis/measure_theory/measurable_space.lean
index 809960b8ba70f..c51bcab35db15 100644
--- a/analysis/measure_theory/measurable_space.lean
+++ b/analysis/measure_theory/measurable_space.lean
@@ -36,7 +36,7 @@ lemma is_measurable.compl : is_measurable s → is_measurable (-s) :=
 lemma is_measurable.compl_iff : is_measurable (-s) ↔ is_measurable s :=
 ⟨λ h, by simpa using h.compl, is_measurable.compl⟩
 
-lemma is_measurable_univ : is_measurable (univ : set α) :=
+lemma is_measurable.univ : is_measurable (univ : set α) :=
 by simpa using (@is_measurable.empty α _).compl
 
 lemma encodable.Union_decode2 {α} [encodable β] (f : β → set α) :
@@ -71,6 +71,10 @@ lemma is_measurable.sUnion {s : set (set α)} (hs : countable s) (h : ∀t∈s,
   is_measurable (⋃₀ s) :=
 by rw sUnion_eq_bUnion; exact is_measurable.bUnion hs h
 
+lemma is_measurable.Union_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
+  is_measurable (⋃b, f b) :=
+by by_cases p; simp [h, hf, is_measurable.empty]
+
 lemma is_measurable.Inter [encodable β] {f : β → set α} (h : ∀b, is_measurable (f b)) :
   is_measurable (⋂b, f b) :=
 is_measurable.compl_iff.1 $
@@ -85,6 +89,10 @@ lemma is_measurable.sInter {s : set (set α)} (hs : countable s) (h : ∀t∈s,
   is_measurable (⋂₀ s) :=
 by rw sInter_eq_bInter; exact is_measurable.bInter hs h
 
+lemma is_measurable.Inter_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
+  is_measurable (⋂b, f b) :=
+by by_cases p; simp [h, hf, is_measurable.univ]
+
 lemma is_measurable.union {s₁ s₂ : set α}
   (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ ∪ s₂) :=
 by rw union_eq_Union; exact
@@ -107,6 +115,9 @@ lemma is_measurable.disjointed {f : ℕ → set α} (h : ∀i, is_measurable (f
   is_measurable (disjointed f n) :=
 disjointed_induct (h n) (assume t i ht, is_measurable.diff ht $ h _)
 
+lemma is_measurable.const (p : Prop) : is_measurable {a : α | p} :=
+by by_cases p; simp [h, is_measurable.empty]; apply is_measurable.univ
+
 end
 
 @[extensionality] lemma measurable_space.ext :
diff --git a/analysis/measure_theory/measure_space.lean b/analysis/measure_theory/measure_space.lean
index c0767d8e7cc80..b158ea158f1c1 100644
--- a/analysis/measure_theory/measure_space.lean
+++ b/analysis/measure_theory/measure_space.lean
@@ -182,7 +182,7 @@ le_antisymm (le_trim_iff.2 $ λ s hs, by simp [trim_eq _ hs, le_refl]) (trim_ge
 theorem trim_zero : (0 : outer_measure α).trim = 0 :=
 ext $ λ s, le_antisymm
   (le_trans ((trim 0).mono (subset_univ s)) $
-      le_of_eq $ trim_eq _ is_measurable_univ)
+    le_of_eq $ trim_eq _ is_measurable.univ)
   (zero_le _)
 
 theorem trim_add (m₁ m₂ : outer_measure α) : (m₁ + m₂).trim = m₁.trim + m₂.trim :=
@@ -215,7 +215,7 @@ For measurable sets this returns the measure assigned by the `measure_of` field
 But we can extend this to _all_ sets, but using the outer measure. This gives us monotonicity and
 subadditivity for all sets.
 -/
-instance {α} [measurable_space α] : has_coe_to_fun (measure α) :=
+instance measure.has_coe_to_fun {α} [measurable_space α] : has_coe_to_fun (measure α) :=
 ⟨λ _, set α → ennreal, λ m, m.to_outer_measure⟩
 
 namespace measure
@@ -316,7 +316,7 @@ begin
   { simpa }
 end
 
-lemma measure_sUnion [encodable β] {S : set (set α)} (hs : countable S)
+lemma measure_sUnion {S : set (set α)} (hs : countable S)
   (hd : pairwise_on S disjoint) (h : ∀s∈S, is_measurable s) :
   μ (⋃₀ S) = ∑s:S, μ s.1 :=
 by rw [sUnion_eq_bUnion, measure_bUnion hs hd h]
@@ -507,11 +507,19 @@ def count : measure α := sum dirac
 @[class] def is_complete {α} {_:measurable_space α} (μ : measure α) : Prop :=
 ∀ s, μ s = 0 → is_measurable s
 
+/-- The "almost everywhere" filter of co-null sets. -/
+def a_e (μ : measure α) : filter α :=
+{ sets := {s | μ (-s) = 0},
+  exists_mem_sets := ⟨univ, by simp [measure_empty]⟩,
+  upwards_sets := λ s t s0 h, measure_mono_null (set.compl_subset_compl.2 h) s0,
+  directed_sets := λ s s0 t t0, ⟨s ∩ t,
+    by simp [compl_inter]; exact measure_union_null s0 t0,
+    inter_subset_left _ _, inter_subset_right _ _⟩ }
+
 end measure
 
 end measure_theory
 
-
 section is_complete
 open measure_theory
 
@@ -660,3 +668,64 @@ instance completion.is_complete {α : Type u} [measurable_space α] (μ : measur
 λ z hz, null_is_null_measurable hz
 
 end is_complete
+
+namespace measure_theory
+
+/-- A measure space is a measurable space equipped with a
+  measure, referred to as `volume`. -/
+class measure_space (α : Type*) extends measurable_space α :=
+(μ {} : measure α)
+
+section measure_space
+variables {α : Type*} [measure_space α] {s₁ s₂ : set α}
+open measure_space
+
+def volume : set α → ennreal := @μ α _
+
+@[simp] lemma volume_empty : volume (∅ : set α) = 0 := μ.empty
+
+lemma volume_mono : s₁ ⊆ s₂ → volume s₁ ≤ volume s₂ := measure_mono
+
+lemma volume_mono_null : s₁ ⊆ s₂ → volume s₂ = 0 → volume s₁ = 0 :=
+measure_mono_null
+
+theorem volume_Union_le {β} [encodable β] :
+  ∀ (s : β → set α), volume (⋃i, s i) ≤ (∑i, volume (s i)) :=
+measure_Union_le
+
+lemma volume_Union_null {β} [encodable β] {s : β → set α} :
+  (∀ i, volume (s i) = 0) → volume (⋃i, s i) = 0 :=
+measure_Union_null
+
+theorem volume_union_le : ∀ (s₁ s₂ : set α), volume (s₁ ∪ s₂) ≤ volume s₁ + volume s₂ :=
+measure_union_le
+
+lemma volume_union_null : volume s₁ = 0 → volume s₂ = 0 → volume (s₁ ∪ s₂) = 0 :=
+measure_union_null
+
+lemma volume_Union {β} [encodable β] {f : β → set α} :
+  pairwise (disjoint on f) → (∀i, is_measurable (f i)) →
+  volume (⋃i, f i) = (∑i, volume (f i)) :=
+measure_Union
+
+lemma volume_union : disjoint s₁ s₂ → is_measurable s₁ → is_measurable s₂ →
+  volume (s₁ ∪ s₂) = volume s₁ + volume s₂ :=
+measure_union
+
+lemma volume_bUnion {β} {s : set β} {f : β → set α} : countable s →
+  pairwise_on s (disjoint on f) → (∀b∈s, is_measurable (f b)) →
+  volume (⋃b∈s, f b) = ∑p:s, volume (f p.1) :=
+measure_bUnion
+
+lemma volume_sUnion {S : set (set α)} : countable S →
+  pairwise_on S disjoint → (∀s∈S, is_measurable s) →
+  volume (⋃₀ S) = ∑s:S, volume s.1 :=
+measure_sUnion
+
+lemma volume_diff : s₂ ⊆ s₁ → is_measurable s₁ → is_measurable s₂ →
+  volume s₂ < ⊤ → volume (s₁ \ s₂) = volume s₁ - volume s₂ :=
+measure_diff
+
+end measure_space
+
+end measure_theory
\ No newline at end of file
diff --git a/analysis/topology/topological_space.lean b/analysis/topology/topological_space.lean
index df4ff60c2f89c..323014e67b493 100644
--- a/analysis/topology/topological_space.lean
+++ b/analysis/topology/topological_space.lean
@@ -1247,23 +1247,32 @@ let ⟨f, hf⟩ := this in
         from ne_empty_of_mem ⟨hf _ hs, mem_bUnion hs $ mem_Union.mpr ⟨hs, by simp⟩⟩,
       by simp [this]) ⟩⟩
 
-lemma is_open_sUnion_countable [second_countable_topology α]
-  (S : set (set α)) (H : ∀ s ∈ S, _root_.is_open s) :
-  ∃ T : set (set α), countable T ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S :=
+variables {α}
+
+lemma is_open_Union_countable [second_countable_topology α]
+  {ι} (s : ι → set α) (H : ∀ i, _root_.is_open (s i)) :
+  ∃ T : set ι, countable T ∧ (⋃ i ∈ T, s i) = ⋃ i, s i :=
 let ⟨B, cB, _, bB⟩ := is_open_generated_countable_inter α in
 begin
-  let B' := {b ∈ B | ∃ s ∈ S, b ⊆ s},
+  let B' := {b ∈ B | ∃ i, b ⊆ s i},
   rcases axiom_of_choice (λ b:B', b.2.2) with ⟨f, hf⟩,
-  change B' → set α at f,
+  change B' → ι at f,
   haveI : encodable B' := (countable_subset (sep_subset _ _) cB).to_encodable,
-  have : range f ⊆ S := range_subset_iff.2 (λ x, (hf x).fst),
-  exact ⟨_, countable_range f, this,
-    subset.antisymm (sUnion_subset_sUnion this) $
-    sUnion_subset $ λ s hs x xs,
-      let ⟨b, hb, xb, bs⟩ := mem_basis_subset_of_mem_open bB xs (H _ hs) in
-      ⟨_, ⟨⟨_, hb, _, hs, bs⟩, rfl⟩, (hf _).snd xb⟩⟩
+  refine ⟨_, countable_range f,
+    subset.antisymm (bUnion_subset_Union _ _) (sUnion_subset _)⟩,
+  rintro _ ⟨i, rfl⟩ x xs,
+  rcases mem_basis_subset_of_mem_open bB xs (H _) with ⟨b, hb, xb, bs⟩,
+  exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ (by exact xb)⟩
 end
 
+lemma is_open_sUnion_countable [second_countable_topology α]
+  (S : set (set α)) (H : ∀ s ∈ S, _root_.is_open s) :
+  ∃ T : set (set α), countable T ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S :=
+let ⟨T, cT, hT⟩ := is_open_Union_countable (λ s:S, s.1) (λ s, H s.1 s.2) in
+⟨subtype.val '' T, countable_image _ cT,
+  image_subset_iff.2 $ λ ⟨x, xs⟩ xt, xs,
+  by rwa [sUnion_image, sUnion_eq_Union]⟩
+
 end topological_space
 
 section limit
diff --git a/data/set/basic.lean b/data/set/basic.lean
index f305d946aa437..6db8a84d044e4 100644
--- a/data/set/basic.lean
+++ b/data/set/basic.lean
@@ -978,6 +978,9 @@ eq_univ_iff_forall
 @[simp] theorem image_univ {ι : Type*} {f : ι → β} : f '' univ = range f :=
 ext $ by simp [image, range]
 
+theorem image_subset_range {ι : Type*} (f : ι → β) (s : set ι) : f '' s ⊆ range f :=
+by rw ← image_univ; exact image_subset _ (subset_univ _)
+
 theorem range_comp {g : α → β} : range (g ∘ f) = g '' range f :=
 subset.antisymm
   (forall_range_iff.mpr $ assume i, mem_image_of_mem g (mem_range_self _))
@@ -994,10 +997,17 @@ begin
 end
 
 theorem image_preimage_eq_inter_range {f : α → β} {t : set β} :
-  f '' preimage f t = t ∩ range f :=
+  f '' (f ⁻¹' t) = t ∩ range f :=
 ext $ assume x, ⟨assume ⟨x, hx, heq⟩, heq ▸ ⟨hx, mem_range_self _⟩,
   assume ⟨hx, ⟨y, h_eq⟩⟩, h_eq ▸ mem_image_of_mem f $
-    show y ∈ preimage f t, by simp [preimage, h_eq, hx]⟩
+    show y ∈ f ⁻¹' t, by simp [preimage, h_eq, hx]⟩
+
+theorem preimage_inter_range {f : α → β} {s : set β} : f ⁻¹' (s ∩ range f) = f ⁻¹' s :=
+set.ext $ λ x, and_iff_left ⟨x, rfl⟩
+
+theorem preimage_image_preimage {f : α → β} {s : set β} :
+  f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s :=
+by rw [image_preimage_eq_inter_range, preimage_inter_range]
 
 @[simp] theorem quot_mk_range_eq [setoid α] : range (λx : α, ⟦x⟧) = univ :=
 range_iff_surjective.2 quot.exists_rep
diff --git a/data/set/finite.lean b/data/set/finite.lean
index 23165ad084aa4..44a0d9c1b7ee2 100644
--- a/data/set/finite.lean
+++ b/data/set/finite.lean
@@ -219,6 +219,10 @@ theorem finite_sUnion {s : set (set α)} (h : finite s) (H : ∀t∈s, finite t)
 by rw sUnion_eq_Union; haveI := finite.fintype h;
    apply finite_Union; simpa using H
 
+theorem finite_bUnion {α} {ι : Type*} {s : set ι} {f : ι → set α} :
+  finite s → (∀i, finite (f i)) → finite (⋃ i∈s, f i)
+| ⟨hs⟩ h := by rw [bUnion_eq_Union]; exactI finite_Union (λ i, h _)
+
 instance fintype_lt_nat (n : ℕ) : fintype {i | i < n} :=
 fintype_of_finset (finset.range n) $ by simp
 
diff --git a/data/set/lattice.lean b/data/set/lattice.lean
index e3254a623d182..b3db479bc3251 100644
--- a/data/set/lattice.lean
+++ b/data/set/lattice.lean
@@ -280,6 +280,9 @@ supr_univ
 @[simp] theorem bUnion_singleton (a : α) (s : α → set β) : (⋃ x ∈ ({a} : set α), s x) = s a :=
 supr_singleton
 
+@[simp] theorem bUnion_of_singleton (s : set α) : (⋃ x ∈ s, {x}) = s :=
+ext $ by simp
+
 theorem bUnion_union (s t : set α) (u : α → set β) :
   (⋃ x ∈ s ∪ t, u x) = (⋃ x ∈ s, u x) ∪ (⋃ x ∈ t, u x) :=
 supr_union
@@ -418,6 +421,10 @@ lemma Union_subset_Union2 {ι₂ : Sort*} {s : ι → set α} {t : ι₂ → set
 lemma Union_subset_Union_const {ι₂ : Sort x} {s : set α} (h : ι → ι₂) : (⋃ i:ι, s) ⊆ (⋃ j:ι₂, s) :=
 @supr_le_supr_const (set α) ι ι₂ _ s h
 
+theorem bUnion_subset_Union (s : set α) (t : α → set β) :
+  (⋃ x ∈ s, t x) ⊆ (⋃ x, t x) :=
+Union_subset_Union $ λ i, Union_subset $ λ h, by refl
+
 lemma sUnion_eq_bUnion {s : set (set α)} : (⋃₀ s) = (⋃ (i : set α) (h : i ∈ s), i) :=
 set.ext $ by simp
 
@@ -494,6 +501,10 @@ theorem monotone_preimage {f : α → β} : monotone (preimage f) := assume a b
   preimage f (⋃i, s i) = (⋃i, preimage f (s i)) :=
 set.ext $ by simp [preimage]
 
+theorem preimage_bUnion {ι} {f : α → β} {s : set ι} {t : ι → set β} :
+  preimage f (⋃i ∈ s, t i) = (⋃i ∈ s, preimage f (t i)) :=
+by simp
+
 @[simp] theorem preimage_sUnion {f : α → β} {s : set (set β)} :
   preimage f (⋃₀ s) = (⋃t ∈ s, preimage f t) :=
 set.ext $ by simp [preimage]
diff --git a/order/bounds.lean b/order/bounds.lean
index 5c9aedc4daa12..468e43af4ccc5 100644
--- a/order/bounds.lean
+++ b/order/bounds.lean
@@ -22,6 +22,12 @@ def is_greatest (s : set α) (a : α) : Prop := a ∈ s ∧ a ∈ upper_bounds s
 def is_lub (s : set α) : α → Prop := is_least (upper_bounds s)
 def is_glb (s : set α) : α → Prop := is_greatest (lower_bounds s)
 
+lemma upper_bounds_mono (h₁ : a₁ ≤ a₂) (h₂ : a₁ ∈ upper_bounds s) : a₂ ∈ upper_bounds s :=
+λ a h, le_trans (h₂ _ h) h₁
+
+lemma lower_bounds_mono (h₁ : a₂ ≤ a₁) (h₂ : a₁ ∈ lower_bounds s) : a₂ ∈ lower_bounds s :=
+λ a h, le_trans h₁ (h₂ _ h)
+
 lemma mem_upper_bounds_image (Hf : monotone f) (Ha : a ∈ upper_bounds s) :
   f a ∈ upper_bounds (f '' s) :=
 ball_image_of_ball (assume x H, Hf (Ha _ ‹x ∈ s›))
@@ -59,6 +65,12 @@ eq_of_is_least_of_is_least
 lemma is_lub_iff_eq_of_is_lub : is_lub s a₁ → (is_lub s a₂ ↔ a₁ = a₂) :=
 is_least_iff_eq_of_is_least
 
+lemma is_lub_le_iff (h : is_lub s a₁) : a₁ ≤ a₂ ↔ a₂ ∈ upper_bounds s :=
+⟨λ hl, upper_bounds_mono hl h.1, h.2 _⟩
+
+lemma le_is_glb_iff (h : is_glb s a₁) : a₂ ≤ a₁ ↔ a₂ ∈ lower_bounds s :=
+⟨λ hl, lower_bounds_mono hl h.1, h.2 _⟩
+
 lemma eq_of_is_glb_of_is_glb : is_glb s a₁ → is_glb s a₂ → a₁ = a₂ :=
 eq_of_is_greatest_of_is_greatest
 
@@ -113,6 +125,21 @@ is_glb_iff_eq_of_is_glb $ is_glb_insert_inf $ is_glb_singleton
 
 end lattice
 
+section linear_order
+variables [linear_order α] {a₁ a₂ : α}
+
+lemma lt_is_lub_iff (h : is_lub s a₁) : a₂ < a₁ ↔ ∃ a ∈ s, a₂ < a :=
+by haveI := classical.dec;
+   simpa [upper_bounds, not_ball] using
+   not_congr (@is_lub_le_iff _ _ a₂ _ _ h)
+
+lemma is_glb_lt_iff (h : is_glb s a₁) : a₁ < a₂ ↔ ∃ a ∈ s, a < a₂ :=
+by haveI := classical.dec;
+   simpa [lower_bounds, not_ball] using
+   not_congr (@le_is_glb_iff _ _ a₂ _ _ h)
+
+end linear_order
+
 section complete_lattice
 variables [complete_lattice α] {f : ι → α}
 
diff --git a/order/order_iso.lean b/order/order_iso.lean
index 6e85c01904720..56db6126523ee 100644
--- a/order/order_iso.lean
+++ b/order/order_iso.lean
@@ -21,6 +21,10 @@ definition subtype.order_embedding {X : Type*} (r : X → X → Prop) (p : X →
 ((subtype.val : subtype p → X) ⁻¹'o r) ≼o r :=
 ⟨⟨subtype.val,subtype.val_injective⟩,by intros;refl⟩
 
+theorem preimage_equivalence {α β} (f : α → β) {s : β → β → Prop}
+  (hs : equivalence s) : equivalence (f ⁻¹'o s) :=
+⟨λ a, hs.1 _, λ a b h, hs.2.1 h, λ a b c h₁ h₂, hs.2.2 h₁ h₂⟩
+
 namespace order_embedding
 
 instance : has_coe_to_fun (r ≼o s) := ⟨λ _, α → β, λ o, o.to_embedding⟩
diff --git a/tactic/interactive.lean b/tactic/interactive.lean
index 9e18b40209185..9a7d9d0b12729 100644
--- a/tactic/interactive.lean
+++ b/tactic/interactive.lean
@@ -119,8 +119,10 @@ l.mmap' (λ h, get_local h >>= tactic.subst) >> try (tactic.reflexivity reducibl
 
 /-- Unfold coercion-related definitions -/
 meta def unfold_coes (loc : parse location) : tactic unit :=
-unfold [``coe,``lift_t,``has_lift_t.lift,``coe_t,``has_coe_t.coe,``coe_b,``has_coe.coe,
-        ``coe_fn, ``has_coe_to_fun.coe, ``coe_sort, ``has_coe_to_sort.coe] loc
+unfold [
+  ``coe, ``coe_t, ``has_coe_t.coe, ``coe_b,``has_coe.coe,
+  ``lift, ``has_lift.lift, ``lift_t, ``has_lift_t.lift,
+  ``coe_fn, ``has_coe_to_fun.coe, ``coe_sort, ``has_coe_to_sort.coe] loc
 
 /-- Unfold auxiliary definitions associated with the current declaration. -/
 meta def unfold_aux : tactic unit :=