-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrable.integrableOn_nhds_isCompact (hf : LocallyIntegrable f μ) {k : Set X}
    (hk : IsCompact k) : ∃ u, IsOpen u ∧ k ⊆ u ∧ IntegrableOn f u μ

Proof state:
case refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
a✝ : x ∈ k
⊢ ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
rcases hf x with ⟨u, ux, hu⟩

Result:
case refine_4.intro.intro
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
a✝ : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
⊢ ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ

Proof state:
case refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
intro x _

Result:
case refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
a✝ : x ∈ k
⊢ ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ

Proof state:
case refine_2
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen u ∧ s ⊆ u ∧ IntegrableOn f u μ

Tactic:
rintro s t hst ⟨u, u_open, tu, hu⟩

Result:
case refine_2.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
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
s t : Set X
hst : s ⊆ t
u : Set X
u_open : IsOpen u
tu : t ⊆ u
hu : IntegrableOn f u μ
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ IntegrableOn f u μ

Proof state:
case refine_3.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
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
s t u : Set X
u_open : IsOpen u
su : s ⊆ u
hu : IntegrableOn f u μ
v : Set X
v_open : IsOpen v
tv : t ⊆ v
hv : IntegrableOn f v μ
⊢ ∃ u, IsOpen u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

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

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
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∃ u, IsOpen u ∧ k ⊆ u ∧ IntegrableOn f u μ

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

Result:
case refine_1
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∃ u, IsOpen u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ

case refine_2
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen u ∧ s ⊆ u ∧ IntegrableOn f u μ

case refine_3
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ ⦃s t : Set X⦄,
    (∃ u, IsOpen u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
      (∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

case refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ

Proof state:
case refine_2.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
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
s t : Set X
hst : s ⊆ t
u : Set X
u_open : IsOpen u
tu : t ⊆ u
hu : IntegrableOn f u μ
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ IntegrableOn f u μ

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

Result:
no goals

Proof state:
case refine_1
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∃ u, IsOpen u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ

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

Result:
no goals

Proof state:
case refine_4.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
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
a✝ : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
v : Set X
vu : v ⊆ u
v_open : IsOpen v
xv : x ∈ v
⊢ ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen 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⟩

Result:
no goals

Proof state:
case refine_3
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ ⦃s t : Set X⦄,
    (∃ u, IsOpen u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
      (∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
rintro s t ⟨u, u_open, su, hu⟩ ⟨v, v_open, tv, hv⟩

Result:
case refine_3.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
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
s t u : Set X
u_open : IsOpen u
su : s ⊆ u
hu : IntegrableOn f u μ
v : Set X
v_open : IsOpen v
tv : t ⊆ v
hv : IntegrableOn f v μ
⊢ ∃ u, IsOpen u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

Proof state:
case refine_4.intro.intro
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
a✝ : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
⊢ ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ

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

Result:
case refine_4.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
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
a✝ : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
v : Set X
vu : v ⊆ u
v_open : IsOpen v
xv : x ∈ v
⊢ ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ