awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : PseudoMetrizableSpace ε
inst_5 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ℕ → Set X
su : s ⊆ ⋃ (n : ℕ), u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
this : s = ⋃ (n : ℕ), u n ∩ s
⊢ ∀ (i : ℕ), AEStronglyMeasurable f (μ.restrict (u i ∩ s))

Tactic:
fun i : ℕ => (hu i).aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : PseudoMetrizableSpace ε
inst_5 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ℕ → Set X
su : s ⊆ ⋃ (n : ℕ), u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
this : s = ⋃ (n : ℕ), u n ∩ s
⊢ ∀ (i : ℕ), AEStronglyMeasurable f (μ.restrict (u i ∩ s))

Tactic:
exact fun i : ℕ => (hu i).aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn f s μ ↔ ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ

Tactic:
⟨fun hf k hk ↦ hf.integrableOn_compact_subset hk, fun hf x hx ↦ ?_⟩

Premises used: MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
hs : IsLocallyClosed s
refine : ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (x : X) (hx : x ∈ s), IntegrableAtFilter f (𝓝[s] x) μ
⊢ LocallyIntegrableOn f s μ ↔ ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ

Tactic:
refine ⟨fun hf k hk ↦ hf.integrableOn_compact_subset hk, fun hf x hx ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
x : X
hx : x ∈ s
rcases :
  ∀ (U Z : Set X) (hU : IsOpen[inst_1] U) (hZ : IsClosed[inst_1] Z) (hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ)
    (hx : x ∈ U ∩ Z), IntegrableAtFilter f (𝓝[U ∩ Z] x) μ
⊢ IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
rcases hs with ⟨U, Z, hU, hZ, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
rcases : ∀ (K : Set X) (hK : IsCompact K) (hxK : x ∈ interior K) (hKU : K ⊆ U), IntegrableAtFilter f (𝓝[U ∩ Z] x) μ
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ

Tactic:
rcases exists_compact_subset hU hx.1 with ⟨K, hK, hxK, hKU⟩

Premises used: exists_compact_subset, And.left
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
rw : IntegrableAtFilter f (𝓝[Z] x) μ
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ

Tactic:
rw [nhdsWithin_inter_of_mem (nhdsWithin_le_nhds <| hU.mem_nhds hx.1)]

Premises used: nhdsWithin_inter_of_mem, nhdsWithin_le_nhds, And.left, IsOpen.mem_nhds
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableAtFilter f (𝓝[Z] x) μ

Tactic:
⟨Z ∩ K, inter_mem_nhdsWithin _ (mem_interior_iff_mem_nhds.1 hxK), ?_⟩

Premises used: inter_mem_nhdsWithin, mem_interior_iff_mem_nhds, Inter.inter, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
refine : IntegrableOn f (Z ∩ K) μ
⊢ IntegrableAtFilter f (𝓝[Z] x) μ

Tactic:
refine ⟨Z ∩ K, inter_mem_nhdsWithin _ (mem_interior_iff_mem_nhds.1 hxK), ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableOn f (Z ∩ K) μ

Tactic:
hf (Z ∩ K) (fun y hy ↦ ⟨hKU hy.2, hy.1⟩) (.inter_left hK hZ)

Premises used: IsCompact.inter_left, Inter.inter, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableOn f (Z ∩ K) μ

Tactic:
exact hf (Z ∩ K) (fun y hy ↦ ⟨hKU hy.2, hy.1⟩) (.inter_left hK hZ)

Premises used: IsCompact.inter_left, Inter.inter, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
s : Set X
E : Type u_9
H : Type u_10
𝕜 : Type u_11
𝕜' : Type u_12
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜' E
inst_6 : NormedAddCommGroup H
inst_7 : NormedSpace 𝕜 H
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
f : X → H
L : H →SL[σ] E
hf : LocallyIntegrableOn f s μ
⊢ LocallyIntegrableOn.{u_1, u_9} (ε := E) ((⇑L : (a : H) → E) ∘ f) s μ

Tactic:
(L.integrableAtFilter_comp <| hf · ·)

Premises used: ContinuousLinearMap.integrableAtFilter_comp, MeasureTheory.LocallyIntegrableOn
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
s : Set X
inst_4 : ContinuousAdd ε''
f g : X → ε''
hf : LocallyIntegrableOn f s μ
hg : LocallyIntegrableOn g s μ
⊢ LocallyIntegrableOn (f + g) s μ

Tactic:
fun x hx ↦ (hf x hx).add (hg x hx)

Premises used: MeasureTheory.IntegrableAtFilter.add, MeasureTheory.LocallyIntegrableOn
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
f g : X → E
hf : LocallyIntegrableOn f s μ
hg : LocallyIntegrableOn g s μ
⊢ LocallyIntegrableOn (f - g) s μ

Tactic:
fun x hx ↦ (hf x hx).sub (hg x hx)

Premises used: MeasureTheory.LocallyIntegrableOn, MeasureTheory.IntegrableAtFilter.sub
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
f : X → E
hf : LocallyIntegrableOn f s μ
⊢ LocallyIntegrableOn (-f) s μ

Tactic:
fun x hx ↦ (hf x hx).neg

Premises used: MeasureTheory.IntegrableAtFilter.neg, MeasureTheory.LocallyIntegrableOn
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
f : X → E
⊢ (∀ x ∈ s, IntegrableAtFilter (-f) (𝓝[s] x) μ) ↔ ∀ x ∈ s, IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
simp_rw [MeasureTheory.integrableAtFilter_neg_iff]

Premises used: MeasureTheory.integrableAtFilter_neg_iff
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
𝕜 : Type u_9
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 E
f : X → E
hf : LocallyIntegrableOn f s μ
c : 𝕜
⊢ LocallyIntegrableOn (c • f) s μ

Tactic:
fun x hx ↦ (hf x hx).smul c

Premises used: MeasureTheory.IntegrableAtFilter.smul, MeasureTheory.LocallyIntegrableOn
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
𝕜 : Type u_9
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 E
f : X → E
c : 𝕜
⊢ (∀ x ∈ s, IntegrableAtFilter (c • f) (𝓝[s] x) μ) ↔ c = 0 ∨ ∀ x ∈ s, IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
grind [integrableAtFilter_smul_iff]

Premises used: MeasureTheory.integrableAtFilter_smul_iff
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
hs : MeasurableSet s
simp_rw :
  LocallyIntegrable.{u_1, u_3} (ε := ε) (fun (x : (↑s : Type u_1)) ↦ f (↑x : X))
      (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) ↔
    ∀ (x : { a : X // a ∈ s }), IntegrableAtFilter f (Filter.map (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x)) μ
⊢ LocallyIntegrable.{u_1, u_3} (ε := ε) (fun (x : (↑s : Type u_1)) ↦ f (↑x : X))
      (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) ↔
    LocallyIntegrableOn f s μ

Tactic:
simp_rw [LocallyIntegrableOn, Subtype.forall', ← map_nhds_subtype_val]

Premises used: MeasureTheory.LocallyIntegrableOn, Subtype.forall', map_nhds_subtype_val
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
hs : MeasurableSet s
⊢ LocallyIntegrable.{u_1, u_3} (ε := ε) (fun (x : (↑s : Type u_1)) ↦ f (↑x : X))
      (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) ↔
    ∀ (x : { a : X // a ∈ s }), IntegrableAtFilter f (Filter.map (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x)) μ

Tactic:
forall_congr' fun _ ↦ (MeasurableEmbedding.subtype_coe hs).integrableAtFilter_iff_comap.symm

Premises used: MeasurableEmbedding.integrableAtFilter_iff_comap, MeasureTheory.LocallyIntegrable, forall_congr', Iff.symm, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
hs : MeasurableSet s
⊢ LocallyIntegrable.{u_1, u_3} (ε := ε) (fun (x : (↑s : Type u_1)) ↦ f (↑x : X))
      (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) ↔
    ∀ (x : { a : X // a ∈ s }), IntegrableAtFilter f (Filter.map (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x)) μ

Tactic:
exact forall_congr' fun _ ↦ (MeasurableEmbedding.subtype_coe hs).integrableAtFilter_iff_comap.symm

Premises used: MeasurableEmbedding.integrableAtFilter_iff_comap, forall_congr', Iff.symm, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
simp : (∀ (x : X), IntegrableAtFilter f (𝓝 x) μ) ↔ LocallyIntegrable f μ
⊢ LocallyIntegrableOn f univ μ ↔ LocallyIntegrable f μ

Tactic:
simp only [LocallyIntegrableOn, nhdsWithin_univ, mem_univ, true_imp_iff]

Premises used: nhdsWithin_univ, true_imp_iff, MeasureTheory.LocallyIntegrableOn, Set.mem_univ
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
⊢ (∀ (x : X), IntegrableAtFilter f (𝓝 x) μ) ↔ LocallyIntegrable f μ

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
hf : LocallyIntegrable f μ
s : Set X
⊢ LocallyIntegrableOn f s μ

Tactic:
fun x _ => (hf x).filter_mono nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, MeasureTheory.LocallyIntegrableOn, MeasureTheory.IntegrableAtFilter.filter_mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
hf : Integrable f μ
⊢ LocallyIntegrable f μ

Tactic:
fun _ =>
  hf.integrableAtFilter _

Premises used: MeasureTheory.LocallyIntegrable, nhds, MeasureTheory.Integrable.integrableAtFilter
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
ε' : Type u_4
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
inst_4 : TopologicalSpace ε'
inst_5 : ContinuousENorm ε'
f : X → ε
μ : Measure X
hf : LocallyIntegrable f μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
rw :
  ∀ (hf : LocallyIntegrableOn f univ μ) {g : X → ε'} (hg : AEStronglyMeasurable g μ)
    (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ), LocallyIntegrableOn g univ μ
⊢ LocallyIntegrable g μ

Tactic:
rw [← locallyIntegrableOn_univ] at hf ⊢

Premises used: MeasureTheory.locallyIntegrableOn_univ
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
ε' : Type u_4
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
inst_4 : TopologicalSpace ε'
inst_5 : ContinuousENorm ε'
f : X → ε
μ : Measure X
hf : LocallyIntegrableOn f univ μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
⊢ LocallyIntegrableOn g univ μ

Tactic:
hf.mono_enorm hg h

Premises used: MeasureTheory.LocallyIntegrableOn.mono_enorm
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
ε' : Type u_4
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
inst_4 : TopologicalSpace ε'
inst_5 : ContinuousENorm ε'
f : X → ε
μ : Measure X
hf : LocallyIntegrableOn f univ μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
⊢ LocallyIntegrableOn g univ μ

Tactic:
exact hf.mono_enorm hg h

Premises used: MeasureTheory.LocallyIntegrableOn.mono_enorm
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
F : Type u_7
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
μ : Measure X
f : X → E
hf : LocallyIntegrable f μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
rw :
  ∀ (hf : LocallyIntegrableOn f univ μ) {g : X → F} (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖),
    LocallyIntegrableOn g univ μ
⊢ LocallyIntegrable g μ

Tactic:
rw [← locallyIntegrableOn_univ] at hf ⊢

Premises used: MeasureTheory.locallyIntegrableOn_univ
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
F : Type u_7
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
μ : Measure X
f : X → E
hf : LocallyIntegrableOn f univ μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrableOn g univ μ

Tactic:
hf.mono hg h

Premises used: MeasureTheory.LocallyIntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
F : Type u_7
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
μ : Measure X
f : X → E
hf : LocallyIntegrableOn f univ μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrableOn g univ μ

Tactic:
exact hf.mono hg h

Premises used: MeasureTheory.LocallyIntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
hf : LocallyIntegrable f μ
h : ν ≤ μ
⊢ LocallyIntegrable f ν

Tactic:
(hf · |>.mono_measure h)

Premises used: MeasureTheory.IntegrableAtFilter.mono_measure, MeasureTheory.LocallyIntegrable
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
hf : LocallyIntegrable f μ
h : f =ᶠ[ae μ] g
⊢ LocallyIntegrable g μ

Tactic:
(hf · |>.congr h)

Premises used: MeasureTheory.IntegrableAtFilter.congr, MeasureTheory.LocallyIntegrable
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
h : f =ᶠ[ae μ] g
⊢ LocallyIntegrable f μ ↔ LocallyIntegrable g μ

Tactic:
⟨(·.congr h), (·.congr h.symm)⟩

Premises used: MeasureTheory.LocallyIntegrable.congr, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
_ : x ∈ s → IntegrableAtFilter f (𝓝[s] x) μ
⊢ x ∈ s → IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
h : x ∈ s
obtain : ∀ (t : Set X) (ht_mem : t ∈ 𝓝 x) (ht_int : IntegrableOn f t (μ.restrict s)), IntegrableAtFilter f (𝓝[s] x) μ
⊢ IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
obtain ⟨t, ht_mem, ht_int⟩ := hf x
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
h : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t (μ.restrict s)
obtain : ∀ (u : Set X) (hu_sub : u ⊆ t) (hu_o : IsOpen[inst_1] u) (hu_mem : x ∈ u), IntegrableAtFilter f (𝓝[s] x) μ
⊢ IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
obtain ⟨u, hu_sub, hu_o, hu_mem⟩ := mem_nhds_iff.mp ht_mem

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
h : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t (μ.restrict s)
u : Set X
hu_sub : u ⊆ t
hu_o : IsOpen[inst_1] u
hu_mem : x ∈ u
⊢ IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
⟨_, inter_mem_nhdsWithin s (hu_o.mem_nhds hu_mem), ?_⟩

Premises used: inter_mem_nhdsWithin, MeasureTheory.IntegrableAtFilter, And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
h : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t (μ.restrict s)
u : Set X
hu_sub : u ⊆ t
hu_o : IsOpen[inst_1] u
hu_mem : x ∈ u
refine : IntegrableOn f (s ∩ u) μ
⊢ IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
refine ⟨_, inter_mem_nhdsWithin s (hu_o.mem_nhds hu_mem), ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
h : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t (μ.restrict s)
u : Set X
hu_sub : u ⊆ t
hu_o : IsOpen[inst_1] u
hu_mem : x ∈ u
⊢ IntegrableOn f (s ∩ u) μ

Tactic:
simpa only [IntegrableOn, Measure.restrict_restrict hu_o.measurableSet, inter_comm] using
    ht_int.mono_set hu_sub

Premises used: MeasureTheory.IntegrableOn, IsOpen.measurableSet, MeasureTheory.Measure.restrict_restrict, Set.inter_comm, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hs : IsClosed[inst_1] s
⊢ LocallyIntegrableOn f s μ ↔ LocallyIntegrable f (μ.restrict s)

Tactic:
⟨fun hf x => ?_, locallyIntegrableOn_of_locallyIntegrable_restrict⟩

Premises used: MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hs : IsClosed[inst_1] s
refine : ∀ (hf : LocallyIntegrableOn f s μ) (x : X), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
⊢ LocallyIntegrableOn f s μ ↔ LocallyIntegrable f (μ.restrict s)

Tactic:
refine ⟨fun hf x => ?_, locallyIntegrableOn_of_locallyIntegrable_restrict⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
pos : ∀ (h : x ∈ s), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
neg : ∀ (h : x ∉ s), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
by_cases h : x ∈ s