-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem locallyIntegrableOn_iff [LocallyCompactSpace X] (hs : IsLocallyClosed s) :
    LocallyIntegrableOn f s μ ↔ ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn f k μ

Proof state:
case 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
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen U
hZ : IsClosed Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ

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

Result:
case intro.intro.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
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen U
hZ : IsClosed 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 (𝓝[U ∩ Z] x) μ

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✝ : LocallyCompactSpace X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
x : X
hx : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x) μ

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

Result:
case 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
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen U
hZ : IsClosed Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ

Proof state:
case intro.intro.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
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen U
hZ : IsClosed 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 (𝓝[U ∩ Z] x) μ

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

Result:
case intro.intro.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
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen U
hZ : IsClosed 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) μ

Proof state:
case intro.intro.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
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen U
hZ : IsClosed 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:
refine ⟨Z ∩ K, inter_mem_nhdsWithin _ (mem_interior_iff_mem_nhds.1 hxK), ?_⟩

Result:
case intro.intro.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
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen U
hZ : IsClosed 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) μ

Proof state:
case intro.intro.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
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen U
hZ : IsClosed 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)

Result:
no goals

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✝ : LocallyCompactSpace X
hs : IsLocallyClosed s
⊢ 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 ↦ ?_⟩

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✝ : LocallyCompactSpace X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
x : X
hx : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x) μ