diff --git a/src/data/equiv/list.lean b/src/data/equiv/list.lean
index a78557c219daa..274f71e5848b8 100644
--- a/src/data/equiv/list.lean
+++ b/src/data/equiv/list.lean
@@ -144,24 +144,28 @@ def fintype_pi (α : Type*) (π : α → Type*) [decidable_eq α] [fintype α] [
 def sorted_univ (α) [fintype α] [encodable α] : list α :=
 finset.univ.sort (encodable.encode' α ⁻¹'o (≤))
 
-theorem mem_sorted_univ {α} [fintype α] [encodable α] (x : α) : x ∈ sorted_univ α :=
+@[simp] theorem mem_sorted_univ {α} [fintype α] [encodable α] (x : α) : x ∈ sorted_univ α :=
 (finset.mem_sort _).2 (finset.mem_univ _)
 
-theorem length_sorted_univ {α} [fintype α] [encodable α] :
+@[simp] theorem length_sorted_univ (α) [fintype α] [encodable α] :
   (sorted_univ α).length = fintype.card α :=
 finset.length_sort _
 
-theorem sorted_univ_nodup {α} [fintype α] [encodable α] : (sorted_univ α).nodup :=
+@[simp] theorem sorted_univ_nodup (α) [fintype α] [encodable α] : (sorted_univ α).nodup :=
 finset.sort_nodup _ _
 
+@[simp] theorem sorted_univ_to_finset (α) [fintype α] [encodable α] [decidable_eq α] :
+  (sorted_univ α).to_finset = finset.univ :=
+finset.sort_to_finset _ _
+
 /-- An encodable `fintype` is equivalent to the same size `fin`. -/
 def fintype_equiv_fin {α} [fintype α] [encodable α] :
   α ≃ fin (fintype.card α) :=
 begin
   haveI : decidable_eq α := encodable.decidable_eq_of_encodable _,
   transitivity,
-  { exact fintype.equiv_fin_of_forall_mem_list mem_sorted_univ (@sorted_univ_nodup α _ _) },
-  exact equiv.cast (congr_arg _ (@length_sorted_univ α _ _))
+  { exact fintype.equiv_fin_of_forall_mem_list mem_sorted_univ (sorted_univ_nodup α) },
+  exact equiv.cast (congr_arg _ (length_sorted_univ α))
 end
 
 /-- If `α` and `β` are encodable and `α` is a fintype, then `α → β` is encodable as well. -/
diff --git a/src/measure_theory/constructions/pi.lean b/src/measure_theory/constructions/pi.lean
index 7cb435d0e8f9d..fcd29e3840ae4 100644
--- a/src/measure_theory/constructions/pi.lean
+++ b/src/measure_theory/constructions/pi.lean
@@ -218,20 +218,11 @@ begin
 end
 
 lemma tprod_tprod (l : list δ) (μ : Π i, measure (π i)) [∀ i, sigma_finite (μ i)]
-  {s : Π i, set (π i)} (hs : ∀ i, measurable_set (s i)) :
+  (s : Π i, set (π i)) :
   measure.tprod l μ (set.tprod l s) = (l.map (λ i, (μ i) (s i))).prod :=
 begin
   induction l with i l ih, { simp },
-  simp_rw [tprod_cons, set.tprod, prod_prod (hs i) (measurable_set.tprod l hs), map_cons,
-    prod_cons, ih]
-end
-
-lemma tprod_tprod_le (l : list δ) (μ : Π i, measure (π i)) [∀ i, sigma_finite (μ i)]
-  (s : Π i, set (π i)) : measure.tprod l μ (set.tprod l s) ≤ (l.map (λ i, (μ i) (s i))).prod :=
-begin
-  induction l with i l ih, { simp [le_refl] },
-  simp_rw [tprod_cons, set.tprod, map_cons, prod_cons],
-  refine (prod_prod_le _ _).trans _, exact ennreal.mul_left_mono ih
+  rw [tprod_cons, set.tprod, prod_prod, map_cons, prod_cons, ih]
 end
 
 end tprod
@@ -247,28 +238,10 @@ variables [encodable ι]
 def pi' : measure (Π i, α i) :=
 measure.map (tprod.elim' mem_sorted_univ) (measure.tprod (sorted_univ ι) μ)
 
-lemma pi'_pi [∀ i, sigma_finite (μ i)] {s : Π i, set (α i)}
-  (hs : ∀ i, measurable_set (s i)) : pi' μ (pi univ s) = ∏ i, μ i (s i) :=
-begin
-  have hl := λ i : ι, mem_sorted_univ i,
-  have hnd := @sorted_univ_nodup ι _ _,
-  rw [pi', map_apply (measurable_tprod_elim' hl) (measurable_set.pi_fintype (λ i _, hs i)),
-    elim_preimage_pi hnd, tprod_tprod _ μ hs, ← list.prod_to_finset _ hnd],
-  congr' with i, simp [hl]
-end
-
-lemma pi'_pi_le [∀ i, sigma_finite (μ i)] {s : Π i, set (α i)} :
-  pi' μ (pi univ s) ≤ ∏ i, μ i (s i) :=
-begin
-  have hl := λ i : ι, mem_sorted_univ i,
-  have hnd := @sorted_univ_nodup ι _ _,
-  apply ((pi_measurable_equiv_tprod hnd hl).symm.map_apply (pi univ s)).trans_le,
-  dsimp only [pi_measurable_equiv_tprod_symm_apply],
-  rw [elim_preimage_pi hnd],
-  refine (tprod_tprod_le _ _ _).trans_eq _,
-  rw [← list.prod_to_finset _ hnd],
-  congr' with i, simp [hl]
-end
+lemma pi'_pi [∀ i, sigma_finite (μ i)] (s : Π i, set (α i)) : pi' μ (pi univ s) = ∏ i, μ i (s i) :=
+by rw [pi', ← measurable_equiv.pi_measurable_equiv_tprod_symm_apply, measurable_equiv.map_apply,
+  measurable_equiv.pi_measurable_equiv_tprod_symm_apply, elim_preimage_pi, tprod_tprod _ μ,
+  ← list.prod_to_finset, sorted_univ_to_finset]; exact sorted_univ_nodup ι
 
 end encodable
 
@@ -293,15 +266,15 @@ end
 @[irreducible] protected def pi : measure (Π i, α i) :=
 to_measure (outer_measure.pi (λ i, (μ i).to_outer_measure)) (pi_caratheodory μ)
 
-lemma pi_pi [∀ i, sigma_finite (μ i)] (s : Π i, set (α i)) (hs : ∀ i, measurable_set (s i)) :
+lemma pi_pi_aux [∀ i, sigma_finite (μ i)] (s : Π i, set (α i)) (hs : ∀ i, measurable_set (s i)) :
   measure.pi μ (pi univ s) = ∏ i, μ i (s i) :=
 begin
   refine le_antisymm _ _,
   { rw [measure.pi, to_measure_apply _ _ (measurable_set.pi_fintype (λ i _, hs i))],
     apply outer_measure.pi_pi_le },
   { haveI : encodable ι := fintype.encodable ι,
-    rw [← pi'_pi μ hs],
-    simp_rw [← pi'_pi μ hs, measure.pi,
+    rw [← pi'_pi μ s],
+    simp_rw [← pi'_pi μ s, measure.pi,
       to_measure_apply _ _ (measurable_set.pi_fintype (λ i _, hs i)), ← to_outer_measure_apply],
     suffices : (pi' μ).to_outer_measure ≤ outer_measure.pi (λ i, (μ i).to_outer_measure),
     { exact this _ },
@@ -309,48 +282,14 @@ begin
     rw [outer_measure.le_pi],
     intros s hs,
     simp_rw [to_outer_measure_apply],
-    exact pi'_pi_le μ }
+    exact (pi'_pi μ s).le }
 end
 
-lemma pi_univ [∀ i, sigma_finite (μ i)] : measure.pi μ univ = ∏ i, μ i univ :=
-by rw [← pi_univ, pi_pi μ _ (λ i, measurable_set.univ)]
-
-lemma pi_ball [∀ i, sigma_finite (μ i)] [∀ i, metric_space (α i)] [∀ i, borel_space (α i)]
-  (x : Π i, α i) {r : ℝ} (hr : 0 < r) :
-  measure.pi μ (metric.ball x r) = ∏ i, μ i (metric.ball (x i) r) :=
-begin
-  rw [ball_pi _ hr, pi_pi],
-  exact λ i, measurable_set_ball
-end
-
-lemma pi_closed_ball [∀ i, sigma_finite (μ i)] [∀ i, metric_space (α i)] [∀ i, borel_space (α i)]
-  (x : Π i, α i) {r : ℝ} (hr : 0 ≤ r) :
-  measure.pi μ (metric.closed_ball x r) = ∏ i, μ i (metric.closed_ball (x i) r) :=
-begin
-  rw [closed_ball_pi _ hr, pi_pi],
-  exact λ i, measurable_set_closed_ball
-end
-
-lemma pi_unique_eq_map {β : Type*} {m : measurable_space β} (μ : measure β) (α : Type*) [unique α] :
-  measure.pi (λ a : α, μ) = map (measurable_equiv.fun_unique α β).symm μ :=
-begin
-  set e := measurable_equiv.fun_unique α β,
-  have : pi_premeasure (λ _ : α, μ.to_outer_measure) = map e.symm μ,
-  { ext1 s,
-    rw [pi_premeasure, fintype.prod_unique, to_outer_measure_apply, e.symm.map_apply],
-    congr' 1, exact e.to_equiv.image_eq_preimage s },
-  simp only [measure.pi, outer_measure.pi, this, bounded_by_measure, to_outer_measure_to_measure],
-end
-
-lemma map_fun_unique {α β : Type*} [unique α] {m : measurable_space β} (μ : measure β) :
-  map (measurable_equiv.fun_unique α β) (measure.pi $ λ _, μ) = μ :=
-(measurable_equiv.fun_unique α β).map_apply_eq_iff_map_symm_apply_eq.2 (pi_unique_eq_map μ _).symm
-
 variable {μ}
 
 /-- `measure.pi μ` has finite spanning sets in rectangles of finite spanning sets. -/
 def finite_spanning_sets_in.pi {C : Π i, set (set (α i))}
-  (hμ : ∀ i, (μ i).finite_spanning_sets_in (C i)) (hC : ∀ i (s ∈ C i), measurable_set s) :
+  (hμ : ∀ i, (μ i).finite_spanning_sets_in (C i)) :
   (measure.pi μ).finite_spanning_sets_in (pi univ '' pi univ C) :=
 begin
   haveI := λ i, (hμ i).sigma_finite,
@@ -358,8 +297,14 @@ begin
   let e : ℕ → (ι → ℕ) := λ n, (decode (ι → ℕ) n).iget,
   refine ⟨λ n, pi univ (λ i, (hμ i).set (e n i)), λ n, _, λ n, _, _⟩,
   { refine mem_image_of_mem _ (λ i _, (hμ i).set_mem _) },
-  { simp_rw [pi_pi μ (λ i, (hμ i).set (e n i)) (λ i, hC i _ ((hμ i).set_mem _))],
-    exact ennreal.prod_lt_top (λ i _, ((hμ i).finite _).ne) },
+  { calc measure.pi μ (pi univ (λ i, (hμ i).set (e n i)))
+        ≤ measure.pi μ (pi univ (λ i, to_measurable (μ i) ((hμ i).set (e n i)))) :
+      measure_mono (pi_mono $ λ i hi, subset_to_measurable _ _)
+    ... = ∏ i, μ i (to_measurable (μ i) ((hμ i).set (e n i))) :
+      pi_pi_aux μ _ (λ i, measurable_set_to_measurable _ _)
+    ... = ∏ i, μ i ((hμ i).set (e n i)) :
+      by simp only [measure_to_measurable]
+    ... < ∞ : ennreal.prod_lt_top (λ i hi, ((hμ i).finite _).ne) },
   { simp_rw [(surjective_decode_iget (ι → ℕ)).Union_comp (λ x, pi univ (λ i, (hμ i).set (x i))),
       Union_univ_pi (λ i, (hμ i).set), (hμ _).spanning, set.pi_univ] }
 end
@@ -376,13 +321,13 @@ lemma pi_eq_generate_from {C : Π i, set (set (α i))}
 begin
   have h4C : ∀ i (s : set (α i)), s ∈ C i → measurable_set s,
   { intros i s hs, rw [← hC], exact measurable_set_generate_from hs },
-  refine (finite_spanning_sets_in.pi h3C h4C).ext
+  refine (finite_spanning_sets_in.pi h3C).ext
     (generate_from_eq_pi hC (λ i, (h3C i).is_countably_spanning)).symm
     (is_pi_system.pi h2C) _,
   rintro _ ⟨s, hs, rfl⟩,
   rw [mem_univ_pi] at hs,
   haveI := λ i, (h3C i).sigma_finite,
-  simp_rw [h₁ s hs, pi_pi μ s (λ i, h4C i _ (hs i))]
+  simp_rw [h₁ s hs, pi_pi_aux μ s (λ i, h4C i _ (hs i))]
 end
 
 variables [∀ i, sigma_finite (μ i)]
@@ -396,10 +341,46 @@ pi_eq_generate_from (λ i, generate_from_measurable_set)
   (λ i, is_pi_system_measurable_set)
   (λ i, (μ i).to_finite_spanning_sets_in) h
 
-variable (μ)
+variables (μ)
+
+lemma pi'_eq_pi [encodable ι] : pi' μ = measure.pi μ :=
+eq.symm $ pi_eq $ λ s hs, pi'_pi μ s
+
+@[simp] lemma pi_pi (s : Π i, set (α i)) : measure.pi μ (pi univ s) = ∏ i, μ i (s i) :=
+begin
+  haveI : encodable ι := fintype.encodable ι,
+  rw [← pi'_eq_pi, pi'_pi]
+end
+
+lemma pi_univ : measure.pi μ univ = ∏ i, μ i univ := by rw [← pi_univ, pi_pi μ]
+
+lemma pi_ball [∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ}
+  (hr : 0 < r) :
+  measure.pi μ (metric.ball x r) = ∏ i, μ i (metric.ball (x i) r) :=
+by rw [ball_pi _ hr, pi_pi]
+
+lemma pi_closed_ball [∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ}
+  (hr : 0 ≤ r) :
+  measure.pi μ (metric.closed_ball x r) = ∏ i, μ i (metric.closed_ball (x i) r) :=
+by rw [closed_ball_pi _ hr, pi_pi]
+
+lemma pi_unique_eq_map {β : Type*} {m : measurable_space β} (μ : measure β) (α : Type*) [unique α] :
+  measure.pi (λ a : α, μ) = map (measurable_equiv.fun_unique α β).symm μ :=
+begin
+  set e := measurable_equiv.fun_unique α β,
+  have : pi_premeasure (λ _ : α, μ.to_outer_measure) = map e.symm μ,
+  { ext1 s,
+    rw [pi_premeasure, fintype.prod_unique, to_outer_measure_apply, e.symm.map_apply],
+    congr' 1, exact e.to_equiv.image_eq_preimage s },
+  simp only [measure.pi, outer_measure.pi, this, bounded_by_measure, to_outer_measure_to_measure],
+end
+
+lemma map_fun_unique {α β : Type*} [unique α] {m : measurable_space β} (μ : measure β) :
+  map (measurable_equiv.fun_unique α β) (measure.pi $ λ _, μ) = μ :=
+(measurable_equiv.fun_unique α β).map_apply_eq_iff_map_symm_apply_eq.2 (pi_unique_eq_map μ _).symm
 
 instance pi.sigma_finite : sigma_finite (measure.pi μ) :=
-(finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in) (λ _ _, id)).sigma_finite
+(finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in)).sigma_finite
 
 lemma pi_of_empty {α : Type*} [is_empty α] {β : α → Type*} {m : Π a, measurable_space (β a)}
   (μ : Π a : α, measure (β a)) (x : Π a, β a := is_empty_elim) :
@@ -417,7 +398,7 @@ lemma {u} pi_fin_two_eq_map {α : fin 2 → Type u} {m : Π i, measurable_space
 begin
   refine pi_eq (λ s hs, _),
   rw [measurable_equiv.map_apply, fin.prod_univ_succ, fin.prod_univ_succ, fin.prod_univ_zero,
-    mul_one, ← measure.prod_prod (hs _) (hs _)]; [skip, apply_instance],
+    mul_one, ← measure.prod_prod],
   congr' 1,
   ext ⟨a, b⟩,
   simp [fin.forall_fin_succ, is_empty.forall_iff]
@@ -451,9 +432,8 @@ begin
   clear_dependent s,
   /- Now rewrite it as `set.pi`, and apply `pi_pi` -/
   rw [← univ_pi_update_univ, pi_pi],
-  { apply finset.prod_eq_zero (finset.mem_univ i), simp [hμt] },
-  { intro j,
-    rcases em (j = i) with rfl | hj; simp * }
+  apply finset.prod_eq_zero (finset.mem_univ i),
+  simp [hμt]
 end
 
 lemma pi_hyperplane (i : ι) [has_no_atoms (μ i)] (x : α i) :
@@ -549,15 +529,14 @@ lemma pi_has_no_atoms (i : ι) [has_no_atoms (μ i)] :
 instance [h : nonempty ι] [∀ i, has_no_atoms (μ i)] : has_no_atoms (measure.pi μ) :=
 h.elim $ λ i, pi_has_no_atoms i
 
-instance [Π i, topological_space (α i)] [∀ i, opens_measurable_space (α i)]
-  [∀ i, is_locally_finite_measure (μ i)] :
+instance [Π i, topological_space (α i)] [∀ i, is_locally_finite_measure (μ i)] :
   is_locally_finite_measure (measure.pi μ) :=
 begin
   refine ⟨λ x, _⟩,
   choose s hxs ho hμ using λ i, (μ i).exists_is_open_measure_lt_top (x i),
   refine ⟨pi univ s, set_pi_mem_nhds finite_univ (λ i hi, is_open.mem_nhds (ho i) (hxs i)), _⟩,
   rw [pi_pi],
-  exacts [ennreal.prod_lt_top (λ i _, (hμ i).ne), λ i, (ho i).measurable_set]
+  exact ennreal.prod_lt_top (λ i _, (hμ i).ne)
 end
 
 variable (μ)
@@ -585,10 +564,6 @@ begin
   rw [measure.map_apply (measurable_pi_equiv_pi_subtype_prod_symm _ p)
         (measurable_set.univ_pi_fintype hs), A,
       measure.prod_prod, pi_pi, pi_pi, ← fintype.prod_subtype_mul_prod_subtype p (λ i, μ i (s i))],
-  { exact λ i, hs i.1 },
-  { exact λ i, hs i.1 },
-  { exact measurable_set.univ_pi_fintype (λ i, hs i.1) },
-  { exact measurable_set.univ_pi_fintype (λ i, hs i.1) },
 end
 
 lemma map_pi_equiv_pi_subtype_prod (p : ι → Prop) [decidable_pred p] :
@@ -610,18 +585,17 @@ lemma volume_pi [Π i, measure_space (α i)] :
 rfl
 
 lemma volume_pi_pi [Π i, measure_space (α i)] [∀ i, sigma_finite (volume : measure (α i))]
-  (s : Π i, set (α i)) (hs : ∀ i, measurable_set (s i)) :
+  (s : Π i, set (α i)) :
   volume (pi univ s) = ∏ i, volume (s i) :=
-measure.pi_pi (λ i, volume) s hs
+measure.pi_pi (λ i, volume) s
 
 lemma volume_pi_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (volume : measure (α i))]
-  [∀ i, metric_space (α i)] [∀ i, borel_space (α i)] (x : Π i, α i) {r : ℝ} (hr : 0 < r) :
+  [∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ} (hr : 0 < r) :
   volume (metric.ball x r) = ∏ i, volume (metric.ball (x i) r) :=
 measure.pi_ball _ _ hr
 
 lemma volume_pi_closed_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (volume : measure (α i))]
-  [∀ i, metric_space (α i)] [∀ i, borel_space (α i)]
-  (x : Π i, α i) {r : ℝ} (hr : 0 ≤ r) :
+  [∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ} (hr : 0 ≤ r) :
   volume (metric.closed_ball x r) = ∏ i, volume (metric.closed_ball (x i) r) :=
 measure.pi_closed_ball _ _ hr
 
diff --git a/src/measure_theory/constructions/prod.lean b/src/measure_theory/constructions/prod.lean
index 18bcd3e810e5a..9e4aa61261d22 100644
--- a/src/measure_theory/constructions/prod.lean
+++ b/src/measure_theory/constructions/prod.lean
@@ -330,20 +330,36 @@ lemma prod_apply {s : set (α × β)} (hs : measurable_set s) :
 by simp_rw [measure.prod, bind_apply hs measurable.map_prod_mk_left,
   map_apply measurable_prod_mk_left hs]
 
-@[simp] lemma prod_prod {s : set α} {t : set β}
-  (hs : measurable_set s) (ht : measurable_set t) : μ.prod ν (s.prod t) = μ s * ν t :=
-by simp_rw [prod_apply (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
-  lintegral_indicator _ hs, lintegral_const, restrict_apply measurable_set.univ,
-  univ_inter, mul_comm]
-
-/-- If we don't assume measurability of `s` and `t`, we can bound the measure of their product. -/
-lemma prod_prod_le (s : set α) (t : set β) : μ.prod ν (s.prod t) ≤ μ s * ν t :=
-calc μ.prod ν (s.prod t) ≤ μ.prod ν ((to_measurable μ s).prod (to_measurable ν t)) :
-  measure_mono $ set.prod_mono (subset_to_measurable _ _) (subset_to_measurable _ _)
-... = μ (to_measurable μ s) * ν (to_measurable ν t) :
-  prod_prod (measurable_set_to_measurable _ _) (measurable_set_to_measurable _ _)
-... = μ s * ν t :
-  by rw [measure_to_measurable, measure_to_measurable]
+/-- The product measure of the product of two sets is the product of their measures. Note that we
+do not need the sets to be measurable. -/
+@[simp] lemma prod_prod (s : set α) (t : set β) : μ.prod ν (s.prod t) = μ s * ν t :=
+begin
+  apply le_antisymm,
+  { set ST := (to_measurable μ s).prod (to_measurable ν t),
+    have hSTm : measurable_set ST :=
+      (measurable_set_to_measurable _ _).prod (measurable_set_to_measurable _ _),
+    calc μ.prod ν (s.prod t) ≤ μ.prod ν ST :
+      measure_mono $ set.prod_mono (subset_to_measurable _ _) (subset_to_measurable _ _)
+    ... = μ (to_measurable μ s) * ν (to_measurable ν t) :
+      by simp_rw [prod_apply hSTm, mk_preimage_prod_right_eq_if, measure_if,
+        lintegral_indicator _ (measurable_set_to_measurable _ _), lintegral_const,
+        restrict_apply_univ, mul_comm]
+    ... = μ s * ν t : by rw [measure_to_measurable, measure_to_measurable] },
+  { /- Formalization is based on https://mathoverflow.net/a/254134/136589 -/
+    set ST := to_measurable (μ.prod ν) (s.prod t),
+    have hSTm : measurable_set ST := measurable_set_to_measurable _ _,
+    have hST : s.prod t ⊆ ST := subset_to_measurable _ _,
+    set f : α → ℝ≥0∞ := λ x, ν (prod.mk x ⁻¹' ST),
+    have hfm : measurable f := measurable_measure_prod_mk_left hSTm,
+    set s' : set α := {x | ν t ≤ f x},
+    have hss' : s ⊆ s' := λ x hx, measure_mono (λ y hy, hST $ mk_mem_prod hx hy),
+    calc μ s * ν t ≤ μ s' * ν t : mul_le_mul_right' (measure_mono hss') _
+    ... = ∫⁻ x in s', ν t ∂μ    : by rw [set_lintegral_const, mul_comm]
+    ... ≤ ∫⁻ x in s', f x ∂μ    : set_lintegral_mono measurable_const hfm (λ x, id)
+    ... ≤ ∫⁻ x, f x ∂μ          : lintegral_mono' restrict_le_self le_rfl
+    ... = μ.prod ν ST           : (prod_apply hSTm).symm
+    ... = μ.prod ν (s.prod t)   : measure_to_measurable _ }
+end
 
 lemma ae_measure_lt_top {s : set (α × β)} (hs : measurable_set s)
   (h2s : (μ.prod ν) s ≠ ∞) : ∀ᵐ x ∂μ, ν (prod.mk x ⁻¹' s) < ∞ :=
@@ -387,14 +403,13 @@ measure_ae_null_of_prod_null h
 
 /-- `μ.prod ν` has finite spanning sets in rectangles of finite spanning sets. -/
 def finite_spanning_sets_in.prod {ν : measure β} {C : set (set α)} {D : set (set β)}
-  (hμ : μ.finite_spanning_sets_in C) (hν : ν.finite_spanning_sets_in D)
-  (hC : ∀ s ∈ C, measurable_set s) (hD : ∀ t ∈ D, measurable_set t) :
+  (hμ : μ.finite_spanning_sets_in C) (hν : ν.finite_spanning_sets_in D) :
   (μ.prod ν).finite_spanning_sets_in (image2 set.prod C D) :=
 begin
   haveI := hν.sigma_finite,
   refine ⟨λ n, (hμ.set n.unpair.1).prod (hν.set n.unpair.2),
     λ n, mem_image2_of_mem (hμ.set_mem _) (hν.set_mem _), λ n, _, _⟩,
-  { simp_rw [prod_prod (hC _ (hμ.set_mem _)) (hD _ (hν.set_mem _))],
+  { rw [prod_prod],
     exact mul_lt_top (hμ.finite _).ne (hν.finite _).ne },
   { simp_rw [Union_unpair_prod, hμ.spanning, hν.spanning, univ_prod_univ] }
 end
@@ -402,21 +417,19 @@ end
 lemma prod_fst_absolutely_continuous : map prod.fst (μ.prod ν) ≪ μ :=
 begin
   refine absolutely_continuous.mk (λ s hs h2s, _),
-  simp_rw [map_apply measurable_fst hs, ← prod_univ, prod_prod hs measurable_set.univ],
-  rw [h2s, zero_mul] -- for some reason `simp_rw [h2s]` doesn't work
+  rw [map_apply measurable_fst hs, ← prod_univ, prod_prod, h2s, zero_mul],
 end
 
 lemma prod_snd_absolutely_continuous : map prod.snd (μ.prod ν) ≪ ν :=
 begin
   refine absolutely_continuous.mk (λ s hs h2s, _),
-  simp_rw [map_apply measurable_snd hs, ← univ_prod, prod_prod measurable_set.univ hs],
-  rw [h2s, mul_zero] -- for some reason `simp_rw [h2s]` doesn't work
+  rw [map_apply measurable_snd hs, ← univ_prod, prod_prod, h2s, mul_zero]
 end
 
 variables [sigma_finite μ]
 
 instance prod.sigma_finite : sigma_finite (μ.prod ν) :=
-(μ.to_finite_spanning_sets_in.prod ν.to_finite_spanning_sets_in (λ _, id) (λ _, id)).sigma_finite
+(μ.to_finite_spanning_sets_in.prod ν.to_finite_spanning_sets_in).sigma_finite
 
 /-- A measure on a product space equals the product measure if they are equal on rectangles
   with as sides sets that generate the corresponding σ-algebras. -/
@@ -427,15 +440,11 @@ lemma prod_eq_generate_from {μ : measure α} {ν : measure β} {C : set (set α
   {μν : measure (α × β)}
   (h₁ : ∀ (s ∈ C) (t ∈ D), μν (set.prod s t) = μ s * ν t) : μ.prod ν = μν :=
 begin
-  have h4C : ∀ (s : set α), s ∈ C → measurable_set s,
-  { intros s hs, rw [← hC], exact measurable_set_generate_from hs },
-  have h4D : ∀ (t : set β), t ∈ D → measurable_set t,
-  { intros t ht, rw [← hD], exact measurable_set_generate_from ht },
-  refine (h3C.prod h3D h4C h4D).ext
+  refine (h3C.prod h3D).ext
     (generate_from_eq_prod hC hD h3C.is_countably_spanning h3D.is_countably_spanning).symm
     (h2C.prod h2D) _,
   { rintro _ ⟨s, t, hs, ht, rfl⟩, haveI := h3D.sigma_finite,
-    simp_rw [h₁ s hs t ht, prod_prod (h4C s hs) (h4D t ht)] }
+    rw [h₁ s hs t ht, prod_prod] }
 end
 
 /-- A measure on a product space equals the product measure if they are equal on rectangles. -/
@@ -449,7 +458,7 @@ lemma prod_swap : map prod.swap (μ.prod ν) = ν.prod μ :=
 begin
   refine (prod_eq _).symm,
   intros s t hs ht,
-  simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod ht hs, mul_comm]
+  simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod, mul_comm]
 end
 
 lemma prod_apply_symm {s : set (α × β)} (hs : measurable_set s) :
@@ -462,29 +471,28 @@ lemma prod_assoc_prod [sigma_finite τ] :
 begin
   refine (prod_eq_generate_from generate_from_measurable_set generate_from_prod
     is_pi_system_measurable_set is_pi_system_prod μ.to_finite_spanning_sets_in
-    (ν.to_finite_spanning_sets_in.prod τ.to_finite_spanning_sets_in (λ _, id) (λ _, id)) _).symm,
+    (ν.to_finite_spanning_sets_in.prod τ.to_finite_spanning_sets_in) _).symm,
   rintro s hs _ ⟨t, u, ht, hu, rfl⟩, rw [mem_set_of_eq] at hs ht hu,
-  simp_rw [map_apply (measurable_equiv.measurable _) (hs.prod (ht.prod hu)), prod_prod ht hu,
+  simp_rw [map_apply (measurable_equiv.measurable _) (hs.prod (ht.prod hu)),
     measurable_equiv.prod_assoc, measurable_equiv.coe_mk, equiv.prod_assoc_preimage,
-    prod_prod (hs.prod ht) hu, prod_prod hs ht, mul_assoc]
+    prod_prod, mul_assoc]
 end
 
 /-! ### The product of specific measures -/
 
-lemma prod_restrict {s : set α} {t : set β} (hs : measurable_set s) (ht : measurable_set t) :
+lemma prod_restrict (s : set α) (t : set β) :
   (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s.prod t) :=
 begin
   refine prod_eq (λ s' t' hs' ht', _),
-  simp_rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod (hs'.inter hs) (ht'.inter ht),
-    restrict_apply hs', restrict_apply ht']
+  rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
+    restrict_apply ht']
 end
 
-lemma restrict_prod_eq_prod_univ {s : set α} (hs : measurable_set s) :
+lemma restrict_prod_eq_prod_univ (s : set α) :
   (μ.restrict s).prod ν = (μ.prod ν).restrict (s.prod univ) :=
 begin
   have : ν = ν.restrict set.univ := measure.restrict_univ.symm,
   rwa [this, measure.prod_restrict, ← this],
-  exact measurable_set.univ,
 end
 
 lemma prod_dirac (y : β) : μ.prod (dirac y) = map (λ x, (x, y)) μ :=
@@ -508,21 +516,21 @@ lemma prod_sum {ι : Type*} [fintype ι] (ν : ι → measure β) [∀ i, sigma_
   μ.prod (sum ν) = sum (λ i, μ.prod (ν i)) :=
 begin
   refine prod_eq (λ s t hs ht, _),
-  simp_rw [sum_apply _ (hs.prod ht), sum_apply _ ht, prod_prod hs ht, tsum_fintype, finset.mul_sum]
+  simp_rw [sum_apply _ (hs.prod ht), sum_apply _ ht, prod_prod, ennreal.tsum_mul_left]
 end
 
 lemma sum_prod {ι : Type*} [fintype ι] (μ : ι → measure α) [∀ i, sigma_finite (μ i)] :
   (sum μ).prod ν = sum (λ i, (μ i).prod ν) :=
 begin
   refine prod_eq (λ s t hs ht, _),
-  simp_rw [sum_apply _ (hs.prod ht), sum_apply _ hs, prod_prod hs ht, tsum_fintype, finset.sum_mul]
+  simp_rw [sum_apply _ (hs.prod ht), sum_apply _ hs, prod_prod, ennreal.tsum_mul_right]
 end
 
 lemma prod_add (ν' : measure β) [sigma_finite ν'] : μ.prod (ν + ν') = μ.prod ν + μ.prod ν' :=
-by { refine prod_eq (λ s t hs ht, _), simp_rw [add_apply, prod_prod hs ht, left_distrib] }
+by { refine prod_eq (λ s t hs ht, _), simp_rw [add_apply, prod_prod, left_distrib] }
 
 lemma add_prod (μ' : measure α) [sigma_finite μ'] : (μ + μ').prod ν = μ.prod ν + μ'.prod ν :=
-by { refine prod_eq (λ s t hs ht, _), simp_rw [add_apply, prod_prod hs ht, right_distrib] }
+by { refine prod_eq (λ s t hs ht, _), simp_rw [add_apply, prod_prod, right_distrib] }
 
 @[simp] lemma zero_prod (ν : measure β) : (0 : measure α).prod ν = 0 :=
 by { rw measure.prod, exact bind_zero_left _ }
@@ -538,7 +546,7 @@ begin
   haveI := hgc.of_map μc hg,
   refine prod_eq (λ s t hs ht, _),
   rw [map_apply (hf.prod_map hg) (hs.prod ht), map_apply hf hs, map_apply hg ht],
-  exact prod_prod (hf hs) (hg ht)
+  exact prod_prod (f ⁻¹' s) (g ⁻¹' t)
 end
 
 end measure
@@ -957,4 +965,13 @@ lemma integral_integral_swap ⦃f : α → β → E⦄ (hf : integrable (uncurry
   ∫ x, ∫ y, f x y ∂ν ∂μ = ∫ y, ∫ x, f x y ∂μ ∂ν :=
 (integral_integral hf).trans (integral_prod_symm _ hf)
 
+/-- **Fubini's Theorem** for set integrals. -/
+lemma set_integral_prod (f : α × β → E) {s : set α} {t : set β}
+  (hf : integrable_on f (s.prod t) (μ.prod ν)) :
+  ∫ z in s.prod t, f z ∂(μ.prod ν) = ∫ x in s, ∫ y in t, f (x, y) ∂ν ∂μ :=
+begin
+  simp only [← measure.prod_restrict s t, integrable_on] at hf ⊢,
+  exact integral_prod f hf
+end
+
 end measure_theory
diff --git a/src/measure_theory/group/arithmetic.lean b/src/measure_theory/group/arithmetic.lean
index 16ad5f677f1d2..cc22009185d5a 100644
--- a/src/measure_theory/group/arithmetic.lean
+++ b/src/measure_theory/group/arithmetic.lean
@@ -44,7 +44,7 @@ measurable function, arithmetic operator
 
 universes u v
 
-open_locale big_operators
+open_locale big_operators pointwise
 open measure_theory
 
 /-!
@@ -338,6 +338,9 @@ measurable_inv.comp_ae_measurable hf
 
 attribute [measurability] measurable.neg ae_measurable.neg
 
+@[to_additive] lemma measurable_set.inv {s : set G} (hs : measurable_set s) : measurable_set s⁻¹ :=
+measurable_inv hs
+
 @[simp, to_additive] lemma measurable_inv_iff {G : Type*} [group G] [measurable_space G]
   [has_measurable_inv G] {f : α → G} : measurable (λ x, (f x)⁻¹) ↔ measurable f :=
 ⟨λ h, by simpa only [inv_inv] using h.inv, λ h, h.inv⟩
diff --git a/src/measure_theory/group/prod.lean b/src/measure_theory/group/prod.lean
index 00391d3a2af22..3f81d54b9d0bc 100644
--- a/src/measure_theory/group/prod.lean
+++ b/src/measure_theory/group/prod.lean
@@ -35,7 +35,7 @@ https://math.stackexchange.com/questions/3974485/does-right-translation-preserve
 
 noncomputable theory
 open topological_space set (hiding prod_eq) function
-open_locale classical ennreal
+open_locale classical ennreal pointwise
 
 namespace measure_theory
 
@@ -105,28 +105,27 @@ begin
     map_prod_inv_mul_eq_swap hν]
 end
 
-@[to_additive]
-lemma measure_null_of_measure_inv_null (hμ : is_mul_left_invariant μ)
-  {E : set G} (hE : measurable_set E) (h2E : μ ((λ x, x⁻¹) ⁻¹' E) = 0) : μ E = 0 :=
+@[to_additive] lemma quasi_measure_preserving_inv (hμ : is_mul_left_invariant μ) :
+  quasi_measure_preserving (has_inv.inv : G → G) μ μ :=
 begin
+  refine ⟨measurable_inv, absolutely_continuous.mk $ λ s hsm hμs, _⟩,
+  rw [map_apply measurable_inv hsm, inv_preimage],
   have hf : measurable (λ z : G × G, (z.2 * z.1, z.1⁻¹)) :=
-  (measurable_snd.mul measurable_fst).prod_mk measurable_fst.inv,
-  suffices : map (λ z : G × G, (z.2 * z.1, z.1⁻¹)) (μ.prod μ) (E.prod E) = 0,
-  { simpa only [map_prod_mul_inv_eq hμ hμ, prod_prod hE hE, mul_eq_zero, or_self] using this },
-  simp_rw [map_apply hf (hE.prod hE), prod_apply_symm (hf (hE.prod hE)), preimage_preimage,
-    mk_preimage_prod],
-  convert lintegral_zero, ext1 x, refine measure_mono_null (inter_subset_right _ _) h2E
+    (measurable_snd.mul measurable_fst).prod_mk measurable_fst.inv,
+  suffices : map (λ z : G × G, (z.2 * z.1, z.1⁻¹)) (μ.prod μ) ((s⁻¹).prod s⁻¹) = 0,
+  { simpa only [map_prod_mul_inv_eq hμ hμ, prod_prod, mul_eq_zero, or_self] using this },
+  have hsm' : measurable_set (s⁻¹.prod s⁻¹) := hsm.inv.prod hsm.inv,
+  simp_rw [map_apply hf hsm', prod_apply_symm (hf hsm'), preimage_preimage, mk_preimage_prod,
+    inv_preimage, set.inv_inv, measure_mono_null (inter_subset_right _ _) hμs, lintegral_zero]
 end
 
 @[to_additive]
-lemma measure_inv_null (hμ : is_mul_left_invariant μ) {E : set G} (hE : measurable_set E) :
+lemma measure_inv_null (hμ : is_mul_left_invariant μ) {E : set G} :
   μ ((λ x, x⁻¹) ⁻¹' E) = 0 ↔ μ E = 0 :=
 begin
-  refine ⟨measure_null_of_measure_inv_null hμ hE, _⟩,
-  intro h2E,
-  apply measure_null_of_measure_inv_null hμ (measurable_inv hE),
-  convert h2E using 2,
-  exact set.inv_inv
+  refine ⟨λ hE, _, (quasi_measure_preserving_inv hμ).preimage_null⟩,
+  convert (quasi_measure_preserving_inv hμ).preimage_null hE,
+  exact set.inv_inv.symm
 end
 
 @[to_additive]
@@ -156,18 +155,16 @@ begin
 end
 
 @[to_additive]
-lemma measure_mul_right_null (hμ : is_mul_left_invariant μ) {E : set G} (hE : measurable_set E)
-  (y : G) : μ ((λ x, x * y) ⁻¹' E) = 0 ↔ μ E = 0 :=
-begin
-  rw [← measure_inv_null hμ hE, ← hμ y⁻¹ (measurable_inv hE),
-    ← measure_inv_null hμ (measurable_mul_const y hE)],
-  convert iff.rfl using 3, ext x, simp,
-end
+lemma measure_mul_right_null (hμ : is_mul_left_invariant μ) {E : set G} (y : G) :
+  μ ((λ x, x * y) ⁻¹' E) = 0 ↔ μ E = 0 :=
+calc μ ((λ x, x * y) ⁻¹' E) = 0 ↔ μ (has_inv.inv ⁻¹' ((λ x, y⁻¹ * x) ⁻¹' (has_inv.inv ⁻¹' E))) = 0 :
+  by simp only [preimage_preimage, mul_inv_rev, inv_inv]
+... ↔ μ E = 0 : by simp only [measure_inv_null hμ, hμ.measure_preimage_mul]
 
 @[to_additive]
-lemma measure_mul_right_ne_zero (hμ : is_mul_left_invariant μ) {E : set G} (hE : measurable_set E)
+lemma measure_mul_right_ne_zero (hμ : is_mul_left_invariant μ) {E : set G}
   (h2E : μ E ≠ 0) (y : G) : μ ((λ x, x * y) ⁻¹' E) ≠ 0 :=
-(not_iff_not_of_iff (measure_mul_right_null hμ hE y)).mpr h2E
+(not_iff_not_of_iff (measure_mul_right_null hμ y)).mpr h2E
 
 /-- A technical lemma relating two different measures. This is basically [Halmos, §60 Th. A].
   Note that if `f` is the characteristic function of a measurable set `F` this states that
@@ -203,7 +200,7 @@ begin
     λ y, (regular.lt_top_of_is_compact $ (homeomorph.mul_right _).compact_preimage.mpr hE).ne,
   simp_rw [this, lintegral_mul_const _ (mE _), lintegral_indicator _ (measurable_mul_const _ Em),
     set_lintegral_one, g, inv_inv,
-    ennreal.mul_div_cancel' (measure_mul_right_ne_zero hν Em h2E _) (h3E _)]
+    ennreal.mul_div_cancel' (measure_mul_right_ne_zero hν h2E _) (h3E _)]
 end
 
 /-- This is roughly the uniqueness (up to a scalar) of left invariant Borel measures on a second
diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
index a729523e2559b..f9dcea1a6b9d1 100644
--- a/src/measure_theory/measure/haar_lebesgue.lean
+++ b/src/measure_theory/measure/haar_lebesgue.lean
@@ -73,7 +73,7 @@ lemma add_haar_measure_eq_volume_pi (ι : Type*) [fintype ι] :
   add_haar_measure (pi_Icc01 ι) = volume :=
 begin
   convert (add_haar_measure_unique _ (pi_Icc01 ι)).symm,
-  { simp only [pi_Icc01, volume_pi_pi (λ i, Icc (0 : ℝ) 1) (λ (i : ι), measurable_set_Icc),
+  { simp only [pi_Icc01, volume_pi_pi (λ i, Icc (0 : ℝ) 1),
       finset.prod_const_one, ennreal.of_real_one, real.volume_Icc, one_smul, sub_zero] },
   { apply_instance },
   { exact is_add_left_invariant_real_volume_pi ι }
diff --git a/src/measure_theory/measure/hausdorff.lean b/src/measure_theory/measure/hausdorff.lean
index c6278be73ab70..adfd81ecef870 100644
--- a/src/measure_theory/measure/hausdorff.lean
+++ b/src/measure_theory/measure/hausdorff.lean
@@ -687,7 +687,7 @@ begin
     { refine le_hausdorff_measure _ _ ∞ ennreal.coe_lt_top (λ s h₁ h₂, _),
       rw [ennreal.rpow_nat_cast],
       exact real.volume_pi_le_diam_pow s },
-    rw [← volume_pi_pi (λ i, Ioo (a i : ℝ) (b i)) (λ i, measurable_set_Ioo)],
+    rw [← volume_pi_pi (λ i, Ioo (a i : ℝ) (b i))],
     exact measure.le_iff'.1 Hle _ },
   /- For the other inequality `μH s ≤ volume s`, we use a covering of `s` by sets of small diameter
   `1/n`, namely cubes with left-most point of the form `a i + f i / n` with `f i` ranging between
diff --git a/src/measure_theory/measure/lebesgue.lean b/src/measure_theory/measure/lebesgue.lean
index c6977362895d1..802587d7ec823 100644
--- a/src/measure_theory/measure/lebesgue.lean
+++ b/src/measure_theory/measure/lebesgue.lean
@@ -138,8 +138,7 @@ instance is_finite_measure_restrict_Ioo (x y : ℝ) : is_finite_measure (volume.
 lemma volume_Icc_pi {a b : ι → ℝ} : volume (Icc a b) = ∏ i, ennreal.of_real (b i - a i) :=
 begin
   rw [← pi_univ_Icc, volume_pi_pi],
-  { simp only [real.volume_Icc] },
-  { exact λ i, measurable_set_Icc }
+  simp only [real.volume_Icc]
 end
 
 @[simp] lemma volume_Icc_pi_to_real {a b : ι → ℝ} (h : a ≤ b) :
@@ -197,7 +196,7 @@ lemma volume_pi_le_prod_diam (s : set (ι → ℝ)) :
 calc volume s ≤ volume (pi univ (λ i, closure (function.eval i '' s))) :
   volume.mono $ subset.trans (subset_pi_eval_image univ s) $ pi_mono $ λ i hi, subset_closure
           ... = ∏ i, volume (closure $ function.eval i '' s) :
-  volume_pi_pi _ $ λ i, measurable_set_closure
+  volume_pi_pi _
           ... ≤ ∏ i : ι, emetric.diam (function.eval i '' s) :
   finset.prod_le_prod' $ λ i hi, (volume_le_diam _).trans_eq (emetric.diam_closure _)
 
@@ -286,8 +285,7 @@ begin
     = set.pi univ (λ (i : ι), ((+) (a i)) ⁻¹' (s i)), by { ext, simp },
   rw [measure.map_apply (measurable_const_add a) (measurable_set.univ_pi_fintype hs), A,
       volume_pi_pi],
-  { simp only [volume_preimage_add_left] },
-  { exact λ i, measurable_const_add (a i) (hs i) }
+  simp only [volume_preimage_add_left]
 end
 
 @[simp] lemma volume_pi_preimage_add_left (a : ι → ℝ) (s : set (ι → ℝ)) :
@@ -322,8 +320,7 @@ begin
       mul_inv_cancel A, abs_one, ennreal.of_real_one, one_mul] },
   rw [this, volume_pi_pi, finset.abs_prod,
     ennreal.of_real_prod_of_nonneg (λ i hi, abs_nonneg (D i)), ← finset.prod_mul_distrib],
-  { simp only [B] },
-  { exact λ i, measurable_const_mul _ (hs i) },
+  simp only [B]
 end
 
 /-- A transvection preserves Lebesgue measure. -/
@@ -493,11 +490,11 @@ begin
       ← volume_region_between_eq_lintegral' hf.measurable_mk hg.measurable_mk hs],
   convert h₂ using 1,
   { rw measure.restrict_prod_eq_prod_univ,
-    exacts [ (measure.restrict_eq_self' (hs.prod measurable_set.univ)
-      (region_between_subset f g s)).symm, hs], },
+    exact (measure.restrict_eq_self' (hs.prod measurable_set.univ)
+      (region_between_subset f g s)).symm, },
   { rw measure.restrict_prod_eq_prod_univ,
-    exacts [(measure.restrict_eq_self' (hs.prod measurable_set.univ)
-      (region_between_subset (ae_measurable.mk f hf) (ae_measurable.mk g hg) s)).symm, hs] },
+    exact (measure.restrict_eq_self' (hs.prod measurable_set.univ)
+      (region_between_subset (ae_measurable.mk f hf) (ae_measurable.mk g hg) s)).symm },
 end
 
 
diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean
index a1ee44b64921c..6ed21c16bd078 100644
--- a/src/measure_theory/measure/measure_space.lean
+++ b/src/measure_theory/measure/measure_space.lean
@@ -1415,6 +1415,10 @@ lemma ae_eq (h : quasi_measure_preserving f μa μb) {g₁ g₂ : β → δ} (hg
   g₁ ∘ f =ᵐ[μa] g₂ ∘ f :=
 h.ae hg
 
+lemma preimage_null (h : quasi_measure_preserving f μa μb) {s : set β} (hs : μb s = 0) :
+  μa (f ⁻¹' s) = 0 :=
+preimage_null_of_map_null h.1 (h.2 hs)
+
 end quasi_measure_preserving
 
 /-! ### The `cofinite` filter -/