feat: a function with vanishing integral against smooth functions sup…

…ported in U is ae zero in U (#8805)

A stronger version of #8800, the differences are:

+ assume either `IsSigmaCompact U` or `SigmaCompactSpace M`;

+ only need test functions satisfying `tsupport g ⊆ U` rather than `support g ⊆ U`;

+ requires `LocallyIntegrableOn` U rather than `LocallyIntegrable` on the whole space.

Also fills in some missing APIs around the manifold and measure theory libraries.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Algebra/Support.lean

@@ -90,6 +90,22 @@ theorem mulSupport_eq_iff {f : α → M} {s : Set α} :
 #align function.mul_support_eq_iff Function.mulSupport_eq_iff
 #align function.support_eq_iff Function.support_eq_iff
 
+@[to_additive]
+theorem mulSupport_extend_one_subset {f : α → M} {g : α → N} :
+    mulSupport (f.extend g 1) ⊆ f '' mulSupport g :=
+  mulSupport_subset_iff'.mpr fun x hfg ↦ by
+    by_cases hf : ∃ a, f a = x
+    · rw [extend, dif_pos hf, ← nmem_mulSupport]
+      rw [← Classical.choose_spec hf] at hfg
+      exact fun hg ↦ hfg ⟨_, hg, rfl⟩
+    · rw [extend_apply' _ _ _ hf]; rfl
+
+@[to_additive]
+theorem mulSupport_extend_one {f : α → M} {g : α → N} (hf : f.Injective) :
+    mulSupport (f.extend g 1) = f '' mulSupport g :=
+  mulSupport_extend_one_subset.antisymm <| by
+    rintro _ ⟨x, hx, rfl⟩; rwa [mem_mulSupport, hf.extend_apply]
+
 @[to_additive]
 theorem mulSupport_disjoint_iff {f : α → M} {s : Set α} :
     Disjoint (mulSupport f) s ↔ EqOn f 1 s := by

Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

@@ -38,7 +38,7 @@ variable {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
 /-- If a locally integrable function `f` on a finite-dimensional real manifold has zero integral
 when multiplied by any smooth compactly supported function, then `f` vanishes almost everywhere. -/
 theorem ae_eq_zero_of_integral_smooth_smul_eq_zero (hf : LocallyIntegrable f μ)
-    (h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ) g → HasCompactSupport g → ∫ x, g x • f x ∂μ = 0) :
+    (h : ∀ g : M → ℝ, Smooth I 𝓘(ℝ) g → HasCompactSupport g → ∫ x, g x • f x ∂μ = 0) :
     ∀ᵐ x ∂μ, f x = 0 := by
   -- record topological properties of `M`
   have := I.locallyCompactSpace
@@ -110,6 +110,46 @@ theorem ae_eq_zero_of_integral_smooth_smul_eq_zero (hf : LocallyIntegrable f μ)
     simpa [g_supp] using vK n
   simpa [this] using L
 
+
+/-- If a function `f` locally integrable on an open subset `U` of a finite-dimensional real
+  manifold has zero integral when multiplied by any smooth function compactly supported
+  in `U`, then `f` vanishes almost everywhere in `U`. -/
+nonrec theorem IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero' {U : Set M} (hU : IsOpen U)
+    (hSig : IsSigmaCompact U) (hf : LocallyIntegrableOn f U μ)
+    (h : ∀ g : M → ℝ,
+      Smooth I 𝓘(ℝ) g → HasCompactSupport g → tsupport g ⊆ U → ∫ x, g x • f x ∂μ = 0) :
+    ∀ᵐ x ∂μ, x ∈ U → f x = 0 := by
+  have meas_U := hU.measurableSet
+  rw [← ae_restrict_iff' meas_U, ae_restrict_iff_subtype meas_U]
+  let U : Opens M := ⟨U, hU⟩
+  change ∀ᵐ (x : U) ∂_, _
+  haveI : SigmaCompactSpace U := isSigmaCompact_iff_sigmaCompactSpace.mp hSig
+  refine ae_eq_zero_of_integral_smooth_smul_eq_zero I ?_ fun g g_smth g_supp ↦ ?_
+  · exact (locallyIntegrable_comap meas_U).mpr hf
+  specialize h (Subtype.val.extend g 0) (g_smth.extend_zero g_supp)
+    (g_supp.extend_zero continuous_subtype_val) ((g_supp.tsupport_extend_zero_subset
+      continuous_subtype_val).trans <| Subtype.coe_image_subset _ _)
+  rw [← set_integral_eq_integral_of_forall_compl_eq_zero (s := U) fun x hx ↦ ?_] at h
+  · rw [← integral_subtype_comap] at h
+    · simp_rw [Subtype.val_injective.extend_apply] at h; exact h
+    · exact meas_U
+  rw [Function.extend_apply' _ _ _ (mt _ hx)]
+  · apply zero_smul
+  · rintro ⟨x, rfl⟩; exact x.2
+
+theorem IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero {U : Set M} (hU : IsOpen U)
+    (hf : LocallyIntegrableOn f U μ)
+    (h : ∀ g : M → ℝ,
+      Smooth I 𝓘(ℝ) g → HasCompactSupport g → tsupport g ⊆ U → ∫ x, g x • f x ∂μ = 0) :
+    ∀ᵐ x ∂μ, x ∈ U → f x = 0 :=
+  haveI := I.locallyCompactSpace
+  haveI := ChartedSpace.locallyCompactSpace H M
+  haveI := hU.locallyCompactSpace
+  haveI := I.secondCountableTopology
+  haveI := ChartedSpace.secondCountable_of_sigma_compact H M
+  hU.ae_eq_zero_of_integral_smooth_smul_eq_zero' _
+    (isSigmaCompact_iff_sigmaCompactSpace.mpr inferInstance) hf h
+
 /-- If two locally integrable functions on a finite-dimensional real manifold have the same integral
 when multiplied by any smooth compactly supported function, then they coincide almost everywhere. -/
 theorem ae_eq_of_integral_smooth_smul_eq
@@ -151,4 +191,15 @@ theorem ae_eq_of_integral_contDiff_smul_eq
   ae_eq_of_integral_smooth_smul_eq 𝓘(ℝ, E) hf hf'
     (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)
 
+/-- If a function `f` locally integrable on an open subset `U` of a finite-dimensional real
+  manifold has zero integral when multiplied by any smooth function compactly supported
+  in an open set `U`, then `f` vanishes almost everywhere in `U`. -/
+theorem IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero {U : Set E} (hU : IsOpen U)
+    (hf : LocallyIntegrableOn f U μ)
+    (h : ∀ (g : E → ℝ), ContDiff ℝ ⊤ g → HasCompactSupport g → tsupport g ⊆ U →
+        ∫ x, g x • f x ∂μ = 0) :
+    ∀ᵐ x ∂μ, x ∈ U → f x = 0 :=
+  hU.ae_eq_zero_of_integral_smooth_smul_eq_zero 𝓘(ℝ, E) hf
+    (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)
+
 end VectorSpace

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -1162,6 +1162,17 @@ protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G
     · exact isOpen_inter_preimage_symm (chartAt _ _) s.2
 #align topological_space.opens.has_groupoid TopologicalSpace.Opens.instHasGroupoid
 
+theorem chartAt_subtype_val_symm_eventuallyEq (U : Opens M) {x : U} :
+    (chartAt H x.val).symm =ᶠ[𝓝 (chartAt H x.val x.val)] Subtype.val ∘ (chartAt H x).symm := by
+  set i : U → M := Subtype.val
+  set e := chartAt H x.val
+  haveI : Nonempty U := ⟨x⟩
+  haveI : Nonempty M := ⟨i x⟩
+  have heUx_nhds : (e.subtypeRestr U).target ∈ 𝓝 (e x) := by
+    apply (e.subtypeRestr U).open_target.mem_nhds
+    exact e.map_subtype_source (mem_chart_source _ _)
+  exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn U)
+
 theorem chartAt_inclusion_symm_eventuallyEq {U V : Opens M} (hUV : U ≤ V) {x : U} :
     (chartAt H (Set.inclusion hUV x)).symm
     =ᶠ[𝓝 (chartAt H (Set.inclusion hUV x) (Set.inclusion hUV x))]

Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

@@ -353,6 +353,24 @@ section Inclusion
 
 open TopologicalSpace
 
+theorem contMdiffAt_subtype_iff {n : ℕ∞} {U : Opens M} {f : M → M'} {x : U} :
+    ContMDiffAt I I' n (fun x : U ↦ f x) x ↔ ContMDiffAt I I' n f x :=
+  ((contDiffWithinAt_localInvariantProp I I' n).liftPropAt_iff_comp_subtype_val _ _).symm
+
+theorem contMDiff_subtype_val {n : ℕ∞} {U : Opens M} : ContMDiff I I n (Subtype.val : U → M) :=
+  fun _ ↦ contMdiffAt_subtype_iff.mpr contMDiffAt_id
+
+@[to_additive]
+theorem ContMDiff.extend_one [T2Space M] [One M'] {n : ℕ∞} {U : Opens M} {f : U → M'}
+    (supp : HasCompactMulSupport f) (diff : ContMDiff I I' n f) :
+    ContMDiff I I' n (Subtype.val.extend f 1) := fun x ↦ by
+  by_cases h : x ∈ mulTSupport (Subtype.val.extend f 1)
+  · rw [show x = ↑(⟨x, Subtype.coe_image_subset _ _
+      (supp.mulTSupport_extend_one_subset continuous_subtype_val h)⟩ : U) by rfl,
+      ← contMdiffAt_subtype_iff, ← comp_def, extend_comp Subtype.val_injective]
+    exact diff.contMDiffAt
+  · exact contMDiffAt_const.congr_of_eventuallyEq (not_mem_mulTSupport_iff_eventuallyEq.mp h)
+
 theorem contMDiff_inclusion {n : ℕ∞} {U V : Opens M} (h : U ≤ V) :
     ContMDiff I I n (Set.inclusion h : U → V) := by
   rintro ⟨x, hx : x ∈ U⟩
@@ -365,6 +383,16 @@ theorem contMDiff_inclusion {n : ℕ∞} {U V : Opens M} (h : U ≤ V) :
   · exact congr_arg I (I.left_inv y)
 #align cont_mdiff_inclusion contMDiff_inclusion
 
+theorem smooth_subtype_iff {U : Opens M} {f : M → M'} {x : U} :
+    SmoothAt I I' (fun x : U ↦ f x) x ↔ SmoothAt I I' f x := contMdiffAt_subtype_iff
+
+theorem smooth_subtype_val {U : Opens M} : Smooth I I (Subtype.val : U → M) := contMDiff_subtype_val
+
+@[to_additive]
+theorem Smooth.extend_one [T2Space M] [One M'] {U : Opens M} {f : U → M'}
+    (supp : HasCompactMulSupport f) (diff : Smooth I I' f) :
+    Smooth I I' (Subtype.val.extend f 1) := ContMDiff.extend_one supp diff
+
 theorem smooth_inclusion {U V : Opens M} (h : U ≤ V) : Smooth I I (Set.inclusion h : U → V) :=
   contMDiff_inclusion h
 #align smooth_inclusion smooth_inclusion

Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

@@ -542,17 +542,33 @@ theorem liftProp_id (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) :
   exact fun x ↦ hG.congr' ((chartAt H x).eventually_right_inverse <| mem_chart_target H x) (hQ _)
 #align structure_groupoid.local_invariant_prop.lift_prop_id StructureGroupoid.LocalInvariantProp.liftProp_id
 
+theorem liftPropAt_iff_comp_subtype_val (hG : LocalInvariantProp G G' P) {U : Opens M}
+    (f : M → M') (x : U) :
+    LiftPropAt P f x ↔ LiftPropAt P (f ∘ Subtype.val) x := by
+  congrm ?_ ∧ ?_
+  · simp_rw [continuousWithinAt_univ, U.openEmbedding'.continuousAt_iff]
+  · apply hG.congr_iff
+    exact (U.chartAt_subtype_val_symm_eventuallyEq).fun_comp (chartAt H' (f x) ∘ f)
+
 theorem liftPropAt_iff_comp_inclusion (hG : LocalInvariantProp G G' P) {U V : Opens M} (hUV : U ≤ V)
     (f : V → M') (x : U) :
     LiftPropAt P f (Set.inclusion hUV x) ↔ LiftPropAt P (f ∘ Set.inclusion hUV : U → M') x := by
   congrm ?_ ∧ ?_
-  · simp [continuousWithinAt_univ,
+  · simp_rw [continuousWithinAt_univ,
       (TopologicalSpace.Opens.openEmbedding_of_le hUV).continuousAt_iff]
   · apply hG.congr_iff
     exact (TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq hUV).fun_comp
       (chartAt H' (f (Set.inclusion hUV x)) ∘ f)
 #align structure_groupoid.local_invariant_prop.lift_prop_at_iff_comp_inclusion StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion
 
+theorem liftProp_subtype_val {Q : (H → H) → Set H → H → Prop} (hG : LocalInvariantProp G G Q)
+    (hQ : ∀ y, Q id univ y) (U : Opens M) :
+    LiftProp Q (Subtype.val : U → M) := by
+  intro x
+  show LiftPropAt Q (id ∘ Subtype.val) x
+  rw [← hG.liftPropAt_iff_comp_subtype_val]
+  apply hG.liftProp_id hQ
+
 theorem liftProp_inclusion {Q : (H → H) → Set H → H → Prop} (hG : LocalInvariantProp G G Q)
     (hQ : ∀ y, Q id univ y) {U V : Opens M} (hUV : U ≤ V) :
     LiftProp Q (Set.inclusion hUV : U → V) := by

Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

@@ -28,11 +28,11 @@ open MeasureTheory MeasureTheory.Measure Set Function TopologicalSpace Bornology
 
 open scoped Topology Interval ENNReal BigOperators
 
-variable {X Y E R : Type*} [MeasurableSpace X] [TopologicalSpace X]
+variable {X Y E F R : Type*} [MeasurableSpace X] [TopologicalSpace X]
 
 variable [MeasurableSpace Y] [TopologicalSpace Y]
 
-variable [NormedAddCommGroup E] {f g : X → E} {μ : Measure X} {s : Set X}
+variable [NormedAddCommGroup E] [NormedAddCommGroup F] {f g : X → E} {μ : Measure X} {s : Set X}
 
 namespace MeasureTheory
 
@@ -45,17 +45,24 @@ def LocallyIntegrableOn (f : X → E) (s : Set X) (μ : Measure X := by volume_t
   ∀ x : X, x ∈ s → IntegrableAtFilter f (𝓝[s] x) μ
 #align measure_theory.locally_integrable_on MeasureTheory.LocallyIntegrableOn
 
-theorem LocallyIntegrableOn.mono (hf : MeasureTheory.LocallyIntegrableOn f s μ) {t : Set X}
+theorem LocallyIntegrableOn.mono_set (hf : LocallyIntegrableOn f s μ) {t : Set X}
     (hst : t ⊆ s) : LocallyIntegrableOn f t μ := fun x hx =>
   (hf x <| hst hx).filter_mono (nhdsWithin_mono x hst)
-#align measure_theory.locally_integrable_on.mono MeasureTheory.LocallyIntegrableOn.mono
+#align measure_theory.locally_integrable_on.mono MeasureTheory.LocallyIntegrableOn.mono_set
 
 theorem LocallyIntegrableOn.norm (hf : LocallyIntegrableOn f s μ) :
     LocallyIntegrableOn (fun x => ‖f x‖) s μ := fun t ht =>
   let ⟨U, hU_nhd, hU_int⟩ := hf t ht
   ⟨U, hU_nhd, hU_int.norm⟩
 #align measure_theory.locally_integrable_on.norm MeasureTheory.LocallyIntegrableOn.norm
 
+theorem LocallyIntegrableOn.mono (hf : LocallyIntegrableOn f s μ) {g : X → F}
+    (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ x ∂μ, ‖g x‖ ≤ ‖f x‖) :
+    LocallyIntegrableOn g s μ := by
+  intro x hx
+  rcases hf x hx with ⟨t, t_mem, ht⟩
+  exact ⟨t, t_mem, Integrable.mono ht hg.restrict (ae_restrict_of_ae h)⟩
+
 theorem IntegrableOn.locallyIntegrableOn (hf : IntegrableOn f s μ) : LocallyIntegrableOn f s μ :=
   fun _ _ => ⟨s, self_mem_nhdsWithin, hf⟩
 #align measure_theory.integrable_on.locally_integrable_on MeasureTheory.IntegrableOn.locallyIntegrableOn
@@ -69,7 +76,7 @@ theorem LocallyIntegrableOn.integrableOn_isCompact (hf : LocallyIntegrableOn f s
 
 theorem LocallyIntegrableOn.integrableOn_compact_subset (hf : LocallyIntegrableOn f s μ) {t : Set X}
     (hst : t ⊆ s) (ht : IsCompact t) : IntegrableOn f t μ :=
-  (hf.mono hst).integrableOn_isCompact ht
+  (hf.mono_set hst).integrableOn_isCompact ht
 #align measure_theory.locally_integrable_on.integrable_on_compact_subset MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset
 
 /-- If a function `f` is locally integrable on a set `s` in a second countable topological space,
@@ -171,6 +178,11 @@ def LocallyIntegrable (f : X → E) (μ : Measure X := by volume_tac) : Prop :=
   ∀ x : X, IntegrableAtFilter f (𝓝 x) μ
 #align measure_theory.locally_integrable MeasureTheory.LocallyIntegrable
 
+theorem locallyIntegrable_comap (hs : MeasurableSet s) :
+    LocallyIntegrable (fun x : s ↦ f x) (μ.comap Subtype.val) ↔ LocallyIntegrableOn f s μ := by
+  simp_rw [LocallyIntegrableOn, Subtype.forall', ← map_nhds_subtype_val]
+  exact forall_congr' fun _ ↦ (MeasurableEmbedding.subtype_coe hs).integrableAtFilter_iff_comap.symm
+
 theorem locallyIntegrableOn_univ : LocallyIntegrableOn f univ μ ↔ LocallyIntegrable f μ := by
   simp only [LocallyIntegrableOn, nhdsWithin_univ, mem_univ, true_imp_iff]; rfl
 #align measure_theory.locally_integrable_on_univ MeasureTheory.locallyIntegrableOn_univ
@@ -183,6 +195,12 @@ theorem Integrable.locallyIntegrable (hf : Integrable f μ) : LocallyIntegrable
   hf.integrableAtFilter _
 #align measure_theory.integrable.locally_integrable MeasureTheory.Integrable.locallyIntegrable
 
+theorem LocallyIntegrable.mono (hf : LocallyIntegrable f μ) {g : X → F}
+    (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ x ∂μ, ‖g x‖ ≤ ‖f x‖) :
+    LocallyIntegrable g μ := by
+  rw [← locallyIntegrableOn_univ] at hf ⊢
+  exact hf.mono hg h
+
 /-- If `f` is locally integrable with respect to `μ.restrict s`, it is locally integrable on `s`.
 (See `locallyIntegrableOn_iff_locallyIntegrable_restrict` for an iff statement when `s` is
 closed.) -/

Mathlib/MeasureTheory/Integral/IntegrableOn.lean

@@ -169,6 +169,11 @@ theorem IntegrableOn.restrict (h : IntegrableOn f s μ) (hs : MeasurableSet s) :
   rw [IntegrableOn, Measure.restrict_restrict hs]; exact h.mono_set (inter_subset_left _ _)
 #align measure_theory.integrable_on.restrict MeasureTheory.IntegrableOn.restrict
 
+theorem IntegrableOn.inter_of_restrict (h : IntegrableOn f s (μ.restrict t)) :
+    IntegrableOn f (s ∩ t) μ := by
+  have := h.mono_set (inter_subset_left s t)
+  rwa [IntegrableOn, μ.restrict_restrict_of_subset (inter_subset_right s t)] at this
+
 lemma Integrable.piecewise [DecidablePred (· ∈ s)]
     (hs : MeasurableSet s) (hf : IntegrableOn f s μ) (hg : IntegrableOn g sᶜ μ) :
     Integrable (s.piecewise f g) μ := by
@@ -240,12 +245,18 @@ theorem integrableOn_add_measure :
 
 theorem _root_.MeasurableEmbedding.integrableOn_map_iff [MeasurableSpace β] {e : α → β}
     (he : MeasurableEmbedding e) {f : β → E} {μ : Measure α} {s : Set β} :
-    IntegrableOn f s (Measure.map e μ) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ := by
-  simp only [IntegrableOn, he.restrict_map, he.integrable_map_iff]
+    IntegrableOn f s (μ.map e) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ := by
+  simp_rw [IntegrableOn, he.restrict_map, he.integrable_map_iff]
 #align measurable_embedding.integrable_on_map_iff MeasurableEmbedding.integrableOn_map_iff
 
+theorem _root_.MeasurableEmbedding.integrableOn_iff_comap [MeasurableSpace β] {e : α → β}
+    (he : MeasurableEmbedding e) {f : β → E} {μ : Measure β} {s : Set β} (hs : s ⊆ range e) :
+    IntegrableOn f s μ ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) (μ.comap e) := by
+  simp_rw [← he.integrableOn_map_iff, he.map_comap, IntegrableOn,
+    Measure.restrict_restrict_of_subset hs]
+
 theorem integrableOn_map_equiv [MeasurableSpace β] (e : α ≃ᵐ β) {f : β → E} {μ : Measure α}
-    {s : Set β} : IntegrableOn f s (Measure.map e μ) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ := by
+    {s : Set β} : IntegrableOn f s (μ.map e) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ := by
   simp only [IntegrableOn, e.restrict_map, integrable_map_equiv e]
 #align measure_theory.integrable_on_map_equiv MeasureTheory.integrableOn_map_equiv
 
@@ -397,6 +408,22 @@ def IntegrableAtFilter (f : α → E) (l : Filter α) (μ : Measure α := by vol
 
 variable {l l' : Filter α}
 
+theorem _root_.MeasurableEmbedding.integrableAtFilter_map_iff [MeasurableSpace β] {e : α → β}
+    (he : MeasurableEmbedding e) {f : β → E} :
+    IntegrableAtFilter f (l.map e) (μ.map e) ↔ IntegrableAtFilter (f ∘ e) l μ := by
+  simp_rw [IntegrableAtFilter, he.integrableOn_map_iff]
+  constructor <;> rintro ⟨s, hs⟩
+  · exact ⟨_, hs⟩
+  · exact ⟨e '' s, by rwa [mem_map, he.injective.preimage_image]⟩
+
+theorem _root_.MeasurableEmbedding.integrableAtFilter_iff_comap [MeasurableSpace β] {e : α → β}
+    (he : MeasurableEmbedding e) {f : β → E} {μ : Measure β} :
+    IntegrableAtFilter f (l.map e) μ ↔ IntegrableAtFilter (f ∘ e) l (μ.comap e) := by
+  simp_rw [← he.integrableAtFilter_map_iff, IntegrableAtFilter, he.map_comap]
+  constructor <;> rintro ⟨s, hs, int⟩
+  · exact ⟨s, hs, int.mono_measure <| μ.restrict_le_self⟩
+  · exact ⟨_, inter_mem hs range_mem_map, int.inter_of_restrict⟩
+
 theorem Integrable.integrableAtFilter (h : Integrable f μ) (l : Filter α) :
     IntegrableAtFilter f l μ :=
   ⟨univ, Filter.univ_mem, integrableOn_univ.2 h⟩

Mathlib/Topology/LocalHomeomorph.lean

@@ -1339,11 +1339,6 @@ noncomputable def toLocalHomeomorph [Nonempty α] : LocalHomeomorph α β :=
     h.continuous.continuousOn h.isOpenMap isOpen_univ
 #align open_embedding.to_local_homeomorph OpenEmbedding.toLocalHomeomorph
 
-theorem continuousAt_iff {f : α → β} {g : β → γ} (hf : OpenEmbedding f) {x : α} :
-    ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x) :=
-  hf.tendsto_nhds_iff'
-#align open_embedding.continuous_at_iff OpenEmbedding.continuousAt_iff
-
 end OpenEmbedding
 
 namespace TopologicalSpace.Opens
@@ -1435,6 +1430,14 @@ theorem subtypeRestr_symm_trans_subtypeRestr (f f' : LocalHomeomorph α β) :
   simp only [mfld_simps, Setoid.refl]
 #align local_homeomorph.subtype_restr_symm_trans_subtype_restr LocalHomeomorph.subtypeRestr_symm_trans_subtypeRestr
 
+theorem subtypeRestr_symm_eqOn (U : Opens α) [Nonempty U] :
+    EqOn e.symm (Subtype.val ∘ (e.subtypeRestr U).symm) (e.subtypeRestr U).target := by
+  intro y hy
+  rw [eq_comm, eq_symm_apply _ _ hy.1]
+  · change restrict _ e _ = _
+    rw [← subtypeRestr_coe, (e.subtypeRestr U).right_inv hy]
+  · have := map_target _ hy; rwa [subtypeRestr_source] at this
+
 theorem subtypeRestr_symm_eqOn_of_le {U V : Opens α} [Nonempty U] [Nonempty V] (hUV : U ≤ V) :
     EqOn (e.subtypeRestr V).symm (Set.inclusion hUV ∘ (e.subtypeRestr U).symm)
       (e.subtypeRestr U).target := by

Mathlib/Topology/Maps.lean

@@ -603,6 +603,11 @@ theorem OpenEmbedding.tendsto_nhds_iff' {f : α → β} (hf : OpenEmbedding f) {
     {l : Filter γ} {a : α} : Tendsto (g ∘ f) (𝓝 a) l ↔ Tendsto g (𝓝 (f a)) l := by
   rw [Tendsto, ← map_map, hf.map_nhds_eq]; rfl
 
+theorem OpenEmbedding.continuousAt_iff {f : α → β} (hf : OpenEmbedding f) {g : β → γ} {x : α} :
+    ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x) :=
+  hf.tendsto_nhds_iff'
+#align open_embedding.continuous_at_iff OpenEmbedding.continuousAt_iff
+
 theorem OpenEmbedding.continuous {f : α → β} (hf : OpenEmbedding f) : Continuous f :=
   hf.toEmbedding.continuous
 #align open_embedding.continuous OpenEmbedding.continuous