awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopologyEither α E
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
a : α
t : Set α
f : α → E
hft : ContinuousOn f t
ht : MeasurableSet t
ha : a ∈ t
⊢ IntegrableAtFilter f (𝓝[t] a) μ

Tactic:
haveI : (𝓝[t] a).IsMeasurablyGenerated := ht.nhdsWithin_isMeasurablyGenerated _
  (hft a ha).integrableAtFilter ⟨_, self_mem_nhdsWithin, hft.aestronglyMeasurable ht⟩
    (μ.finiteAt_nhdsWithin _ _)

Premises used: ContinuousOn.aestronglyMeasurable, self_mem_nhdsWithin, And.intro, Filter.Tendsto.integrableAtFilter, Exists.intro, MeasureTheory.Measure.finiteAt_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopologyEither α E
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
a : α
rw : IntegrableAtFilter f (𝓝[univ] a) μ
⊢ IntegrableAtFilter f (𝓝 a) μ

Tactic:
rw [← nhdsWithin_univ]

Premises used: nhdsWithin_univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopologyEither α E
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
a : α
⊢ IntegrableAtFilter f (𝓝[univ] a) μ

Tactic:
hf.continuousOn.integrableAt_nhdsWithin MeasurableSet.univ (mem_univ a)

Premises used: Continuous.continuousOn, ContinuousOn.integrableAt_nhdsWithin, Set.mem_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopologyEither α E
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
a : α
⊢ IntegrableAtFilter f (𝓝[univ] a) μ

Tactic:
exact hf.continuousOn.integrableAt_nhdsWithin MeasurableSet.univ (mem_univ a)

Premises used: Continuous.continuousOn, ContinuousOn.integrableAt_nhdsWithin, Set.mem_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
inst_4 : SecondCountableTopologyEither α β
f : α → β
s : Set α
μ : Measure α
hs : IsOpen[inst] s
hf : ContinuousOn f s
⊢ ∀ x ∈ s, StronglyMeasurableAtFilter f (𝓝 x) μ

Tactic:
fun _x hx =>
  ⟨s, IsOpen.mem_nhds hs hx, hf.aestronglyMeasurable hs.measurableSet⟩

Premises used: IsOpen.measurableSet, ContinuousOn.aestronglyMeasurable, StronglyMeasurableAtFilter, And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopologyEither α E
f : α → E
s : Set α
μ : Measure α
hs : IsOpen[inst_1] s
hf : ∀ x ∈ s, ContinuousAt f x
⊢ ∀ x ∈ s, StronglyMeasurableAtFilter f (𝓝 x) μ

Tactic:
ContinuousOn.stronglyMeasurableAtFilter hs <| continuousOn_of_forall_continuousAt hf

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.stronglyMeasurableAtFilter
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : TopologicalSpace β
inst_3 : PseudoMetrizableSpace β
inst_4 : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst, inst_2] f
μ : Measure α
l : Filter α
⊢ StronglyMeasurableAtFilter f l μ

Tactic:
hf.stronglyMeasurable.stronglyMeasurableAtFilter

Premises used: Continuous.stronglyMeasurable, MeasureTheory.StronglyMeasurable.stronglyMeasurableAtFilter
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_7
β : Type u_8
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
inst_5 : SecondCountableTopologyEither α β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
x : α
⊢ StronglyMeasurableAtFilter f (𝓝[s] x) μ

Tactic:
⟨s, self_mem_nhdsWithin, hf.aestronglyMeasurable hs⟩

Premises used: ContinuousOn.aestronglyMeasurable, StronglyMeasurableAtFilter, self_mem_nhdsWithin, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
pos : ∀ (hab : a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
neg : ∀ (hab : ¬a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

Tactic:
by_cases hab : a ≤ b
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : a ≤ b
pos : IntegrableOn f (Ioc a b ∪ {a}) μ ↔ IntegrableOn f (Ioc a b) μ
pos₁ : IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f {a} μ ↔ IntegrableOn f (Ioc a b) μ
pos₂ : IntegrableOn f (Ioc a b) μ ∧ True ↔ IntegrableOn f (Ioc a b) μ
pos₃ pos₄ : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioc a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

Tactic:
rw [← Ioc_union_left hab, integrableOn_union, eq_true (integrableOn_singleton ha'), and_true]

Premises used: MeasureTheory.integrableOn_union, and_true, MeasureTheory.integrableOn_singleton, Set.Ioc_union_left, eq_true
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : ¬a ≤ b
neg : ¬a < b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ

Tactic:
rw [Icc_eq_empty hab, Ioc_eq_empty]

Premises used: Set.Icc_eq_empty, Set.Ioc_eq_empty
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : ¬a ≤ b
neg : ∀ (hab : a < b), a ≤ b
⊢ ¬a < b

Tactic:
contrapose hab
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : a < b
⊢ a ≤ b

Tactic:
hab.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : a < b
⊢ a ≤ b

Tactic:
exact hab.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
pos : ∀ (hab : a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
neg : ∀ (hab : ¬a ≤ b), IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
by_cases hab : a ≤ b
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : a ≤ b
pos : IntegrableOn f (Ico a b ∪ {b}) μ ↔ IntegrableOn f (Ico a b) μ
pos₁ : IntegrableOn f (Ico a b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ico a b) μ
pos₂ : IntegrableOn f (Ico a b) μ ∧ True ↔ IntegrableOn f (Ico a b) μ
pos₃ pos₄ : IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ico a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]

Premises used: MeasureTheory.integrableOn_union, and_true, MeasureTheory.integrableOn_singleton, eq_true, Set.Ico_union_right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : ¬a ≤ b
neg : ¬a < b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
rw [Icc_eq_empty hab, Ico_eq_empty]

Premises used: Set.Icc_eq_empty, Set.Ico_eq_empty
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : ¬a ≤ b
neg : ∀ (hab : a < b), a ≤ b
⊢ ¬a < b

Tactic:
contrapose hab
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : a < b
⊢ a ≤ b

Tactic:
hab.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : a < b
⊢ a ≤ b

Tactic:
exact hab.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
pos : ∀ (hab : a < b), IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
neg : ∀ (hab : ¬a < b), IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
by_cases hab : a < b
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : a < b
pos : IntegrableOn f (Ioo a b ∪ {a}) μ ↔ IntegrableOn f (Ioo a b) μ
pos₁ : IntegrableOn f (Ioo a b) μ ∧ IntegrableOn f {a} μ ↔ IntegrableOn f (Ioo a b) μ
pos₂ : IntegrableOn f (Ioo a b) μ ∧ True ↔ IntegrableOn f (Ioo a b) μ
pos₃ pos₄ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [← Ioo_union_left hab, integrableOn_union,
      eq_true (integrableOn_singleton ha'), and_true]

Premises used: MeasureTheory.integrableOn_union, and_true, Set.Ioo_union_left, MeasureTheory.integrableOn_singleton, eq_true
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hab : ¬a < b
neg : IntegrableOn f (Ico a b) μ ↔ IntegrableOn f ∅ μ
neg₁ neg₂ : IntegrableOn f ∅ μ ↔ IntegrableOn f ∅ μ
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [Ioo_eq_empty hab, Ico_eq_empty hab]

Premises used: Set.Ico_eq_empty, Set.Ioo_eq_empty
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
pos : ∀ (hab : a < b), IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
neg : ∀ (hab : ¬a < b), IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
by_cases hab : a < b
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : a < b
pos : IntegrableOn f (Ioo a b ∪ {b}) μ ↔ IntegrableOn f (Ioo a b) μ
pos₁ : IntegrableOn f (Ioo a b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ioo a b) μ
pos₂ : IntegrableOn f (Ioo a b) μ ∧ True ↔ IntegrableOn f (Ioo a b) μ
pos₃ pos₄ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [← Ioo_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]

Premises used: MeasureTheory.integrableOn_union, and_true, MeasureTheory.integrableOn_singleton, Set.Ioo_union_right, eq_true
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
hab : ¬a < b
neg : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f ∅ μ
neg₁ neg₂ : IntegrableOn f ∅ μ ↔ IntegrableOn f ∅ μ
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [Ioo_eq_empty hab, Ioc_eq_empty hab]

Premises used: Set.Ioc_eq_empty, Set.Ioo_eq_empty
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
ha' : ‖f a‖ₑ ≠ ∞
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
rw : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
rw₁ rw₂ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [integrableOn_Icc_iff_integrableOn_Ioc' ha ha', integrableOn_Ioc_iff_integrableOn_Ioo' hb hb']

Premises used: integrableOn_Ioc_iff_integrableOn_Ioo', integrableOn_Icc_iff_integrableOn_Ioc'
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
rw : IntegrableOn f (Ioi b ∪ {b}) μ ↔ IntegrableOn f (Ioi b) μ
rw₁ : IntegrableOn f (Ioi b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ioi b) μ
rw₂ : IntegrableOn f (Ioi b) μ ∧ True ↔ IntegrableOn f (Ioi b) μ
rw₃ rw₄ : IntegrableOn f (Ioi b) μ ↔ IntegrableOn f (Ioi b) μ
⊢ IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ

Tactic:
rw [← Ioi_union_left, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]

Premises used: MeasureTheory.integrableOn_union, and_true, MeasureTheory.integrableOn_singleton, eq_true, Set.Ioi_union_left
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
hb' : ‖f b‖ₑ ≠ ∞
rw : IntegrableOn f (Iio b ∪ {b}) μ ↔ IntegrableOn f (Iio b) μ
rw₁ : IntegrableOn f (Iio b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Iio b) μ
rw₂ : IntegrableOn f (Iio b) μ ∧ True ↔ IntegrableOn f (Iio b) μ
rw₃ rw₄ : IntegrableOn f (Iio b) μ ↔ IntegrableOn f (Iio b) μ
⊢ IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ

Tactic:
rw [← Iio_union_right, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]

Premises used: MeasureTheory.integrableOn_union, and_true, MeasureTheory.integrableOn_singleton, eq_true, Set.Iio_union_right
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst_5 : NoAtoms μ
ha : ‖f a‖ₑ ≠ ∞
rw : Ne (α := ℝ≥0∞) 0 ∞
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst_5 : NoAtoms μ
ha : ‖f a‖ₑ ≠ ∞
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
ENNReal.zero_ne_top

Premises used: ENNReal.zero_ne_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst_5 : NoAtoms μ
ha : ‖f a‖ₑ ≠ ∞
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
exact ENNReal.zero_ne_top

Premises used: ENNReal.zero_ne_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst_5 : NoAtoms μ
hb : ‖f b‖ₑ ≠ ∞
rw : Ne (α := ℝ≥0∞) 0 ∞
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst_5 : NoAtoms μ
hb : ‖f b‖ₑ ≠ ∞
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
ENNReal.zero_ne_top

Premises used: ENNReal.zero_ne_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst_5 : NoAtoms μ
hb : ‖f b‖ₑ ≠ ∞
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
exact ENNReal.zero_ne_top

Premises used: ENNReal.zero_ne_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst_5 : NoAtoms μ
ha : ‖f a‖ₑ ≠ ∞
hb : ‖f b‖ₑ ≠ ∞
rw : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
rw₁ rw₂ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [integrableOn_Icc_iff_integrableOn_Ioc ha, integrableOn_Ioc_iff_integrableOn_Ioo hb]

Premises used: integrableOn_Icc_iff_integrableOn_Ioc, integrableOn_Ioc_iff_integrableOn_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
inst_5 : NoAtoms μ
hb : ‖f b‖ₑ ≠ ∞
rw : Ne (α := ℝ≥0∞) 0 ∞
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
inst_5 : NoAtoms μ
hb : ‖f b‖ₑ ≠ ∞
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
ENNReal.zero_ne_top

Premises used: ENNReal.zero_ne_top
-- Module: Mathlib.MeasureTheory.Integral.IntegrableOn
Goal:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst : PartialOrder α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε'
inst_3 : ESeminormedAddMonoid ε'
inst_4 : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
inst_5 : NoAtoms μ
hb : ‖f b‖ₑ ≠ ∞
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
exact ENNReal.zero_ne_top

Premises used: ENNReal.zero_ne_top
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
φ ψ : ι → Set α
hφ : AECover μ l φ
hsub : ∀ (i : ι), φ i ⊆ ψ i
hmeas : ∀ (i : ι), MeasurableSet (ψ i)
⊢ AECover μ l ψ

Tactic:
⟨hφ.1.mono fun _x hx ↦ hx.mono fun i hi ↦ hsub i hi, hmeas⟩

Premises used: MeasureTheory.AECover.mk, Filter.Eventually.mono, MeasureTheory.AECover.ae_eventually_mem