awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
have neg : ∀ (hab : ¬a < b), IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: by_cases hab : a < b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos : IntegrableOn f (Ioo a b ∪ {a}) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [← Ioo_union_left hab, integrableOn_union,
      eq_true (integrableOn_singleton ha'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos₁ : IntegrableOn f (Ioo a b) μ ∧ IntegrableOn f {a} μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [← Ioo_union_left hab, integrableOn_union,
      eq_true (integrableOn_singleton ha'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos₂ : IntegrableOn f (Ioo a b) μ ∧ True ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [← Ioo_union_left hab, integrableOn_union,
      eq_true (integrableOn_singleton ha'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos₃ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [← Ioo_union_left hab, integrableOn_union,
      eq_true (integrableOn_singleton ha'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
have neg : IntegrableOn f (Ico a b) μ ↔ IntegrableOn f ∅ μ
Tactic: rw [Ioo_eq_empty hab, Ico_eq_empty hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 ∅ μ
⊢ IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ioo a b) μ
have neg₁ : IntegrableOn f ∅ μ ↔ IntegrableOn f ∅ μ
Tactic: rw [Ioo_eq_empty hab, Ico_eq_empty hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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‖ₑ ≠ ∞
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos : ∀ (hab : a < b), IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: by_cases hab : a < b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have neg : ∀ (hab : ¬a < b), IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: by_cases hab : a < b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos : IntegrableOn f (Ioo a b ∪ {b}) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [← Ioo_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos₁ : IntegrableOn f (Ioo a b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [← Ioo_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos₂ : IntegrableOn f (Ioo a b) μ ∧ True ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [← Ioo_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have pos₃ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [← Ioo_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have neg : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f ∅ μ
Tactic: rw [Ioo_eq_empty hab, Ioc_eq_empty hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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 ∅ μ
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have neg₁ : IntegrableOn f ∅ μ ↔ IntegrableOn f ∅ μ
Tactic: rw [Ioo_eq_empty hab, Ioc_eq_empty hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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‖ₑ ≠ ∞
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have rw : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [integrableOn_Icc_iff_integrableOn_Ioc' ha ha', integrableOn_Ioc_iff_integrableOn_Ioo' hb hb']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have rw₁ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [integrableOn_Icc_iff_integrableOn_Ioc' ha ha', integrableOn_Ioc_iff_integrableOn_Ioo' hb hb']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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‖ₑ ≠ ∞
⊢ IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ
have rw : IntegrableOn f (Ioi b ∪ {b}) μ ↔ IntegrableOn f (Ioi b) μ
Tactic: rw [← Ioi_union_left, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ
have rw₁ : IntegrableOn f (Ioi b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ioi b) μ
Tactic: rw [← Ioi_union_left, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ
have rw₂ : IntegrableOn f (Ioi b) μ ∧ True ↔ IntegrableOn f (Ioi b) μ
Tactic: rw [← Ioi_union_left, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ
have rw₃ : IntegrableOn f (Ioi b) μ ↔ IntegrableOn f (Ioi b) μ
Tactic: rw [← Ioi_union_left, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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‖ₑ ≠ ∞
⊢ IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ
have rw : IntegrableOn f (Iio b ∪ {b}) μ ↔ IntegrableOn f (Iio b) μ
Tactic: rw [← Iio_union_right, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ
have rw₁ : IntegrableOn f (Iio b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Iio b) μ
Tactic: rw [← Iio_union_right, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ
have rw₂ : IntegrableOn f (Iio b) μ ∧ True ↔ IntegrableOn f (Iio b) μ
Tactic: rw [← Iio_union_right, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ
have rw₃ : IntegrableOn f (Iio b) μ ↔ IntegrableOn f (Iio b) μ
Tactic: rw [← Iio_union_right, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) 0 ∞
Tactic: rw [measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) 0 ∞
Tactic: rw [measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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‖ₑ ≠ ∞
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have rw : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [integrableOn_Icc_iff_integrableOn_Ioc ha, integrableOn_Ioc_iff_integrableOn_Ioo hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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) μ
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ
have rw₁ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [integrableOn_Icc_iff_integrableOn_Ioc ha, integrableOn_Ioc_iff_integrableOn_Ioo hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegrableOn (goal)
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∞) ((μ : (a : Set α) → ℝ≥0∞) {b} : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) 0 ∞
Tactic: rw [measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
⊢ ∀ᵐ (x_1 : α) ∂μ, ∀ᶠ (i : ι) in l, x_1 ∈ Metric.ball x (r i)
have h : ∀ (y : α), ∀ᶠ (i : ι) in l, y ∈ Metric.ball x (r i)
Tactic: filter_upwards with y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.ball x (r i)
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x_1 : ι |
      x_1 ∈ r ⁻¹' Ioi (dist x y) →
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (i : ι) ↦ y ∈ Metric.ball x (r i)) x_2} x_1}
    a
Tactic: filter_upwards [hr (Ioi_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        x_1 ∈ r ⁻¹' Ioi (dist x y) →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (i : ι) ↦ y ∈ Metric.ball x (r i)) x_2} x_1}
      a
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.ball x (r i)
have h₁ : ∀ a ∈ r ⁻¹' Ioi (dist x y), y ∈ Metric.ball x (r a)
Tactic: filter_upwards [hr (Ioi_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
⊢ ∀ᵐ (x_1 : α) ∂μ, ∀ᶠ (i : ι) in l, x_1 ∈ Metric.closedBall x (r i)
have h : ∀ (y : α), ∀ᶠ (i : ι) in l, y ∈ Metric.closedBall x (r i)
Tactic: filter_upwards with y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.closedBall x (r i)
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x_1 : ι |
      x_1 ∈ r ⁻¹' Ici (dist x y) →
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (i : ι) ↦ y ∈ Metric.closedBall x (r i)) x_2} x_1}
    a
Tactic: filter_upwards [hr (Ici_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : PseudoMetricSpace α
inst_2 : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        x_1 ∈ r ⁻¹' Ici (dist x y) →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (i : ι) ↦ y ∈ Metric.closedBall x (r i)) x_2} x_1}
      a
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.closedBall x (r i)
have h₁ : ∀ a ∈ r ⁻¹' Ici (dist x y), y ∈ Metric.closedBall x (r a)
Tactic: filter_upwards [hr (Ici_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha