feat(measure_theory/integral/bochner): prove set_integral_eq_subtype (

#10858)

Relate integral w.r.t. `μ.restrict s` and w.r.t. `comap (coe : s → α) μ`.

src/measure_theory/integral/bochner.lean

@@ -1313,6 +1313,11 @@ lemma measure_preserving.integral_comp {β} {_ : measurable_space β} {f : α 
   ∫ x, g (f x) ∂μ = ∫ y, g y ∂ν :=
 h₁.map_eq ▸ (h₂.integral_map g).symm
 
+lemma set_integral_eq_subtype {α} [measure_space α] {s : set α} (hs : measurable_set s)
+  (f : α → E) :
+  ∫ x in s, f x = ∫ x : s, f x :=
+by { rw ← map_comap_subtype_coe hs,  exact (measurable_embedding.subtype_coe hs).integral_map _ }
+
 @[simp] lemma integral_dirac' [measurable_space α] (f : α → E) (a : α) (hfm : measurable f) :
   ∫ x, f x ∂(measure.dirac a) = f a :=
 calc ∫ x, f x ∂(measure.dirac a) = ∫ x, f a ∂(measure.dirac a) :