awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
⊢ ∃ (T : Set (Set X)), T.Countable ∧ (∀ u ∈ T, IsOpen[inst_1] u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
have refine_2 : ∀ u_1 ∈ u '' T, IntegrableOn f (u_1 ∩ s) μ
Tactic: refine ⟨u '' T, T_count.image _, ?_, by rwa [biUnion_image], ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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 : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
have 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) μ
Tactic: rcases hf.exists_countable_integrableOn with ⟨T, T_count, T_open, sT, hT⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
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
⊢ ∃ (u : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
have T'_count : T'.Countable
Tactic: have T'_count : T'.Countable := Countable.insert ∅ T_count
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
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
⊢ ∃ (u : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
have T'_ne : T'.Nonempty
Tactic: have T'_ne : T'.Nonempty := by simp only [T', insert_nonempty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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), (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
have 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) μ
Tactic: rcases T'_count.exists_eq_range T'_ne with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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) μ
have refine_1 : ∀ (n : ℕ), IsOpen[inst_1] (u n)
Tactic: refine ⟨u, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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)
⊢ ∃ (u : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
have refine_2 : s ⊆ ⋃ (n : ℕ), u n
Tactic: refine ⟨u, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
⊢ ∃ (u : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧ s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
have refine_3 : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
Tactic: refine ⟨u, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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'
have rw : u n ∈ range u
Tactic: rw [hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
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 : ℕ
⊢ IsOpen[inst_1] (u n)
have this : u n ∈ T'
Tactic: have : u n ∈ T' := by rw [hu]; exact mem_range_self n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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'
⊢ IsOpen[inst_1] (u n)
have refine_1 : ∀ (h : u n = ∅), IsOpen[inst_1] (u n)
Tactic: rcases mem_insert_iff.1 this with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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)
⊢ IsOpen[inst_1] (u n)
have refine_1₁ : ∀ (h : u n ∈ T), IsOpen[inst_1] (u n)
Tactic: rcases mem_insert_iff.1 this with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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] (u n)
have refine_1 : IsOpen[inst_1] ∅
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u n) x
have refine_2 : ∀ (v : Set X) (hv : v ∈ T) (h'v : x ∈ v), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
have rw : v ∈ T'
Tactic: rw [← hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
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
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u n) x
have this : v ∈ range u
Tactic: have : v ∈ range u := by rw [← hu]; exact subset_insert ∅ T hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
⊢ Membership.mem (γ := Set X) (⋃ (n : ℕ), u n) x
have 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
Tactic: obtain ⟨n, rfl⟩ : ∃ n, u n = v := by simpa only [mem_range] using this
Cleared hypotheses: v, hv, h'v, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
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 : ℕ
⊢ IntegrableOn f (u n ∩ s) μ
have this : u n ∈ T'
Tactic: have : u n ∈ T' := by rw [hu]; exact mem_range_self n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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'
⊢ IntegrableOn f (u n ∩ s) μ
have refine_3 : ∀ (h : u n = ∅), IntegrableOn f (u n ∩ s) μ
Tactic: rcases mem_insert_iff.1 this with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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) μ
⊢ IntegrableOn f (u n ∩ s) μ
have refine_3₁ : ∀ (h : u n ∈ T), IntegrableOn f (u n ∩ s) μ
Tactic: rcases mem_insert_iff.1 this with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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 μ
⊢ AEStronglyMeasurable f (μ.restrict s)
have rcases : ∀ (u : ℕ → Set X) (su : s ⊆ ⋃ (n : ℕ), u n) (hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ),
  AEStronglyMeasurable f (μ.restrict s)
Tactic: rcases hf.exists_nat_integrableOn with ⟨u, -, su, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
have rw : s = (⋃ (i : ℕ), u i) ∩ s
Tactic: rw [← iUnion_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (hypothesis)
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) μ
⊢ AEStronglyMeasurable f (μ.restrict s)
have this : s = ⋃ (n : ℕ), u n ∩ s
Tactic: have : s = ⋃ n, u n ∩ s := by rw [← iUnion_inter]; exact (inter_eq_right.mpr su).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
⊢ AEStronglyMeasurable f (μ.restrict s)
have rw : ∀ (i : ℕ), AEStronglyMeasurable f (μ.restrict (u i ∩ s))
Tactic: rw [this, aestronglyMeasurable_iUnion_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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 : LocallyCompactSpace X
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn f s μ ↔ ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
have refine : ∀ (hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ) (x : X) (hx : x ∈ s), IntegrableAtFilter f (𝓝[s] x) μ
Tactic: refine ⟨fun hf k hk ↦ hf.integrableOn_compact_subset hk, fun hf x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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 : LocallyCompactSpace X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
x : X
hx : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x) μ
have rcases : ∀ (U Z : Set X) (hU : IsOpen[inst_1] U) (hZ : IsClosed[inst_1] Z) (hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ)
  (hx : x ∈ U ∩ Z), IntegrableAtFilter f (𝓝[U ∩ Z] x) μ
Tactic: rcases hs with ⟨U, Z, hU, hZ, rfl⟩
Cleared hypotheses: s, hs, hf, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ
have rcases : ∀ (K : Set X) (hK : IsCompact K) (hxK : x ∈ interior K) (hKU : K ⊆ U), IntegrableAtFilter f (𝓝[U ∩ Z] x) μ
Tactic: rcases exists_compact_subset hU hx.1 with ⟨K, hK, hxK, hKU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] 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) μ
have rw : IntegrableAtFilter f (𝓝[Z] x) μ
Tactic: rw [nhdsWithin_inter_of_mem (nhdsWithin_le_nhds <| hU.mem_nhds hx.1)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
inst_4 : PseudoMetrizableSpace ε
inst_5 : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] 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) μ
have refine : IntegrableOn f (Z ∩ K) μ
Tactic: refine ⟨Z ∩ K, inter_mem_nhdsWithin _ (mem_interior_iff_mem_nhds.1 hxK), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
hs : MeasurableSet s
⊢ LocallyIntegrable.{u_1, u_3} (ε := ε) (fun (x : (↑s : Type u_1)) ↦ f (↑x : X))
      (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) ↔
    LocallyIntegrableOn f s μ
have simp_rw : LocallyIntegrable.{u_1, u_3} (ε := ε) (fun (x : (↑s : Type u_1)) ↦ f (↑x : X))
    (Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) μ) ↔
  ∀ (x : { a : X // a ∈ s }), IntegrableAtFilter f (Filter.map (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x)) μ
Tactic: simp_rw [LocallyIntegrableOn, Subtype.forall', ← map_nhds_subtype_val]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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
⊢ LocallyIntegrableOn f univ μ ↔ LocallyIntegrable f μ
have simp : (∀ (x : X), IntegrableAtFilter f (𝓝 x) μ) ↔ LocallyIntegrable f μ
Tactic: simp only [LocallyIntegrableOn, nhdsWithin_univ, mem_univ, true_imp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε : Type u_3
ε' : Type u_4
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
inst_4 : TopologicalSpace ε'
inst_5 : ContinuousENorm ε'
f : X → ε
μ : Measure X
hf : LocallyIntegrable f μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
⊢ LocallyIntegrable g μ
have rw : ∀ (hf : LocallyIntegrableOn f univ μ) {g : X → ε'} (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ),
  LocallyIntegrableOn g univ μ
Tactic: rw [← locallyIntegrableOn_univ] at hf ⊢
Cleared hypotheses: hf, g, hg, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
E : Type u_6
F : Type u_7
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
μ : Measure X
f : X → E
hf : LocallyIntegrable f μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrable g μ
have rw : ∀ (hf : LocallyIntegrableOn f univ μ) {g : X → F} (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖),
  LocallyIntegrableOn g univ μ
Tactic: rw [← locallyIntegrableOn_univ] at hf ⊢
Cleared hypotheses: hf, g, hg, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
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 : LocallyIntegrable f (μ.restrict s)
x : X
h : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x) μ
have obtain : ∀ (t : Set X) (ht_mem : t ∈ 𝓝 x) (ht_int : IntegrableOn f t (μ.restrict s)), IntegrableAtFilter f (𝓝[s] x) μ
Tactic: obtain ⟨t, ht_mem, ht_int⟩ := hf x