awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
u : Set X
hu : IsOpen[inst_1] u
hxu : x ∈ u
hut : u ∩ s ⊆ t
refine : IntegrableOn f (u ∩ s) ν
⊢ IntegrableAtFilter f (𝓝[s] x) ν

Tactic:
refine ⟨u ∩ s, inter_mem (mem_nhdsWithin.mpr ⟨u, hu, hxu, inter_subset_left⟩) self_mem_nhdsWithin,
    ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
u : Set X
hu : IsOpen[inst_1] u
hxu : x ∈ u
hut : u ∩ s ⊆ t
⊢ IntegrableOn f (u ∩ s) ν

Tactic:
hf.mono_set hut |>.mono_measure' ?_

Premises used: MeasureTheory.IntegrableOn.mono_set, MeasureTheory.IntegrableOn.mono_measure'
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
u : Set X
hu : IsOpen[inst_1] u
hxu : x ∈ u
hut : u ∩ s ⊆ t
refine : ν.restrict (u ∩ s) ≤ μ.restrict (u ∩ s)
⊢ IntegrableOn f (u ∩ s) ν

Tactic:
refine hf.mono_set hut |>.mono_measure' ?_

Premises used: MeasureTheory.IntegrableOn.mono_set, MeasureTheory.IntegrableOn.mono_measure'
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
u : Set X
hu : IsOpen[inst_1] u
hxu : x ∈ u
hut : u ∩ s ⊆ t
simp_rw : (ν.restrict s).restrict u ≤ (μ.restrict s).restrict u
⊢ ν.restrict (u ∩ s) ≤ μ.restrict (u ∩ s)

Tactic:
simp_rw [← restrict_restrict hu.measurableSet]

Premises used: IsOpen.measurableSet, MeasureTheory.Measure.restrict_restrict
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
inst_4 : OpensMeasurableSpace X
hf_1 : LocallyIntegrableOn f s μ
h : ν.restrict s ≤ μ.restrict s
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hf : IntegrableOn f t μ
u : Set X
hu : IsOpen[inst_1] u
hxu : x ∈ u
hut : u ∩ s ⊆ t
⊢ (ν.restrict s).restrict u ≤ (μ.restrict s).restrict u

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ ν : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
h : ν ≤ μ
⊢ LocallyIntegrableOn f s ν

Tactic:
fun x hx ↦ (hf x hx).mono_measure h

Premises used: MeasureTheory.IntegrableAtFilter.mono_measure, MeasureTheory.LocallyIntegrableOn
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
obtain : ∀ (t : Set X) (hxt : t ∈ 𝓝[s] x) (hft : IntegrableOn f t μ), IntegrableAtFilter g (𝓝[s] x) μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
obtain ⟨t, hxt, hft⟩ := hf x hx
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
⟨s ∩ t, inter_mem self_mem_nhdsWithin hxt, ?_⟩

Premises used: Filter.inter_mem, Inter.inter, MeasureTheory.IntegrableAtFilter, self_mem_nhdsWithin, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
refine : IntegrableOn g (s ∩ t) μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
refine ⟨s ∩ t, inter_mem self_mem_nhdsWithin hxt, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ IntegrableOn g (s ∩ t) μ

Tactic:
(hft.mono_set inter_subset_right).congr ?_

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.Integrable.congr, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
refine : f =ᶠ[ae (μ.restrict (s ∩ t))] g
⊢ IntegrableOn g (s ∩ t) μ

Tactic:
refine (hft.mono_set inter_subset_right).congr ?_

Premises used: MeasureTheory.IntegrableOn.mono_set, MeasureTheory.Integrable.congr, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ f =ᶠ[ae (μ.restrict (s ∩ t))] g

Tactic:
h.filter_mono ?_

Premises used: Filter.EventuallyEq.filter_mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
refine : ae (μ.restrict (s ∩ t)) ≤ ae (μ.restrict s)
⊢ f =ᶠ[ae (μ.restrict (s ∩ t))] g

Tactic:
refine h.filter_mono ?_

Premises used: Filter.EventuallyEq.filter_mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
h₁ : s ∩ t ⊆ s
⊢ ae (μ.restrict (s ∩ t)) ≤ ae (μ.restrict s)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ s ∩ t ⊆ s

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ s ∩ t ⊆ s

Tactic:
exact inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᶠ[ae (μ.restrict s)] g
⊢ LocallyIntegrableOn f s μ ↔ LocallyIntegrableOn g s μ

Tactic:
⟨(·.congr h), (·.congr h.symm)⟩

Premises used: MeasureTheory.LocallyIntegrableOn.congr, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
hf : IntegrableOn f s μ
⊢ LocallyIntegrableOn f s μ

Tactic:
fun _ _ => ⟨s, self_mem_nhdsWithin, hf⟩

Premises used: MeasureTheory.IntegrableAtFilter, self_mem_nhdsWithin, And.intro, Exists.intro, MeasureTheory.LocallyIntegrableOn
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : PseudoMetrizableSpace ε
hf : LocallyIntegrableOn f s μ
hs : IsCompact s
⊢ IntegrableOn f s μ

Tactic:
IsCompact.induction_on hs integrableOn_empty (fun _u _v huv hv => hv.mono_set huv)
    (fun _u _v hu hv => integrableOn_union.mpr ⟨hu, hv⟩) hf

Premises used: IsCompact.induction_on
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : PseudoMetrizableSpace ε
hf : LocallyIntegrableOn f s μ
t : Set X
hst : t ⊆ s
ht : IsCompact t
⊢ IntegrableOn f t μ

Tactic:
(hf.mono_set hst).integrableOn_isCompact ht

Premises used: MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact, MeasureTheory.LocallyIntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
rcases :
  ∀ (t : Set X) (ht : t ∈ 𝓝[s] x) (h't : IntegrableOn f t μ),
    ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ

Tactic:
rcases hf x hx with ⟨t, ht, h't⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
h't : IntegrableOn f t μ
rcases :
  ∀ (u : Set X) (u_open : IsOpen[inst_1] u) (x_mem : x ∈ u) (u_sub : u ∩ s ⊆ t),
    ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ

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

Premises used: mem_nhdsWithin, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : 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[inst_1] u
x_mem : x ∈ u
u_sub : u ∩ s ⊆ t
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ

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

Premises used: MeasureTheory.IntegrableOn.mono_set, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : 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[inst_1] u
x_mem : x ∈ u
u_sub : u ∩ s ⊆ t
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx) : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ

Tactic:
exact ⟨u, u_open, x_mem, h't.mono_set u_sub⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
⊢ ∀ (x : (↑s : Type u_1)), ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑x : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ

Tactic:
have : ∀ x : s, ∃ u, IsOpen u ∧ x.1 ∈ u ∧ IntegrableOn f (u ∩ s) μ := by
    rintro ⟨x, hx⟩
    rcases hf x hx with ⟨t, ht, h't⟩
    rcases mem_nhdsWithin.1 ht with ⟨u, u_open, x_mem, u_sub⟩
    exact ⟨u, u_open, x_mem, h't.mono_set u_sub⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
this : ∀ (x : (↑s : Type u_1)), ∃ (u : Set X), IsOpen[inst_1] u ∧ (↑x : X) ∈ u ∧ IntegrableOn f (u ∩ s) μ
choose :
  ∀ (u : (x : (↑s : Type u_1)) → Set X) (u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x))
    (xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x) (hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ),
    ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
⊢ ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ

Tactic:
choose u u_open xu hu using this
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
⊢ s ⊆ ⋃ (x : (↑s : Type u_1)), u x

Tactic:
have : s ⊆ ⋃ x : s, u x := fun y hy => mem_iUnion_of_mem ⟨y, hy⟩ (xu ⟨y, hy⟩)
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
this : s ⊆ ⋃ (x : (↑s : Type u_1)), u x
obtain :
  ∀ (T : Set (↑s : Type u_1)) (hT_count : T.Countable)
    (hT_un : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ T, u i) (⋃ (i : (↑s : Type u_1)), u i)),
    ∃ (T : Set (↑s : Type u_1)), T.Countable ∧ s ⊆ ⋃ i ∈ T, u i
⊢ ∃ (T : Set (↑s : Type u_1)), T.Countable ∧ s ⊆ ⋃ i ∈ T, u i

Tactic:
obtain ⟨T, hT_count, hT_un⟩ := isOpen_iUnion_countable u u_open

Premises used: TopologicalSpace.isOpen_iUnion_countable
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
this : s ⊆ ⋃ (x : (↑s : Type u_1)), u x
T : Set (↑s : Type u_1)
hT_count : T.Countable
hT_un : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ T, u i) (⋃ (i : (↑s : Type u_1)), u i)
rwa rwa₁ rwa₂ rwa₃ : s ⊆ ⋃ (i : (↑s : Type u_1)), u i
⊢ s ⊆ ⋃ i ∈ T, u i

Tactic:
rwa [hT_un]
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
this : s ⊆ ⋃ (x : (↑s : Type u_1)), u x
T : Set (↑s : Type u_1)
hT_count : T.Countable
hT_un : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ T, u i) (⋃ (i : (↑s : Type u_1)), u i)
⊢ ∃ (T : Set (↑s : Type u_1)), T.Countable ∧ s ⊆ ⋃ i ∈ T, u i

Tactic:
exact ⟨T, hT_count, by rwa [hT_un]⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
obtain :
  ∀ (T : Set (↑s : Type u_1)) (T_count : T.Countable) (hT : s ⊆ ⋃ i ∈ T, u i),
    ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
⊢ ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] 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]⟩

Premises used: Set.Elem, Set
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
T : Set (↑s : Type u_1)
T_count : T.Countable
hT rwa rwa₁ rwa₂ rwa₃ : s ⊆ ⋃ y ∈ T, u y
⊢ s ⊆ ⋃ u_1 ∈ u '' T, u_1

Tactic:
rwa [biUnion_image]

Premises used: Set.biUnion_image
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
T : Set (↑s : Type u_1)
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
refine_1 : ∀ u_1 ∈ u '' T, IsOpen[inst_1] u_1
refine_2 : ∀ u_1 ∈ u '' T, IntegrableOn f (u_1 ∩ s) μ
⊢ ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ

Tactic:
refine ⟨u '' T, T_count.image _, ?_, by rwa [biUnion_image], ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
T : Set (↑s : Type u_1)
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
w : (↑s : Type u_1)
⊢ IsOpen[inst_1] (u w)

Tactic:
u_open _
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
T : Set (↑s : Type u_1)
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
w : (↑s : Type u_1)
⊢ IsOpen[inst_1] (u w)

Tactic:
exact u_open _
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
T : Set (↑s : Type u_1)
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
w : (↑s : Type u_1)
⊢ IntegrableOn f (u w ∩ s) μ

Tactic:
hu _
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : (x : (↑s : Type u_1)) → Set X
u_open : ∀ (x : (↑s : Type u_1)), IsOpen[inst_1] (u x)
xu : ∀ (x : (↑s : Type u_1)), (↑x : X) ∈ u x
hu : ∀ (x : (↑s : Type u_1)), IntegrableOn f (u x ∩ s) μ
T : Set (↑s : Type u_1)
T_count : T.Countable
hT : s ⊆ ⋃ i ∈ T, u i
w : (↑s : Type u_1)
⊢ IntegrableOn f (u w ∩ s) μ

Tactic:
exact hu _
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
rcases :
  ∀ (T : Set (Set X)) (T_count : T.Countable) (T_open : ∀ u ∈ T, IsOpen[inst_1] u) (sT : s ⊆ ⋃ u ∈ T, u)
    (hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ),
    ∃ (u : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
⊢ ∃ (u : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ

Tactic:
rcases hf.exists_countable_integrableOn with ⟨T, T_count, T_open, sT, hT⟩

Premises used: MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn