-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem locallyIntegrableOn_of_locallyIntegrable_restrict [OpensMeasurableSpace X]
    (hf : LocallyIntegrable f (μ.restrict s)) : LocallyIntegrableOn f s μ

Proof state:
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
⊢ LocallyIntegrableOn f s μ

Tactic:
intro x _

Result:
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
a✝ : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x) μ

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
a✝ : 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 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

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
a✝ : 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 u
hu_mem : x ∈ u
⊢ IntegrableAtFilter f (𝓝[s] x) μ

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

Result:
case intro.intro.intro.intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
a✝ : 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 u
hu_mem : x ∈ u
⊢ IntegrableOn f (s ∩ u) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
a✝ : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
obtain ⟨t, ht_mem, ht_int⟩ := hf x

Result:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
a✝ : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝[s] x) μ

Proof state:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
a✝ : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝[s] x) μ

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

Result:
case intro.intro.intro.intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
a✝ : 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 u
hu_mem : x ∈ u
⊢ IntegrableAtFilter f (𝓝[s] x) μ