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 ε
μ : Measure X
inst_4 : IsLocallyFiniteMeasure μ
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ LocallyIntegrable.{u_1, u_3} (ε := ε) (fun (x : X) ↦ c) μ

Tactic:
(memLp_top_const_enorm hc).locallyIntegrable le_top

Premises used: MeasureTheory.MemLp.locallyIntegrable, MeasureTheory.memLp_top_const_enorm, le_top
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
inst_3 : IsLocallyFiniteMeasure μ
c : E
⊢ LocallyIntegrable.{u_1, u_6} (ε := E) (fun (x : X) ↦ c) μ

Tactic:
locallyIntegrable_const_enorm enorm_ne_top

Premises used: enorm_ne_top, MeasureTheory.locallyIntegrable_const_enorm
-- 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 ε
μ : Measure X
s : Set X
inst_4 : IsLocallyFiniteMeasure μ
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ LocallyIntegrableOn.{u_1, u_3} (ε := ε) (fun (x : X) ↦ c) s μ

Tactic:
(locallyIntegrable_const_enorm hc).locallyIntegrableOn s

Premises used: MeasureTheory.LocallyIntegrable.locallyIntegrableOn, MeasureTheory.locallyIntegrable_const_enorm
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
s : Set X
inst_3 : IsLocallyFiniteMeasure μ
c : E
⊢ LocallyIntegrableOn.{u_1, u_6} (ε := E) (fun (x : X) ↦ c) s μ

Tactic:
locallyIntegrableOn_const_enorm enorm_ne_top

Premises used: MeasureTheory.locallyIntegrableOn_const_enorm, enorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
⊢ LocallyIntegrable.{u_1, u_5} (ε := ε'') (fun (x : X) ↦ 0) μ

Tactic:
(integrable_zero X ε'' μ).locallyIntegrable

Premises used: MeasureTheory.integrable_zero, MeasureTheory.Integrable.locallyIntegrable
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
s : Set X
⊢ LocallyIntegrableOn.{u_1, u_5} (ε := ε'') (fun (x : X) ↦ 0) s μ

Tactic:
locallyIntegrable_zero.locallyIntegrableOn s

Premises used: MeasureTheory.LocallyIntegrable.locallyIntegrableOn, MeasureTheory.locallyIntegrable_zero
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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
rcases : ∀ (U : Set X) (hU : U ∈ 𝓝 x) (h'U : IntegrableOn f U μ), IntegrableAtFilter (s.indicator f) (𝓝 x) μ
⊢ IntegrableAtFilter (s.indicator f) (𝓝 x) μ

Tactic:
rcases hf x with ⟨U, hU, h'U⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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
U : Set X
hU : U ∈ 𝓝 x
h'U : IntegrableOn f U μ
⊢ IntegrableAtFilter (s.indicator f) (𝓝 x) μ

Tactic:
⟨U, hU, h'U.indicator hs⟩

Premises used: MeasureTheory.IntegrableOn.indicator, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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
U : Set X
hU : U ∈ 𝓝 x
h'U : IntegrableOn f U μ
⊢ IntegrableAtFilter (s.indicator f) (𝓝 x) μ

Tactic:
exact ⟨U, hU, h'U.indicator hs⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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)) μ

Tactic:
⟨fun h x => ?_, fun h x => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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) μ
refine_2 :
  ∀ (h : LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ) (x : Y),
    IntegrableAtFilter (mα := inst_2) f (𝓝 x) (Measure.map (⇑e : (a : X) → Y) μ)
⊢ LocallyIntegrable f (Measure.map (⇑e : (a : X) → Y) μ) ↔ LocallyIntegrable (f ∘ (⇑e : (a : X) → Y)) μ

Tactic:
refine ⟨fun h x => ?_, fun h x => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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
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) μ
⊢ IntegrableAtFilter (f ∘ (⇑e : (a : X) → Y)) (𝓝 x) μ

Tactic:
rcases h (e x) with ⟨U, hU, h'U⟩

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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) μ

Tactic:
⟨e ⁻¹' U, e.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩

Premises used: Homeomorph.continuous, ContinuousAt.preimage_mem_nhds, Continuous.continuousAt, MeasureTheory.IntegrableAtFilter, Set.preimage, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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) μ)
refine_1 : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) ((⇑e : (a : X) → Y) ⁻¹' U) μ
⊢ IntegrableAtFilter (f ∘ (⇑e : (a : X) → Y)) (𝓝 x) μ

Tactic:
refine ⟨e ⁻¹' U, e.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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) μ)
⊢ IntegrableOn (f ∘ (⇑e : (a : X) → Y)) ((⇑e : (a : X) → Y) ⁻¹' U) μ

Tactic:
(integrableOn_map_equiv e.toMeasurableEquiv).1 h'U

Premises used: Homeomorph.toMeasurableEquiv, MeasureTheory.integrableOn_map_equiv, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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) μ)
⊢ IntegrableOn (f ∘ (⇑e : (a : X) → Y)) ((⇑e : (a : X) → Y) ⁻¹' U) μ

Tactic:
exact (integrableOn_map_equiv e.toMeasurableEquiv).1 h'U

Premises used: Homeomorph.toMeasurableEquiv, MeasureTheory.integrableOn_map_equiv, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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
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) μ)
⊢ IntegrableAtFilter (mα := inst_2) f (𝓝 x) (Measure.map (⇑e : (a : X) → Y) μ)

Tactic:
rcases h (e.symm x) with ⟨U, hU, h'U⟩

Premises used: Homeomorph.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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) μ)

Tactic:
⟨e.symm ⁻¹' U, e.symm.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩

Premises used: Homeomorph.continuous, ContinuousAt.preimage_mem_nhds, Continuous.continuousAt, MeasureTheory.IntegrableAtFilter, Set.preimage, Homeomorph.symm, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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 μ
refine_2 : IntegrableOn (mα := inst_2) f ((⇑e.symm : (a : Y) → X) ⁻¹' U) (Measure.map (⇑e : (a : X) → Y) μ)
⊢ IntegrableAtFilter (mα := inst_2) f (𝓝 x) (Measure.map (⇑e : (a : X) → Y) μ)

Tactic:
refine ⟨e.symm ⁻¹' U, e.symm.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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 μ
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)) μ
⊢ IntegrableOn (mα := inst_2) f ((⇑e.symm : (a : Y) → X) ⁻¹' U) (Measure.map (⇑e : (a : X) → Y) μ)

Tactic:
apply (integrableOn_map_equiv e.toMeasurableEquiv).2

Premises used: Iff.mpr, Homeomorph.toMeasurableEquiv, MeasureTheory.integrableOn_map_equiv
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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 μ
refine_2 :
  IntegrableOn (f ∘ (⇑e : (a : X) → Y))
    (preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' 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)) μ

Tactic:
simp only [Homeomorph.toMeasurableEquiv_coe]

Premises used: Homeomorph.toMeasurableEquiv_coe
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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)) U μ

Tactic:
h'U
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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 μ
h₁ : preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U) = U
⊢ IntegrableOn (f ∘ (⇑e : (a : X) → Y))
    (preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U)) μ

Tactic:
convert! h'U
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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 μ
h₁ :
  ∀ (x : X),
    Membership.mem (γ := Set X) (preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U)) x ↔
      x ∈ U
⊢ preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U) = U

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
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_1 : Y
U : Set X
hU : Membership.mem (γ := Filter X) (𝓝 ((e.symm : (a : Y) → X) x_1) : Filter X) U
h'U : IntegrableOn (f ∘ (⇑e : (a : X) → Y)) U μ
x : X
⊢ Membership.mem (γ := Set X) (preimage.{u_1, u_2} (β := Y) (⇑e : (a : X) → Y) ((⇑e.symm : (a : Y) → X) ⁻¹' U)) x ↔
    x ∈ U

Tactic:
simp only [mem_preimage, Homeomorph.symm_apply_apply]

Premises used: Homeomorph.symm_apply_apply, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε'' : Type u_5
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε''
inst_3 : ESeminormedAddMonoid ε''
μ : Measure X
inst_4 : ContinuousAdd ε''
f g : X → ε''
hf : LocallyIntegrable f μ
hg : LocallyIntegrable g μ
⊢ LocallyIntegrable (f + g) μ

Tactic:
fun x ↦ (hf x).add (hg x)

Premises used: MeasureTheory.LocallyIntegrable, MeasureTheory.IntegrableAtFilter.add
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
f g : X → E
hf : LocallyIntegrable f μ
hg : LocallyIntegrable g μ
⊢ LocallyIntegrable (f - g) μ

Tactic:
fun x ↦ (hf x).sub (hg x)

Premises used: MeasureTheory.LocallyIntegrable, MeasureTheory.IntegrableAtFilter.sub
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
f : X → E
hf : LocallyIntegrable f μ
⊢ LocallyIntegrable (-f) μ

Tactic:
fun x ↦ (hf x).neg

Premises used: MeasureTheory.LocallyIntegrable, MeasureTheory.IntegrableAtFilter.neg
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
f : X → E
⊢ LocallyIntegrable (-f) μ ↔ LocallyIntegrable f μ

Tactic:
simp [← locallyIntegrableOn_univ]

Premises used: MeasureTheory.locallyIntegrableOn_univ
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
f : X → E
𝕜 : Type u_9
inst_3 : NormedAddCommGroup 𝕜
inst_4 : SMulZeroClass 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
hf : LocallyIntegrable f μ
c : 𝕜
⊢ LocallyIntegrable (c • f) μ

Tactic:
fun x ↦ (hf x).smul c

Premises used: MeasureTheory.IntegrableAtFilter.smul, MeasureTheory.LocallyIntegrable
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 E
f : X → E
c : 𝕜
⊢ LocallyIntegrable (c • f) μ ↔ c = 0 ∨ LocallyIntegrable f μ

Tactic:
simp [← locallyIntegrableOn_univ]

Premises used: MeasureTheory.locallyIntegrableOn_univ
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
ε''' : Type u_9
inst_2 : TopologicalSpace ε'''
inst_3 : ESeminormedAddCommMonoid ε'''
inst_4 : ContinuousAdd ε'''
ι : Type u_10
s : Finset ι
f : ι → X → ε'''
hf : ∀ i ∈ s, LocallyIntegrable (f i) μ
⊢ LocallyIntegrable.{u_1, u_9} (ε := ε''') (∑ i ∈ s, f i) μ

Tactic:
Finset.sum_induction f (fun g => LocallyIntegrable g μ) (fun _ _ => LocallyIntegrable.add)
    locallyIntegrable_zero hf

Premises used: MeasureTheory.LocallyIntegrable, MeasureTheory.LocallyIntegrable.add, Finset.sum_induction, MeasureTheory.locallyIntegrable_zero
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
ε''' : Type u_9
inst_2 : TopologicalSpace ε'''
inst_3 : ESeminormedAddCommMonoid ε'''
inst_4 : ContinuousAdd ε'''
ι : Type u_10
s : Finset ι
f : ι → X → ε'''
hf : ∀ i ∈ s, LocallyIntegrable (f i) μ
⊢ LocallyIntegrable.{u_1, u_9} (ε := ε''') (fun (a : X) ↦ ∑ i ∈ s, f i a) μ

Tactic:
simpa only [← Finset.sum_apply] using locallyIntegrable_finsetSum' s hf

Premises used: Finset.sum_apply, MeasureTheory.locallyIntegrable_finsetSum'
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
⊢ IsCompact K

Tactic:
have hK : IsCompact K := h'g
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
apply : (support.{u_1, u_6} (M := E) fun (x : X) ↦ g x • f x) ⊆ K
⊢ Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x

Tactic:
apply indicator_eq_self.2

Premises used: Iff.mpr, Set.indicator_eq_self
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
apply : ∀ x ∉ K, g x • f x = 0
⊢ (support.{u_1, u_6} (M := E) fun (x : X) ↦ g x • f x) ⊆ K

Tactic:
apply support_subset_iff'.2

Premises used: Iff.mpr, Function.support_subset_iff'
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
x : X
hx : x ∉ K
⊢ g x • f x = 0

Tactic:
simp [image_eq_zero_of_notMem_tsupport hx]

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
E : Type u_6
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
inst_6 : OpensMeasurableSpace X
inst_7 : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ Eq (α := (x : X) → E) (K.indicator fun (x : X) ↦ g x • f x) fun (x : X) ↦ g x • f x

Tactic:
have : K.indicator (fun x ↦ g x • f x) = (fun x ↦ g x • f x) := by
    apply indicator_eq_self.2
    apply support_subset_iff'.2
    intro x hx
    simp [image_eq_zero_of_notMem_tsupport hx]