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 : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
x : X
h : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝[s] x) μ
have obtain : ∀ (u : Set X) (hu_sub : u ⊆ t) (hu_o : IsOpen[inst_1] u) (hu_mem : x ∈ u), IntegrableAtFilter f (𝓝[s] x) μ
Tactic: obtain ⟨u, hu_sub, hu_o, hu_mem⟩ := mem_nhds_iff.mp ht_mem
-- 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
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t (μ.restrict s)
u : Set X
hu_sub : u ⊆ t
hu_o : IsOpen[inst_1] u
hu_mem : x ∈ u
⊢ IntegrableAtFilter f (𝓝[s] x) μ
have refine : IntegrableOn f (s ∩ u) μ
Tactic: refine ⟨_, inter_mem_nhdsWithin s (hu_o.mem_nhds hu_mem), ?_⟩
-- 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
hs : IsClosed[inst_1] s
⊢ LocallyIntegrableOn f s μ ↔ LocallyIntegrable f (μ.restrict s)
have refine : ∀ (hf : LocallyIntegrableOn f s μ) (x : X), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
Tactic: refine ⟨fun hf x => ?_, locallyIntegrableOn_of_locallyIntegrable_restrict⟩
-- 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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
have pos : ∀ (h : x ∈ s), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
Tactic: by_cases h : x ∈ s
-- 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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
pos : ∀ (h : x ∈ s), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
have neg : ∀ (h : x ∉ s), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
Tactic: by_cases h : x ∈ s
-- 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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
have pos : ∀ (t : Set X) (ht_nhds : t ∈ 𝓝[s] x) (ht_int : IntegrableOn f t μ), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
Tactic: obtain ⟨t, ht_nhds, ht_int⟩ := hf x 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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
have pos : ∀ (u : Set X) (hu_o : IsOpen[inst_1] u) (hu_x : x ∈ u) (hu_sub : u ∩ s ⊆ t), IntegrableAtFilter f (𝓝 x) (μ.restrict s)
Tactic: obtain ⟨u, hu_o, hu_x, hu_sub⟩ := mem_nhdsWithin.mp ht_nhds
-- 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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst_1] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
have pos : IntegrableOn f u (μ.restrict s)
Tactic: refine ⟨u, hu_o.mem_nhds hu_x, ?_⟩
-- 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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst_1] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ IntegrableOn f u (μ.restrict s)
have pos : Integrable f (μ.restrict (u ∩ s))
Tactic: rw [IntegrableOn, restrict_restrict hu_o.measurableSet]
-- 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
hs : IsClosed[inst_1] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
have neg : ∀ (hs : IsOpen[inst_1] sᶜ) (hf : LocallyIntegrableOn f s μ) (x : X) (h : x ∉ s),
  IntegrableAtFilter f (𝓝 x) (μ.restrict s)
Tactic: rw [← isOpen_compl_iff] at hs
Cleared hypotheses: hs, hf, x, 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
hs : IsOpen[inst_1] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
have neg : IntegrableOn f sᶜ (μ.restrict s)
Tactic: refine ⟨sᶜ, hs.mem_nhds 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
hs : IsOpen[inst_1] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableOn f sᶜ (μ.restrict s)
have neg : IntegrableOn f ∅ μ
Tactic: rw [IntegrableOn, restrict_restrict, inter_comm, inter_compl_self, ← IntegrableOn]
-- 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
hs : IsOpen[inst_1] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
neg : IntegrableOn f ∅ μ
⊢ IntegrableOn f sᶜ (μ.restrict s)
have neg₁ : MeasurableSet sᶜ
Tactic: rw [IntegrableOn, restrict_restrict, inter_comm, inter_compl_self, ← IntegrableOn]
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ k ⊆ u ∧ IntegrableOn f u μ
have refine_1 : ∃ (u : Set X), IsOpen[inst_1] u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ
Tactic: refine IsCompact.induction_on hk ?_ ?_ ?_ ?_
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
refine_1 : ∃ (u : Set X), IsOpen[inst_1] u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ k ⊆ u ∧ IntegrableOn f u μ
have refine_2 : ∀ ⦃s t : Set X⦄,
  s ⊆ t →
    (∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ) →
      ∃ (u : Set X), IsOpen[inst_1] u ∧ s ⊆ u ∧ IntegrableOn f u μ
Tactic: refine IsCompact.induction_on hk ?_ ?_ ?_ ?_
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
refine_1 : ∃ (u : Set X), IsOpen[inst_1] u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ
refine_2 :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t →
      (∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ) →
        ∃ (u : Set X), IsOpen[inst_1] u ∧ s ⊆ u ∧ IntegrableOn f u μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ k ⊆ u ∧ IntegrableOn f u μ
have refine_3 : ∀ ⦃s t : Set X⦄,
  (∃ (u : Set X), IsOpen[inst_1] u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
    (∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ) →
      ∃ (u : Set X), IsOpen[inst_1] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ
Tactic: refine IsCompact.induction_on hk ?_ ?_ ?_ ?_
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
refine_1 : ∃ (u : Set X), IsOpen[inst_1] u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ
refine_2 :
  ∀ ⦃s t : Set X⦄,
    s ⊆ t →
      (∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ) →
        ∃ (u : Set X), IsOpen[inst_1] u ∧ s ⊆ u ∧ IntegrableOn f u μ
refine_3 :
  ∀ ⦃s t : Set X⦄,
    (∃ (u : Set X), IsOpen[inst_1] u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
      (∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ) →
        ∃ (u : Set X), IsOpen[inst_1] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ k ⊆ u ∧ IntegrableOn f u μ
have refine_4 : ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ
Tactic: refine IsCompact.induction_on hk ?_ ?_ ?_ ?_
-- 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 ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
h : x ∈ k
⊢ ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ
have refine_4 : ∀ (u : Set X) (ux : u ∈ 𝓝 x) (hu : IntegrableOn f u μ),
  ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ
Tactic: rcases hf x with ⟨u, ux, 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
inst_4 : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
x : X
h : x ∈ k
u : Set X
ux : u ∈ 𝓝 x
hu : IntegrableOn f u μ
⊢ ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ
have refine_4 : ∀ (v : Set X) (vu : v ⊆ u) (v_open : IsOpen[inst_1] v) (xv : x ∈ v),
  ∃ t ∈ 𝓝[k] x, ∃ (u : Set X), IsOpen[inst_1] u ∧ t ⊆ u ∧ IntegrableOn f u μ
Tactic: rcases mem_nhds_iff.1 ux with ⟨v, vu, v_open, xv⟩
-- 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 : SecondCountableTopology X
hf : LocallyIntegrable f μ
⊢ ∃ (u : ℕ → Set X),
    (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧
      Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), u n) univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ
have rcases : ∀ (u : ℕ → Set X) (u_open : ∀ (n : ℕ), IsOpen[inst_1] (u n)) (u_union : Subset.{u_1} (α := Set X) univ (⋃ (n : ℕ), u n))
  (hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ),
  ∃ (u : ℕ → Set X),
    (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧
      Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), u n) univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ
Tactic: rcases (hf.locallyIntegrableOn univ).exists_nat_integrableOn with ⟨u, u_open, u_union, 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
inst_4 : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen[inst_1] (u n)
u_union : Subset.{u_1} (α := Set X) univ (⋃ (n : ℕ), u n)
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
⊢ ∃ (u : ℕ → Set X),
    (∀ (n : ℕ), IsOpen[inst_1] (u n)) ∧
      Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), u n) univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ
have refine : ∀ (n : ℕ), IntegrableOn f (u n) μ
Tactic: refine ⟨u, u_open, eq_univ_of_univ_subset u_union, fun 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
inst_4 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
⊢ IntegrableAtFilter f (𝓝 x) μ
have rcases : ∀ (U : Set X) (hU : U ∈ 𝓝 x) (h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)),
  IntegrableAtFilter f (𝓝 x) μ
Tactic: rcases μ.finiteAt_nhds x with ⟨U, hU, h'U⟩
-- 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
inst_4 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableAtFilter f (𝓝 x) μ
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (μ U < ⊤) := ⟨h'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
inst_4 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ IntegrableAtFilter f (𝓝 x) μ
have refine : IntegrableOn f U μ
Tactic: refine ⟨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
inst_4 : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ IntegrableOn f U μ
have rw : MemLp f 1 (μ.restrict U)
Tactic: rw [IntegrableOn, ← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
f : X → ε''
hf : LocallyIntegrable f μ
s : Set X
hs : MeasurableSet s
x : X
⊢ IntegrableAtFilter (s.indicator f) (𝓝 x) μ
have rcases : ∀ (U : Set X) (hU : U ∈ 𝓝 x) (h'U : IntegrableOn f U μ), IntegrableAtFilter (s.indicator f) (𝓝 x) μ
Tactic: rcases hf x with ⟨U, hU, h'U⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
⊢ LocallyIntegrable f (Measure.map (⇑e : (a : X) → Y) μ) ↔ LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ
have refine_1 : ∀ (h : LocallyIntegrable f (Measure.map (⇑e : (a : X) → Y) μ)) (x : X),
  IntegrableAtFilter (f ∘ (⇑e : (a : X) → Y)) (𝓝 x) μ
Tactic: refine ⟨fun h x => ?_, fun h x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
refine_1 :
  ∀ (h : LocallyIntegrable f (Measure.map (⇑e : (a : X) → Y) μ)) (x : X),
    IntegrableAtFilter (f ∘ (⇑e : (a : X) → Y)) (𝓝 x) μ
⊢ LocallyIntegrable f (Measure.map (⇑e : (a : X) → Y) μ) ↔ LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ
have refine_2 : ∀ (h : LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ) (x : Y),
  IntegrableAtFilter (mα := inst_2) f (𝓝 x) (Measure.map (⇑e : (a : X) → Y) μ)
Tactic: refine ⟨fun h x => ?_, fun h x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable f (Measure.map (⇑e : (a : X) → Y) μ)
x : X
⊢ IntegrableAtFilter (f ∘ (⇑e : (a : X) → Y)) (𝓝 x) μ
have refine_1 : ∀ (U : Set Y) (hU : Membership.mem (γ := Filter Y) (𝓝 ((e : (a : X) → Y) x) : Filter Y) U)
  (h'U : IntegrableOn (mα := inst_2) f U (Measure.map (⇑e : (a : X) → Y) μ)),
  IntegrableAtFilter (f ∘ (⇑e : (a : X) → Y)) (𝓝 x) μ
Tactic: rcases h (e x) with ⟨U, hU, h'U⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable f (Measure.map (⇑e : (a : X) → Y) μ)
x : X
U : Set Y
hU : Membership.mem (γ := Filter Y) (𝓝 ((e : (a : X) → Y) x) : Filter Y) U
h'U : IntegrableOn (mα := inst_2) f U (Measure.map (⇑e : (a : X) → Y) μ)
⊢ IntegrableAtFilter (f ∘ (⇑e : (a : X) → Y)) (𝓝 x) μ
have refine_1 : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) ((⇑e : (a : X) → Y) ⁻¹' U) μ
Tactic: refine ⟨e ⁻¹' U, e.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ
x : Y
⊢ IntegrableAtFilter (mα := inst_2) f (𝓝 x) (Measure.map (⇑e : (a : X) → Y) μ)
have refine_2 : ∀ (U : Set X) (hU : Membership.mem (γ := Filter X) (𝓝 ((e.symm : (a : Y) → X) x) : Filter X) U)
  (h'U : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) U μ),
  IntegrableAtFilter (mα := inst_2) f (𝓝 x) (Measure.map (⇑e : (a : X) → Y) μ)
Tactic: rcases h (e.symm x) with ⟨U, hU, h'U⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ
x : Y
U : Set X
hU : Membership.mem (γ := Filter X) (𝓝 ((e.symm : (a : Y) → X) x) : Filter X) U
h'U : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) U μ
⊢ IntegrableAtFilter (mα := inst_2) f (𝓝 x) (Measure.map (⇑e : (a : X) → Y) μ)
have refine_2 : IntegrableOn (mα := inst_2) f ((⇑e.symm : (a : Y) → X) ⁻¹' U) (Measure.map (⇑e : (a : X) → Y) μ)
Tactic: refine ⟨e.symm ⁻¹' U, e.symm.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ
x : Y
U : Set X
hU : Membership.mem (γ := Filter X) (𝓝 ((e.symm : (a : Y) → X) x) : Filter X) U
h'U : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) U μ
⊢ IntegrableOn (mα := inst_2) f ((⇑e.symm : (a : Y) → X) ⁻¹' U) (Measure.map (⇑e : (a : X) → Y) μ)
have refine_2 : IntegrableOn (f ∘ (⇑e.toMeasurableEquiv : (a : X) → Y))
  (preimage.{u_1, u_2} (β := Y) (⇑e.toMeasurableEquiv : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U)) μ
Tactic: apply (integrableOn_map_equiv e.toMeasurableEquiv).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ
x : Y
U : Set X
hU : Membership.mem (γ := Filter X) (𝓝 ((e.symm : (a : Y) → X) x) : Filter X) U
h'U : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) U μ
⊢ IntegrableOn (f ∘ (⇑e.toMeasurableEquiv : (a : X) → Y))
    (preimage.{u_1, u_2} (β := Y) (⇑e.toMeasurableEquiv : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U)) μ
have refine_2 : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) (preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U))
  μ
Tactic: simp only [Homeomorph.toMeasurableEquiv_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LocallyIntegrable (goal)
Goal:
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace Y
inst_3 : TopologicalSpace Y
inst_4 : TopologicalSpace ε''
inst_5 : ESeminormedAddMonoid ε''
inst_6 : BorelSpace X
inst_7 : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ
x : Y
U : Set X
hU : Membership.mem (γ := Filter X) (𝓝 ((e.symm : (a : Y) → X) x) : Filter X) U
h'U : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) U μ
⊢ IntegrableOn (f ∘ (⇑e : (a : X) → Y))
    (preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U)) μ
have h₁ : preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U) = U
Tactic: convert! h'U