awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ IntegrableOn f (Icc a b) μ

Tactic:
hf.continuousOn.integrableOn_Icc

Premises used: Continuous.continuousOn, ContinuousOn.integrableOn_Icc
-- 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 : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ IntegrableOn f (Ioc a b) μ

Tactic:
hf.integrableOn_Icc.mono_set Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.mono_set, Continuous.integrableOn_Icc
-- 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 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : T2Space X
hf : ContinuousOn f [[a, b]]
⊢ IntegrableOn f [[a, b]] μ

Tactic:
hf.integrableOn_Icc

Premises used: ContinuousOn.integrableOn_Icc, Set.uIcc
-- 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 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : T2Space X
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ IntegrableOn f [[a, b]] μ

Tactic:
hf.integrableOn_Icc

Premises used: Set.uIcc, Continuous.integrableOn_Icc
-- 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 : LinearOrder X
inst_6 : CompactIccSpace X
inst_7 : T2Space X
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ IntegrableOn f (Ι a b) μ

Tactic:
hf.integrableOn_Ioc

Premises used: Set.uIoc, Continuous.integrableOn_Ioc
-- 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 : IsFiniteMeasureOnCompacts μ
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hcf : HasCompactSupport f
⊢ Integrable f μ

Tactic:
(integrableOn_iff_integrable_of_support_subset (subset_tsupport f)).mp <|
    hf.continuousOn.integrableOn_compact' hcf (isClosed_tsupport _).measurableSet

Premises used: Continuous.continuousOn, subset_tsupport, MeasureTheory.integrableOn_iff_integrable_of_support_subset, IsClosed.measurableSet, isClosed_tsupport, Iff.mp, ContinuousOn.integrableOn_compact'
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ BddBelow (f '' s)

Tactic:
have hbelow : BddBelow (f '' s) := ⟨f a, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono ha.1 hy (ha.2 hy)⟩
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hbelow : BddBelow (f '' s)
⊢ BddAbove (f '' s)

Tactic:
have habove : BddAbove (f '' s) := ⟨f b, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono hy hb.1 (hb.2 hy)⟩
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
⊢ Bornology.IsBounded (f '' s)

Tactic:
have : IsBounded (f '' s) := Metric.isBounded_of_bddAbove_of_bddBelow habove hbelow
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
rcases : ∀ (C : ℝ) (hC : ∀ x ∈ f '' s, ‖x‖ ≤ C), MemLp f ∞ (μ.restrict s)
⊢ MemLp f ∞ (μ.restrict s)

Tactic:
rcases isBounded_iff_forall_norm_le.mp this with ⟨C, hC⟩

Premises used: isBounded_iff_forall_norm_le, Iff.mp
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
⊢ MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)

Tactic:
have A : MemLp (fun _ => C) ⊤ (μ.restrict s) := memLp_top_const _
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)
apply : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ ‖C‖
⊢ MemLp f ∞ (μ.restrict s)

Tactic:
apply MemLp.mono A (aemeasurable_restrict_of_monotoneOn h's hmono).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, aemeasurable_restrict_of_monotoneOn, MeasureTheory.MemLp.mono
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)
apply : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ ‖C‖
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ ‖C‖

Tactic:
apply (ae_restrict_iff' h's).mpr

Premises used: Iff.mpr, MeasureTheory.ae_restrict_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
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)
apply : ∀ (y : X) (hy : y ∈ s), ‖f y‖ ≤ ‖C‖
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ ‖C‖

Tactic:
apply ae_of_all _ fun y hy ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)
y : X
hy : y ∈ s
⊢ ‖f y‖ ≤ ‖C‖

Tactic:
(hC _ (mem_image_of_mem f hy)).trans (le_abs_self _)

Premises used: le_abs_self, Set.mem_image_of_mem, LE.le.trans
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : Bornology.IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (ε := ℝ) (fun (x : X) ↦ C) ∞ (μ.restrict s)
y : X
hy : y ∈ s
⊢ ‖f y‖ ≤ ‖C‖

Tactic:
exact (hC _ (mem_image_of_mem f hy)).trans (le_abs_self _)

Premises used: le_abs_self, Set.mem_image_of_mem, LE.le.trans
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : MeasurableSet s
⊢ ∀ x ∉ univ, f x = 0

Tactic:
simp
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : MeasurableSet s
⊢ Ne (α := ℝ≥0∞) ((μ.restrict s : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa using hs
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst_9 : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
inl : ∀ (hs : IsCompact.{u_1} (X := X) ∅) (hmono : MonotoneOn f ∅), MemLp f p (μ.restrict ∅)
inr : ∀ (h : s.Nonempty), MemLp f p (μ.restrict s)
⊢ MemLp f p (μ.restrict s)

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst_9 : IsFiniteMeasureOnCompacts μ
hs : IsCompact.{u_1} (X := X) ∅
hmono : MonotoneOn f ∅
⊢ MemLp f p (μ.restrict ∅)

Tactic:
simp
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst_9 : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : s.Nonempty
⊢ MemLp f p (μ.restrict s)

Tactic:
hmono.memLp_of_measure_ne_top (hs.isLeast_sInf h) (hs.isGreatest_sSup h)
      hs.measure_lt_top.ne hs.measurableSet

Premises used: IsCompact.isLeast_sInf, MonotoneOn.memLp_of_measure_ne_top, IsCompact.measure_lt_top, IsCompact.isGreatest_sSup, LT.lt.ne, 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
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst_9 : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : s.Nonempty
⊢ MemLp f p (μ.restrict s)

Tactic:
exact hmono.memLp_of_measure_ne_top (hs.isLeast_sInf h) (hs.isGreatest_sSup h)
      hs.measure_lt_top.ne hs.measurableSet

Premises used: IsCompact.isLeast_sInf, MonotoneOn.memLp_of_measure_ne_top, IsCompact.measure_lt_top, IsCompact.isGreatest_sSup, LT.lt.ne, 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
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hanti : AntitoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
⊢ MemLp f ∞ (μ.restrict s)

Tactic:
MonotoneOn.memLp_top (E := Eᵒᵈ) hanti ha hb h's

Premises used: MonotoneOn.memLp_top, 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
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
hanti : AntitoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : MeasurableSet s
⊢ MemLp f p (μ.restrict s)

Tactic:
MonotoneOn.memLp_of_measure_ne_top (E := Eᵒᵈ) hanti ha hb hs h's

Premises used: MonotoneOn.memLp_of_measure_ne_top, 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
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst_9 : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hanti : AntitoneOn f s
⊢ MemLp f p (μ.restrict s)

Tactic:
MonotoneOn.memLp_isCompact (E := Eᵒᵈ) hs hanti

Premises used: MonotoneOn.memLp_isCompact, 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
s : Set X
inst_3 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : MeasurableSet s
⊢ IntegrableOn f s μ

Tactic:
memLp_one_iff_integrable.1 (hmono.memLp_of_measure_ne_top ha hb hs h's)

Premises used: MonotoneOn.memLp_of_measure_ne_top, MeasureTheory.IntegrableOn, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
⊢ IntegrableOn f s μ

Tactic:
memLp_one_iff_integrable.1 (hmono.memLp_isCompact hs)

Premises used: MeasureTheory.IntegrableOn, Iff.mp, MonotoneOn.memLp_isCompact, MeasureTheory.memLp_one_iff_integrable
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
hanti : AntitoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : MeasurableSet s
⊢ IntegrableOn f s μ

Tactic:
memLp_one_iff_integrable.1 (hanti.memLp_of_measure_ne_top ha hb hs h's)

Premises used: MeasureTheory.IntegrableOn, AntitoneOn.memLp_of_measure_ne_top, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hanti : AntitoneOn f s
⊢ IntegrableOn f s μ

Tactic:
memLp_one_iff_integrable.1 (hanti.memLp_isCompact hs)

Premises used: AntitoneOn.memLp_isCompact, MeasureTheory.IntegrableOn, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- 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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
rcases :
  ∀ (U : Set X) (hU : U ∈ 𝓝 x) (h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)),
    IntegrableAtFilter f (𝓝 x) μ
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
rcases μ.finiteAt_nhds x with ⟨U, hU, h'U⟩

Premises used: MeasureTheory.Measure.finiteAt_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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (a : X) (b : X), x ∈ Icc a b ∧ Icc a b ∈ 𝓝 x ∧ Icc a b ⊆ U

Tactic:
exists_Icc_mem_subset_of_mem_nhds hU

Premises used: Set.Mem, exists_Icc_mem_subset_of_mem_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 : BorelSpace X
inst_4 : ConditionallyCompleteLinearOrder X
inst_5 : ConditionallyCompleteLinearOrder E
inst_6 : OrderTopology X
inst_7 : OrderTopology E
inst_8 : SecondCountableTopology E
f : X → E
inst_9 : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
obtain : ∀ (a b : X) (xab : x ∈ Icc a b) (hab : Icc a b ∈ 𝓝 x) (abU : Icc a b ⊆ U), IntegrableAtFilter f (𝓝 x) μ
⊢ IntegrableAtFilter f (𝓝 x) μ

Tactic:
obtain ⟨a, b, xab, hab, abU⟩ : ∃ a b : X, x ∈ Icc a b ∧ Icc a b ∈ 𝓝 x ∧ Icc a b ⊆ U :=
    exists_Icc_mem_subset_of_mem_nhds hU

Premises used: nhds, exists_Icc_mem_subset_of_mem_nhds