-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem MemLp.locallyIntegrable [IsLocallyFiniteMeasure μ] {f : X → E} {p : ℝ≥0∞}
    (hf : MemLp f p μ) (hp : 1 ≤ p) : LocallyIntegrable f μ

Proof state:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ⊤
this : Fact (μ U < ⊤)
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
refine ⟨U, hU, ?_⟩

Result:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ⊤
this : Fact (μ U < ⊤)
⊢ IntegrableOn f U μ

Proof state:
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
⊢ IntegrableAtFilter f (𝓝 x) μ

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

Result:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ⊤
⊢ IntegrableAtFilter f (𝓝 x) μ

Proof state:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ⊤
this : Fact (μ U < ⊤)
⊢ IntegrableOn f U μ

Tactic:
rw [IntegrableOn, ← memLp_one_iff_integrable]

Result:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ⊤
this : Fact (μ U < ⊤)
⊢ MemLp f 1 (μ.restrict U)

Proof state:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ⊤
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
have : Fact (μ U < ⊤) := ⟨h'U⟩

Result:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ⊤
this : Fact (μ U < ⊤)
⊢ IntegrableAtFilter f (𝓝 x) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
⊢ LocallyIntegrable f μ

Tactic:
intro x

Result:
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
⊢ IntegrableAtFilter f (𝓝 x) μ

Proof state:
case intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
f : X → E
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ⊤
this : Fact (μ U < ⊤)
⊢ MemLp f 1 (μ.restrict U)

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

Result:
no goals