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 : OpensMeasurableSpace X
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
pos : ∀ (t : Set X) (ht_nhds : t ∈ 𝓝[s] x) (ht_int : IntegrableOn f t μ), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
obtain ⟨t, ht_nhds, ht_int⟩ := hf x h
-- 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
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
pos :
  ∀ (u : Set X) (hu_o : IsOpen[inst_1] u) (hu_x : x ∈ u) (hu_sub : u ∩ s ⊆ t), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
obtain ⟨u, hu_o, hu_x, hu_sub⟩ := mem_nhdsWithin.mp ht_nhds

Premises used: mem_nhdsWithin, 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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst_1] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
⟨u, hu_o.mem_nhds hu_x, ?_⟩

Premises used: 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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst_1] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
pos : IntegrableOn f u (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
refine ⟨u, hu_o.mem_nhds hu_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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst_1] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
pos : Integrable f (μ.restrict (u ∩ s))
⊢ IntegrableOn f u (μ.restrict s)

Tactic:
rw [IntegrableOn, restrict_restrict hu_o.measurableSet]

Premises used: MeasureTheory.IntegrableOn, IsOpen.measurableSet, MeasureTheory.Measure.restrict_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
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst_1] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ Integrable f (μ.restrict (u ∩ s))

Tactic:
ht_int.mono_set hu_sub

Premises used: MeasureTheory.IntegrableOn, 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
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst_1] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ Integrable f (μ.restrict (u ∩ s))

Tactic:
exact ht_int.mono_set hu_sub

Premises used: 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
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
neg :
  ∀ (hs : IsOpen[inst_1] sᶜ) (hf : LocallyIntegrableOn f s μ) (x : X) (h : x ∉ s),
    IntegrableAtFilter f (𝓝 x) (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
rw [← isOpen_compl_iff] at hs

Premises used: isOpen_compl_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
inst_4 : OpensMeasurableSpace X
hs : IsOpen[inst_1] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
⟨sᶜ, hs.mem_nhds h, ?_⟩

Premises used: Compl.compl, 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
hs : IsOpen[inst_1] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
neg : IntegrableOn f sᶜ (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
refine ⟨sᶜ, hs.mem_nhds h, ?_⟩
-- 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 : IsOpen[inst_1] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
neg : IntegrableOn f ∅ μ
neg₁ : MeasurableSet sᶜ
⊢ IntegrableOn f sᶜ (μ.restrict s)

Tactic:
rw [IntegrableOn, restrict_restrict, inter_comm, inter_compl_self, ← IntegrableOn]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_restrict, Set.inter_comm, Set.inter_compl_self
-- 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 : IsOpen[inst_1] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableOn f ∅ μ

Tactic:
integrableOn_empty

Premises used: MeasureTheory.integrableOn_empty
-- 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 : IsOpen[inst_1] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ MeasurableSet sᶜ

Tactic:
hs.measurableSet

Premises used: IsOpen.measurableSet
-- 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 : IsOpen[inst_1] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableOn f ∅ μ

Tactic:
exacts [integrableOn_empty, hs.measurableSet]

Premises used: IsOpen.measurableSet, MeasureTheory.integrableOn_empty
-- 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 ε
k : Set X
hf : LocallyIntegrable f μ
hk : IsCompact k
⊢ IntegrableOn f k μ

Tactic:
(hf.locallyIntegrableOn k).integrableOn_isCompact hk

Premises used: MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact, MeasureTheory.LocallyIntegrable.locallyIntegrableOn
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ k ⊆ u ∧ IntegrableOn f u μ

Tactic:
IsCompact.induction_on hk ?_ ?_ ?_ ?_

Premises used: IsCompact.induction_on
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
refine_1 : ∃ (u : Set X), IsOpen[inst_1] u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ
refine_2 :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t →
      (∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ) →
        ∃ (u : Set X), IsOpen[inst_1] u ∧ s ⊆ u ∧ IntegrableOn f u μ
refine_3 :
  ∀ ⦃s t : Set X⦄,
    (∃ (u : Set X), IsOpen[inst_1] u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
      (∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ) →
        ∃ (u : Set X), IsOpen[inst_1] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ
refine_4 : ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ k ⊆ u ∧ IntegrableOn f u μ

Tactic:
refine IsCompact.induction_on hk ?_ ?_ ?_ ?_
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ

Tactic:
⟨∅, isOpen_empty, Subset.rfl, integrableOn_empty⟩

Premises used: MeasureTheory.integrableOn_empty, Set.Subset.rfl, And.intro, Exists.intro, EmptyCollection.emptyCollection, isOpen_empty
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ

Tactic:
refine ⟨∅, isOpen_empty, Subset.rfl, integrableOn_empty⟩
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
s t : Set X
hst : s ⊆ t
u : Set X
u_open : IsOpen[inst_1] u
tu : t ⊆ u
hu : IntegrableOn f u μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ s ⊆ u ∧ IntegrableOn f u μ

Tactic:
⟨u, u_open, hst.trans tu, hu⟩

Premises used: HasSubset.Subset.trans, And.intro, 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
inst_4 : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
s t : Set X
hst : s ⊆ t
u : Set X
u_open : IsOpen[inst_1] u
tu : t ⊆ u
hu : IntegrableOn f u μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ s ⊆ u ∧ IntegrableOn f u μ

Tactic:
exact ⟨u, u_open, hst.trans tu, hu⟩
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
s t u : Set X
u_open : IsOpen[inst_1] u
su : s ⊆ u
hu : IntegrableOn f u μ
v : Set X
v_open : IsOpen[inst_1] v
tv : t ⊆ v
hv : IntegrableOn f v μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
⟨u ∪ v, u_open.union v_open, union_subset_union su tv, hu.union hv⟩

Premises used: Set.union_subset_union, MeasureTheory.IntegrableOn.union, IsOpen.union, And.intro, Exists.intro, Union.union
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
s t u : Set X
u_open : IsOpen[inst_1] u
su : s ⊆ u
hu : IntegrableOn f u μ
v : Set X
v_open : IsOpen[inst_1] v
tv : t ⊆ v
hv : IntegrableOn f v μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
exact ⟨u ∪ v, u_open.union v_open, union_subset_union su tv, hu.union hv⟩
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
refine_4 : x ∈ k → ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ
⊢ x ∈ k → ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ

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
inst_4 : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
h : x ∈ k
refine_4 :
  ∀ (u : Set X) (ux : u ∈ 𝓝 x) (hu : IntegrableOn f u μ),
    ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ
⊢ ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
rcases hf x with ⟨u, ux, hu⟩
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
h : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
refine_4 :
  ∀ (v : Set X) (vu : v ⊆ u) (v_open : IsOpen[inst_1] v) (xv : x ∈ v),
    ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ
⊢ ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
rcases mem_nhds_iff.1 ux with ⟨v, vu, v_open, xv⟩

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
inst_4 : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
h : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
v : Set X
vu : v ⊆ u
v_open : IsOpen[inst_1] v
xv : x ∈ v
⊢ ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
⟨v, nhdsWithin_le_nhds (v_open.mem_nhds xv), v, v_open, Subset.rfl, hu.mono_set vu⟩

Premises used: nhdsWithin_le_nhds, Set.Subset.rfl, MeasureTheory.IntegrableOn.mono_set, 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
inst_4 : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
h : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
v : Set X
vu : v ⊆ u
v_open : IsOpen[inst_1] v
xv : x ∈ v
⊢ ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
exact ⟨v, nhdsWithin_le_nhds (v_open.mem_nhds xv), v, v_open, Subset.rfl, hu.mono_set vu⟩
-- 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
⊢ LocallyIntegrable f μ ↔ ∀ (k : Set X), IsCompact k → IntegrableOn f k μ

Tactic:
⟨fun hf _k hk => hf.integrableOn_isCompact hk, fun hf x =>
    let ⟨K, hK, h2K⟩ := exists_compact_mem_nhds x
    ⟨K, h2K, hf K hK⟩⟩

Premises used: _private.0.MeasureTheory.locallyIntegrable_iff.match_1, WeaklyLocallyCompactSpace.exists_compact_mem_nhds, nhds, MeasureTheory.IntegrableAtFilter, MeasureTheory.LocallyIntegrable.integrableOn_isCompact, And.intro, Iff.intro, 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
inst_4 : PseudoMetrizableSpace ε
inst_5 : SecondCountableTopology X
hf : LocallyIntegrable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
simpa only [restrict_univ] using (locallyIntegrableOn_univ.mpr hf).aestronglyMeasurable

Premises used: Iff.mpr, MeasureTheory.locallyIntegrableOn_univ, MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable, MeasureTheory.Measure.restrict_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
inst_4 : SecondCountableTopology X
hf : LocallyIntegrable f μ
rcases :
  ∀ (u : ℕ → Set X) (u_open : ∀ (n : ℕ), IsOpen[inst_1] (u n))
    (u_union : Subset.{u_1} (α := Set X) univ (⋃ (n : ℕ), u n)) (hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ),
    ∃ (u : ℕ → Set X),
      (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧
        Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), u n) univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ
⊢ ∃ (u : ℕ → Set X),
    (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧
      Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), u n) univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

Tactic:
rcases (hf.locallyIntegrableOn univ).exists_nat_integrableOn with ⟨u, u_open, u_union, hu⟩

Premises used: Set.univ, MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn, MeasureTheory.LocallyIntegrable.locallyIntegrableOn
-- 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 : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen[inst_1] (u n)
u_union : Subset.{u_1} (α := Set X) univ (⋃ (n : ℕ), u n)
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
⊢ ∃ (u : ℕ → Set X),
    (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧
      Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), u n) univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

Tactic:
⟨u, u_open, eq_univ_of_univ_subset u_union, fun n ↦ ?_⟩

Premises used: Set.eq_univ_of_univ_subset, And.intro, 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
inst_4 : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen[inst_1] (u n)
u_union : Subset.{u_1} (α := Set X) univ (⋃ (n : ℕ), u n)
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
refine : ∀ (n : ℕ), IntegrableOn f (u n) μ
⊢ ∃ (u : ℕ → Set X),
    (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧
      Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), u n) univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

Tactic:
refine ⟨u, u_open, eq_univ_of_univ_subset u_union, fun n ↦ ?_⟩
-- 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 : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen[inst_1] (u n)
u_union : Subset.{u_1} (α := Set X) univ (⋃ (n : ℕ), u n)
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
n : ℕ
⊢ IntegrableOn f (u n) μ

Tactic:
simpa only [inter_univ] using hu n

Premises used: Set.inter_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
inst_4 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
rcases :
  ∀ (U : Set X) (hU : U ∈ 𝓝 x) (h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)),
    IntegrableAtFilter f (𝓝 x) μ
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
rcases μ.finiteAt_nhds x with ⟨U, hU, h'U⟩

Premises used: MeasureTheory.Measure.finiteAt_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 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : Fact (μ U < ⊤) := ⟨h'U⟩
-- 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 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
⟨U, hU, ?_⟩

Premises used: MeasureTheory.IntegrableAtFilter, And.intro, 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
inst_4 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
refine : IntegrableOn f U μ
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
refine ⟨U, hU, ?_⟩
-- 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 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
rw : MemLp f 1 (μ.restrict U)
⊢ IntegrableOn f U μ

Tactic:
rw [IntegrableOn, ← memLp_one_iff_integrable]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.memLp_one_iff_integrable
-- 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 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ MemLp f 1 (μ.restrict U)

Tactic:
apply (hf.restrict U).mono_exponent hp

Premises used: MeasureTheory.MemLp.mono_exponent, MeasureTheory.MemLp.restrict