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 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
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) μ
T' : Set (Set X) := insert ∅ T
⊢ T'.Countable

Tactic:
have T'_count : T'.Countable := Countable.insert ∅ T_count
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
⊢ T'.Nonempty

Tactic:
simp only [T', insert_nonempty]

Premises used: Set.insert_nonempty
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
⊢ T'.Nonempty

Tactic:
have T'_ne : T'.Nonempty := by simp only [T', insert_nonempty]
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
rcases :
  ∀ (u : ℕ → Set X) (hu : T' = range u),
    ∃ (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 T'_count.exists_eq_range T'_ne with ⟨u, hu⟩

Premises used: Set.Countable.exists_eq_range
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
⊢ ∃ (u : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ

Tactic:
⟨u, ?_, ?_, ?_⟩

Premises used: 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
refine_1 : ∀ (n : ℕ), IsOpen[inst_1] (u n)
refine_2 : s ⊆ ⋃ (n : ℕ), u n
refine_3 : ∀ (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:
refine ⟨u, ?_, ?_, ?_⟩
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
rw : u n ∈ range u
⊢ u n ∈ T'

Tactic:
rw [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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
⊢ u n ∈ range u

Tactic:
mem_range_self n

Premises used: Set.mem_range_self
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
⊢ u n ∈ range u

Tactic:
exact mem_range_self n

Premises used: Set.mem_range_self
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
⊢ u n ∈ T'

Tactic:
have : u n ∈ T' := by rw [hu]; exact mem_range_self n
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
refine_1 : ∀ (h : u n = ∅), IsOpen[inst_1] (u n)
refine_1₁ : ∀ (h : u n ∈ T), IsOpen[inst_1] (u n)
⊢ IsOpen[inst_1] (u n)

Tactic:
rcases mem_insert_iff.1 this with h | h

Premises used: Iff.mp, Set.mem_insert_iff
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
h : u n = ∅
refine_1 : IsOpen[inst_1] ∅
⊢ IsOpen[inst_1] (u n)

Tactic:
rw [h]
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
h : u n = ∅
⊢ IsOpen[inst_1] ∅

Tactic:
isOpen_empty

Premises used: isOpen_empty
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
h : u n = ∅
⊢ IsOpen[inst_1] ∅

Tactic:
exact isOpen_empty

Premises used: isOpen_empty
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
h : u n ∈ T
⊢ IsOpen[inst_1] (u n)

Tactic:
T_open _ h
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
h : u n ∈ T
⊢ IsOpen[inst_1] (u n)

Tactic:
exact T_open _ h
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
⊢ ∃ v ∈ T, x ∈ v

Tactic:
simpa only [mem_iUnion, exists_prop] using sT hx

Premises used: Set.mem_iUnion, exists_prop
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
refine_2 : ∀ (v : Set X) (hv : v ∈ T) (h'v : x ∈ v), Membership.mem (γ := Set X) (⋃ (n : ℕ), u n) x
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u n) x

Tactic:
obtain ⟨v, hv, h'v⟩ : ∃ v, v ∈ T ∧ x ∈ v := by simpa only [mem_iUnion, exists_prop] using sT 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 : X → ε
μ : Measure X
s : Set X
inst_4 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
v : Set X
hv : v ∈ T
h'v : x ∈ v
rw : v ∈ T'
⊢ v ∈ range u

Tactic:
rw [← 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
v : Set X
hv : v ∈ T
h'v : x ∈ v
⊢ v ∈ T'

Tactic:
subset_insert ∅ T hv

Premises used: Set.Mem, EmptyCollection.emptyCollection, Set.subset_insert
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
v : Set X
hv : v ∈ T
h'v : x ∈ v
⊢ v ∈ T'

Tactic:
exact subset_insert ∅ T hv

Premises used: EmptyCollection.emptyCollection, Set.subset_insert
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
v : Set X
hv : v ∈ T
h'v : x ∈ v
⊢ v ∈ range u

Tactic:
have : v ∈ range u := by rw [← hu]; exact subset_insert ∅ T hv
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
v : Set X
hv : v ∈ T
h'v : x ∈ v
this : v ∈ range u
⊢ ∃ (n : ℕ), u n = v

Tactic:
simpa only [mem_range] using this

Premises used: Set.mem_range
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
v : Set X
hv : v ∈ T
h'v : x ∈ v
this : v ∈ range u
refine_2 :
  ∀ (n : ℕ) (hv : u n ∈ T) (h'v : x ∈ u n) (this : u n ∈ range u), Membership.mem (γ := Set X) (⋃ (n : ℕ), u n) x
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u n) x

Tactic:
obtain ⟨n, rfl⟩ : ∃ n, u n = v := by simpa only [mem_range] using this

Premises used: rfl
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
n : ℕ
hv : u n ∈ T
h'v : x ∈ u n
this : u n ∈ range u
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u n) x

Tactic:
mem_iUnion_of_mem _ h'v

Premises used: Set.mem_iUnion_of_mem
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
n : ℕ
hv : u n ∈ T
h'v : x ∈ u n
this : u n ∈ range u
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u n) x

Tactic:
exact mem_iUnion_of_mem _ h'v

Premises used: Set.mem_iUnion_of_mem
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
refine_3 : ∀ (h : u n = ∅), IntegrableOn f (u n ∩ s) μ
refine_3₁ : ∀ (h : u n ∈ T), IntegrableOn f (u n ∩ s) μ
⊢ IntegrableOn f (u n ∩ s) μ

Tactic:
rcases mem_insert_iff.1 this with h | h

Premises used: Iff.mp, Set.mem_insert_iff
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
h : u n = ∅
⊢ IntegrableOn f (u n ∩ s) μ

Tactic:
simp only [h, empty_inter, integrableOn_empty]

Premises used: Set.empty_inter, MeasureTheory.integrableOn_empty
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
h : u n ∈ T
⊢ IntegrableOn f (u n ∩ s) μ

Tactic:
hT _ h
-- 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 μ
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) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
h : u n ∈ T
⊢ IntegrableOn f (u n ∩ s) μ

Tactic:
exact hT _ h
-- 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 ε
inst_5 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
rcases :
  ∀ (u : ℕ → Set X) (su : s ⊆ ⋃ (n : ℕ), u n) (hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ),
    AEStronglyMeasurable f (μ.restrict s)
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
rcases hf.exists_nat_integrableOn with ⟨u, -, su, hu⟩

Premises used: MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn
-- 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 ε
inst_5 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ℕ → Set X
su : s ⊆ ⋃ (n : ℕ), u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
rw : s = (⋃ (i : ℕ), u i) ∩ s
⊢ s = ⋃ (n : ℕ), u n ∩ s

Tactic:
rw [← iUnion_inter]

Premises used: Set.iUnion_inter
-- 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 ε
inst_5 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ℕ → Set X
su : s ⊆ ⋃ (n : ℕ), u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
⊢ s = (⋃ (i : ℕ), u i) ∩ s

Tactic:
(inter_eq_right.mpr su).symm

Premises used: Iff.mpr, Set.inter_eq_right, Eq.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
inst_4 : PseudoMetrizableSpace ε
inst_5 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ℕ → Set X
su : s ⊆ ⋃ (n : ℕ), u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
⊢ s = (⋃ (i : ℕ), u i) ∩ s

Tactic:
exact (inter_eq_right.mpr su).symm

Premises used: Iff.mpr, Set.inter_eq_right, Eq.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
inst_4 : PseudoMetrizableSpace ε
inst_5 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ℕ → Set X
su : s ⊆ ⋃ (n : ℕ), u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
⊢ s = ⋃ (n : ℕ), u n ∩ s

Tactic:
have : s = ⋃ n, u n ∩ s := by rw [← iUnion_inter]; exact (inter_eq_right.mpr su).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
inst_4 : PseudoMetrizableSpace ε
inst_5 : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ℕ → Set X
su : s ⊆ ⋃ (n : ℕ), u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
this : s = ⋃ (n : ℕ), u n ∩ s
rw : ∀ (i : ℕ), AEStronglyMeasurable f (μ.restrict (u i ∩ s))
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
rw [this, aestronglyMeasurable_iUnion_iff]

Premises used: aestronglyMeasurable_iUnion_iff