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
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩

Premises used: Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_cocompact, And.right, And.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
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
mpr : ∀ (h : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ), IntegrableAtFilter f (cocompact X) μ
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩

Premises used: Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_cocompact, And.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
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
h : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ

Tactic:
h.1.filter_mono cocompact_le_atBot

Premises used: cocompact_le_atBot, And.left, MeasureTheory.IntegrableAtFilter.filter_mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderTop X
inst_7 : CompactIccSpace X
h : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ

Tactic:
exact h.1.filter_mono cocompact_le_atBot

Premises used: cocompact_le_atBot, And.left, MeasureTheory.IntegrableAtFilter.filter_mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
inst_5 : LinearOrder X
inst_6 : OrderBot X
inst_7 : CompactIccSpace X
⊢ Integrable f μ ↔ IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ

Tactic:
integrable_iff_integrableAtFilter_atBot (X := Xᵒᵈ)

Premises used: MeasureTheory.integrable_iff_integrableAtFilter_atBot, Set.Ici, setOf, Filter.atTop, OrderDual
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
⊢ IntegrableOn f (Iic a) μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ

Tactic:
⟨fun h ↦ ⟨⟨Iic a, Iic_mem_atBot a, h⟩, h.locallyIntegrableOn⟩, fun ⟨⟨s, hsl, hs⟩, h⟩ ↦ ?_⟩

Premises used: _private.0.MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot.match_1, MeasureTheory.IntegrableOn.locallyIntegrableOn, MeasureTheory.IntegrableOn, Filter.Iic_mem_atBot, And.intro, Iff.intro, Exists.intro, Set.Iic
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
refine :
  IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ →
    ∀ (s : Set X) (hsl : Membership.mem (γ := Filter X) atBot s) (hs : IntegrableOn f s μ)
      (h : LocallyIntegrableOn f (Iic a) μ), IntegrableOn f (Iic a) μ
⊢ IntegrableOn f (Iic a) μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ

Tactic:
refine ⟨fun h ↦ ⟨⟨Iic a, Iic_mem_atBot a, h⟩, h.locallyIntegrableOn⟩, fun ⟨⟨s, hsl, hs⟩, 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h_1 : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : Membership.mem (γ := Filter X) atBot s
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
⊢ Nonempty X

Tactic:
haveI : Nonempty X := Nonempty.intro a
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h_1 : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : Membership.mem (γ := Filter X) atBot s
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
obtain : ∀ (a' : X) (ha' : ∀ b ≤ a', b ∈ s), IntegrableOn f (Iic a) μ
⊢ IntegrableOn f (Iic a) μ

Tactic:
obtain ⟨a', ha'⟩ := mem_atBot_sets.mp hsl

Premises used: Iff.mp, Filter.mem_atBot_sets
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h_1 : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : Membership.mem (γ := Filter X) atBot s
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Iic a) μ

Tactic:
(integrableOn_union.mpr ⟨hs.mono ha' le_rfl, ?_⟩).mono Iic_subset_Iic_union_Icc le_rfl

Premises used: Iff.mpr, MeasureTheory.integrableOn_union, le_rfl, Set.Iic_subset_Iic_union_Icc, And.intro, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h_1 : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : Membership.mem (γ := Filter X) atBot s
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
refine : IntegrableOn f (Icc a' a) μ
⊢ IntegrableOn f (Iic a) μ

Tactic:
refine (integrableOn_union.mpr ⟨hs.mono ha' le_rfl, ?_⟩).mono Iic_subset_Iic_union_Icc le_rfl

Premises used: Iff.mpr, MeasureTheory.integrableOn_union, le_rfl, Set.Iic_subset_Iic_union_Icc, And.intro, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h_1 : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : Membership.mem (γ := Filter X) atBot s
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Icc a' a) μ

Tactic:
h.integrableOn_compact_subset Icc_subset_Iic_self isCompact_Icc

Premises used: Set.Icc_subset_Iic_self, CompactIccSpace.isCompact_Icc, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
h_1 : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : Membership.mem (γ := Filter X) atBot s
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Icc a' a) μ

Tactic:
exact h.integrableOn_compact_subset Icc_subset_Iic_self isCompact_Icc

Premises used: Set.Icc_subset_Iic_self, CompactIccSpace.isCompact_Icc, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
⊢ IntegrableOn f (Ici a) μ ↔ IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ

Tactic:
integrableOn_Iic_iff_integrableAtFilter_atBot (X := Xᵒᵈ)

Premises used: Set.Ici, setOf, Filter.atTop, MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot, OrderDual
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
mp :
  IntegrableOn f (Iio a) μ →
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ
mpr :
  IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ →
    IntegrableOn f (Iio a) μ
⊢ IntegrableOn f (Iio a) μ ↔
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

Tactic:
constructor
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
h : IntegrableOn f (Iio a) μ
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

Tactic:
⟨⟨Iio a, Iio_mem_atBot a, h⟩, ⟨Iio a, self_mem_nhdsWithin, h⟩, h.locallyIntegrableOn⟩

Premises used: MeasureTheory.IntegrableOn.locallyIntegrableOn, self_mem_nhdsWithin, And.intro, Exists.intro, Filter.Iio_mem_atBot, Set.Iio
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
h : IntegrableOn f (Iio a) μ
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

Tactic:
exact ⟨⟨Iio a, Iio_mem_atBot a, h⟩, ⟨Iio a, self_mem_nhdsWithin, h⟩, h.locallyIntegrableOn⟩
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
mpr : ∀ (s' : X) (hs'_mono : s' ∈ Iio a) (hs' : Ioo s' a ⊆ s), IntegrableOn f (Iio a) μ
⊢ IntegrableOn f (Iio a) μ

Tactic:
obtain ⟨s', ⟨hs'_mono, hs'⟩⟩ := mem_nhdsLT_iff_exists_Ioo_subset.mp hsl

Premises used: mem_nhdsLT_iff_exists_Ioo_subset, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iio a) μ

Tactic:
(integrableOn_union.mpr ⟨?_, hs.mono hs' le_rfl⟩).mono Iio_subset_Iic_union_Ioo le_rfl

Premises used: Iff.mpr, MeasureTheory.integrableOn_union, le_rfl, And.intro, MeasureTheory.IntegrableOn.mono, Set.Iio_subset_Iic_union_Ioo
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
mpr : IntegrableOn f (Iic s') μ
⊢ IntegrableOn f (Iio a) μ

Tactic:
refine (integrableOn_union.mpr ⟨?_, hs.mono hs' le_rfl⟩).mono Iio_subset_Iic_union_Ioo le_rfl

Premises used: Iff.mpr, MeasureTheory.integrableOn_union, le_rfl, And.intro, MeasureTheory.IntegrableOn.mono, Set.Iio_subset_Iic_union_Ioo
-- 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
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iic s') μ

Tactic:
integrableOn_Iic_iff_integrableAtFilter_atBot.mpr
      ⟨hbot, hlocal.mono_set (Iic_subset_Iio.mpr hs'_mono)⟩

Premises used: Iff.mpr, Set.Iic_subset_Iio, And.intro, MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot, MeasureTheory.LocallyIntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMinOrder X
inst_8 : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iic s') μ

Tactic:
exact integrableOn_Iic_iff_integrableAtFilter_atBot.mpr
      ⟨hbot, hlocal.mono_set (Iic_subset_Iio.mpr hs'_mono)⟩

Premises used: Iff.mpr, Set.Iic_subset_Iio, And.intro, MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot, MeasureTheory.LocallyIntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Function.LocallyIntegrable
Goal:
X : Type u_1
ε : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : X → ε
μ : Measure X
inst_4 : PseudoMetrizableSpace ε
a : X
inst_5 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : NoMaxOrder X
inst_8 : OrderTopology X
⊢ IntegrableOn f (Ioi a) μ ↔
    IntegrableAtFilter f atTop μ ∧ IntegrableAtFilter f (𝓝[>] a) μ ∧ LocallyIntegrableOn f (Ioi a) μ

Tactic:
integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin (X := Xᵒᵈ)

Premises used: Set.Ioi, Set.Ici, setOf, Filter.atTop, MeasureTheory.integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin, OrderDual
-- 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 : OpensMeasurableSpace X
f : X → E
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : SecondCountableTopologyEither X E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ LocallyIntegrable f μ

Tactic:
hf.integrableAt_nhds

Premises used: MeasureTheory.LocallyIntegrable, Continuous.integrableAt_nhds
-- 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 : OpensMeasurableSpace X
K : Set X
f : X → E
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : SecondCountableTopologyEither X E
hf : ContinuousOn f K
hK : MeasurableSet K
⊢ LocallyIntegrableOn f K μ

Tactic:
fun _x hx =>
  hf.integrableAt_nhdsWithin hK hx

Premises used: ContinuousOn.integrableAt_nhdsWithin, MeasureTheory.LocallyIntegrableOn
-- 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 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn f s μ

Tactic:
⟨hf.aestronglyMeasurable_of_subset_isCompact hK hs h's, ?_⟩

Premises used: ContinuousOn.aestronglyMeasurable_of_subset_isCompact, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, And.intro
-- 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 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : HasFiniteIntegral f (μ.restrict s)
⊢ IntegrableOn f s μ

Tactic:
refine ⟨hf.aestronglyMeasurable_of_subset_isCompact hK hs h's, ?_⟩
-- 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 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : Fact (μ s < ∞) := ⟨mus.lt_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
s : Set X
inst_3 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ∃ (C : ℝ), ∀ x ∈ f '' K, ‖x‖ ≤ C

Tactic:
IsBounded.exists_norm_le (hK.image_of_continuousOn hf).isBounded

Premises used: IsCompact.isBounded, IsCompact.image_of_continuousOn, Bornology.IsBounded.exists_norm_le
-- 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 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
obtain : ∀ (C : ℝ) (hC : ∀ x ∈ f '' K, ‖x‖ ≤ C), HasFiniteIntegral f (μ.restrict s)
⊢ HasFiniteIntegral f (μ.restrict s)

Tactic:
obtain ⟨C, hC⟩ : ∃ C, ∀ x ∈ f '' K, ‖x‖ ≤ C :=
    IsBounded.exists_norm_le (hK.image_of_continuousOn hf).isBounded

Premises used: IsCompact.isBounded, IsCompact.image_of_continuousOn, Bornology.IsBounded.exists_norm_le
-- 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 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
apply : ∀ᵐ (a : X) ∂μ.restrict s, ‖f a‖ ≤ C
⊢ HasFiniteIntegral f (μ.restrict s)

Tactic:
apply HasFiniteIntegral.of_bounded (C := C)

Premises used: MeasureTheory.HasFiniteIntegral.of_bounded
-- 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 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
a : X
ha : a ∈ s
⊢ ‖f a‖ ≤ C

Tactic:
hC _ (mem_image_of_mem f (h's ha))

Premises used: Set.mem_image_of_mem
-- 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 : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ s) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ ‖f a‖ ≤ C) x} x}
      a
h₁ h₂ : ∀ (a : X) (ha : a ∈ s), ‖f a‖ ≤ C
⊢ ∀ᵐ (a : X) ∂μ.restrict s, ‖f a‖ ≤ C

Tactic:
filter_upwards [ae_restrict_mem hs] with a ha using hC _ (mem_image_of_mem f (h's ha))

Premises used: MeasureTheory.ae_restrict_mem
-- 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 : OpensMeasurableSpace X
K : Set X
f : X → E
inst_4 : IsFiniteMeasureOnCompacts μ
hK : IsCompact K
h'K : MeasurableSet K
hf : ContinuousOn f K
⊢ IntegrableOn f K μ

Tactic:
hf.integrableOn_of_subset_isCompact hK h'K Subset.rfl hK.measure_ne_top

Premises used: ContinuousOn.integrableOn_of_subset_isCompact, Set.Subset.rfl, IsCompact.measure_ne_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 : OpensMeasurableSpace X
K : Set X
f : X → E
inst_4 : IsFiniteMeasureOnCompacts μ
inst_5 : T2Space X
hK : IsCompact K
hf : ContinuousOn f K
⊢ IntegrableOn f K μ

Tactic:
hf.integrableOn_compact' hK hK.measurableSet

Premises used: ContinuousOn.integrableOn_compact', IsCompact.measurableSet
-- 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 : OpensMeasurableSpace X
f : X → E
a b : X
inst_4 : IsFiniteMeasureOnCompacts μ
inst_5 : Preorder X
inst_6 : CompactIccSpace X
inst_7 : T2Space X
hf : ContinuousOn f (Icc a b)
⊢ IntegrableOn f (Icc a b) μ

Tactic:
hf.integrableOn_compact isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, ContinuousOn.integrableOn_compact