-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrableOn.exists_countable_integrableOn [SecondCountableTopology X]
    (hf : LocallyIntegrableOn f s μ) : ∃ T : Set (Set X), T.Countable ∧
    (∀ u ∈ T, IsOpen u) ∧ (s ⊆ ⋃ u ∈ T, u) ∧ (∀ u ∈ T, IntegrableOn f (u ∩ 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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
⊢ ∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ

Tactic:
obtain ⟨T, T_count, hT⟩ : ∃ T : Set s, T.Countable ∧ s ⊆ ⋃ i ∈ T, u i := by
  have : s ⊆ ⋃ x : s, u x := fun y hy => mem_iUnion_of_mem ⟨y, hy⟩ (xu ⟨y, hy⟩)
  obtain ⟨T, hT_count, hT_un⟩ := isOpen_iUnion_countable u u_open
  exact ⟨T, hT_count, by rwa [hT_un]⟩

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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
T : Set ↑s
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
⊢ ∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ 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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
⊢ ∃ T, T.Countable ∧ s ⊆ ⋃ i ∈ T, u i

Tactic:
have : s ⊆ ⋃ x : s, u x := fun y hy => mem_iUnion_of_mem ⟨y, hy⟩ (xu ⟨y, hy⟩)

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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
this : s ⊆ ⋃ x, u x
⊢ ∃ T, T.Countable ∧ s ⊆ ⋃ i ∈ T, u i

Proof state:
case intro.intro.refine_2
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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
T : Set ↑s
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
⊢ ∀ u_1 ∈ u '' T, IntegrableOn f (u_1 ∩ s) μ

Tactic:
rintro v ⟨w, -, rfl⟩

Result:
case intro.intro.refine_2.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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
T : Set ↑s
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
w : ↑s
⊢ IntegrableOn f (u w ∩ s) μ

Proof state:
case mk.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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
h't : IntegrableOn f t μ
u : Set X
u_open : IsOpen u
x_mem : x ∈ u
u_sub : u ∩ s ⊆ t
⊢ ∃ u, IsOpen u ∧ ↑⟨x, hx⟩ ∈ u ∧ IntegrableOn f (u ∩ s) μ

Tactic:
exact ⟨u, u_open, x_mem, h't.mono_set u_sub⟩

Result:
no goals

Proof state:
case mk.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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
h't : IntegrableOn f t μ
⊢ ∃ u, IsOpen u ∧ ↑⟨x, hx⟩ ∈ u ∧ IntegrableOn f (u ∩ s) μ

Tactic:
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, x_mem, u_sub⟩

Result:
case mk.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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
h't : IntegrableOn f t μ
u : Set X
u_open : IsOpen u
x_mem : x ∈ u
u_sub : u ∩ s ⊆ t
⊢ ∃ u, IsOpen u ∧ ↑⟨x, hx⟩ ∈ u ∧ IntegrableOn f (u ∩ 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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
this : s ⊆ ⋃ x, u x
T : Set ↑s
hT_count : T.Countable
hT_un : ⋃ i ∈ T, u i = ⋃ i, u i
⊢ s ⊆ ⋃ i ∈ T, u i

Tactic:
rwa [hT_un]

Result:
no goals

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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
this : s ⊆ ⋃ x, u x
T : Set ↑s
hT_count : T.Countable
hT_un : ⋃ i ∈ T, u i = ⋃ i, u i
⊢ ∃ T, T.Countable ∧ s ⊆ ⋃ i ∈ T, u i

Tactic:
exact ⟨T, hT_count, by rwa [hT_un]⟩

Result:
no goals

Proof state:
case intro.intro.refine_1
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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
T : Set ↑s
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
⊢ ∀ u_1 ∈ u '' T, IsOpen u_1

Tactic:
rintro v ⟨w, -, rfl⟩

Result:
case intro.intro.refine_1.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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
T : Set ↑s
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
w : ↑s
⊢ IsOpen (u w)

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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
this : ∀ (x : ↑s), ∃ u, IsOpen u ∧ ↑x ∈ u ∧ IntegrableOn f (u ∩ s) μ
⊢ ∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ

Tactic:
choose u u_open xu hu using this

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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ↑s → Set X
u_open : ∀ (x : ↑s), IsOpen (u x)
xu : ∀ (x : ↑s), ↑x ∈ u x
hu : ∀ (x : ↑s), IntegrableOn f (u x ∩ s) μ
⊢ ∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ