awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
inst_3 : NoAtoms μ
rw : Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ico x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Icc x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ioo x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)
Tactic: rw [integral_Icc_eq_integral_Ico, integral_Ico_eq_integral_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᶠ[ae (μ.restrict s)] g
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)
have pos : ∀ (hE : CompleteSpace E), LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᶠ[ae (μ.restrict s)] g
pos : ∀ (hE : CompleteSpace E), LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)
have neg : ∀ (hE : ¬CompleteSpace E), LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)
have refine : f ≤ᶠ[ae (μ.restrict s)] g
Tactic: refine setIntegral_mono_ae_restrict hf hg ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ f ≤ᶠ[ae (μ.restrict s)] g
have rwa : ∀ᵐ (x : X) ∂μ.restrict s, f x ≤ g x
Tactic: rwa [EventuallyLE, ae_restrict_iff' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)
have rw : LE.le.{u_3} (α := E) (∫ (x : X) in toMeasurable μ s, f x ∂μ) (∫ (x : X) in toMeasurable μ s, g x ∂μ)
Tactic: rw [setIntegral_congr_set hs.toMeasurable_ae_eq.symm,
    setIntegral_congr_set hs.toMeasurable_ae_eq.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in toMeasurable μ s, f x ∂μ) (∫ (x : X) in toMeasurable μ s, g x ∂μ)
have refine_1 : IntegrableOn f (toMeasurable μ s) μ
Tactic: refine setIntegral_mono_on_ae ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
refine_1 : IntegrableOn f (toMeasurable μ s) μ
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in toMeasurable μ s, f x ∂μ) (∫ (x : X) in toMeasurable μ s, g x ∂μ)
have refine_2 : IntegrableOn g (toMeasurable μ s) μ
Tactic: refine setIntegral_mono_on_ae ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
refine_1 : IntegrableOn f (toMeasurable μ s) μ
refine_2 : IntegrableOn g (toMeasurable μ s) μ
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in toMeasurable μ s, f x ∂μ) (∫ (x : X) in toMeasurable μ s, g x ∂μ)
have refine_3 : MeasurableSet (toMeasurable μ s)
Tactic: refine setIntegral_mono_on_ae ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
refine_1 : IntegrableOn f (toMeasurable μ s) μ
refine_2 : IntegrableOn g (toMeasurable μ s) μ
refine_3 : MeasurableSet (toMeasurable μ s)
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in toMeasurable μ s, f x ∂μ) (∫ (x : X) in toMeasurable μ s, g x ∂μ)
have refine_4 : ∀ᵐ (x : X) ∂μ, x ∈ toMeasurable μ s → f x ≤ g x
Tactic: refine setIntegral_mono_on_ae ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ ∀ᵐ (x : X) ∂μ, x ∈ toMeasurable μ s → f x ≤ g x
have h₁ : ∀ (x : X) (hx : x ∈ toMeasurable μ s ↔ x ∈ s) (h : x ∈ s → f x ≤ g x), x ∈ toMeasurable μ s → f x ≤ g x
Tactic: filter_upwards [hs.toMeasurable_ae_eq.mem_iff, h] with x hx h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f : X → E
s : Set X
inst_5 : ClosedIciTopology E
inst_6 : CompleteSpace E
c : E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn.{u_1, u_3} (ε := E) (fun (x : X) ↦ f x) s μ
⊢ μ.real s • c ≤ ∫ (x : X) in s, f x ∂μ
have rw : LE.le.{u_3} (α := E) (∫ (x : X) in s, c ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: rw [← setIntegral_const c]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x
⊢ 0 ≤ᶠ[ae (μ.restrict s)] f
have rwa : ∀ᵐ (x : X) ∂μ.restrict s, 0 x ≤ f x
Tactic: rwa [EventuallyLE, ae_restrict_iff' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x
rwa : ∀ᵐ (x : X) ∂μ.restrict s, 0 x ≤ f x
⊢ 0 ≤ᶠ[ae (μ.restrict s)] f
have rwa₁ : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 x ≤ f x
Tactic: rwa [EventuallyLE, ae_restrict_iff' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in {y : X | 0 ≤ f y}, f x ∂μ)
have rw : LE.le (α := ℝ) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X), indicator {a : X | 0 ≤ f a} f x ∂μ)
Tactic: rw [← integral_indicator hs, ←
    integral_indicator (stronglyMeasurable_const.measurableSet_le hf)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0
⊢ f ≤ᶠ[ae (μ.restrict s)] 0
have rwa : ∀ᵐ (x : X) ∂μ.restrict s, f x ≤ 0 x
Tactic: rwa [EventuallyLE, ae_restrict_iff' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0
rwa : ∀ᵐ (x : X) ∂μ.restrict s, f x ≤ 0 x
⊢ f ≤ᶠ[ae (μ.restrict s)] 0
have rwa₁ : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0 x
Tactic: rwa [EventuallyLE, ae_restrict_iff' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : X) in {y : X | f y ≤ 0}, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have rw : LE.le (α := ℝ) (∫ (x : X), indicator {a : X | f a ≤ 0} f x ∂μ) (∫ (x : X), s.indicator f x ∂μ)
Tactic: rw [← integral_indicator hs, ←
    integral_indicator (hf.measurableSet_le stronglyMeasurable_const)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ (μ : (a : Set X) → ℝ≥0∞) s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
have rw : (μ : (a : Set X) → ℝ≥0∞) s ≤ ∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ
Tactic: rw [ofReal_integral_eq_lintegral_ofReal f_int f_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ (μ : (a : Set X) → ℝ≥0∞) s ≤ ∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ
have hf : AEMeasurable (β := ℝ≥0∞) (fun (a : X) ↦ ENNReal.ofReal (f a)) μ
Tactic: apply meas_le_lintegral₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
hf : AEMeasurable (β := ℝ≥0∞) (fun (a : X) ↦ ENNReal.ofReal (f a)) μ
⊢ (μ : (a : Set X) → ℝ≥0∞) s ≤ ∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ
have hs₁ : ∀ x ∈ s, 1 ≤ ENNReal.ofReal (f x)
Tactic: apply meas_le_lintegral₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
have pos : ∀ (H : Integrable f μ), ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
Tactic: by_cases H : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
pos : ∀ (H : Integrable f μ), ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
have neg : ∀ (H : ¬Integrable f μ), ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
Tactic: by_cases H : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
have g_int : Integrable g μ
Tactic: have g_int : Integrable g μ := H.pos_part
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
have h : LE.le (α := ℝ) (∫ (x : X), f x ∂μ) (∫ (x : X), g x ∂μ)
Tactic: apply ENNReal.ofReal_le_ofReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
have this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
Tactic: have : ENNReal.ofReal (∫ x, f x ∂μ) ≤ ENNReal.ofReal (∫ x, g x ∂μ) := by
    apply ENNReal.ofReal_le_ofReal
    exact integral_mono H g_int (fun x ↦ le_max_left _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
have pos : ENNReal.ofReal (∫ (x : X), g x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
Tactic: apply this.trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
⊢ ENNReal.ofReal (∫ (x : X), g x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
have pos : ∫⁻ (x : X), ENNReal.ofReal (g x) ∂μ ≤ (μ : (a : Set X) → ℝ≥0∞) s
Tactic: rw [ofReal_integral_eq_lintegral_ofReal g_int (Eventually.of_forall (fun x ↦ le_max_right _ _))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
⊢ ∫⁻ (x : X), ENNReal.ofReal (g x) ∂μ ≤ (μ : (a : Set X) → ℝ≥0∞) s
have pos : ∀ (a : X), ENNReal.ofReal (g a) ≤ 1
Tactic: apply lintegral_le_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
pos : ∀ (a : X), ENNReal.ofReal (g a) ≤ 1
⊢ ∫⁻ (x : X), ENNReal.ofReal (g x) ∂μ ≤ (μ : (a : Set X) → ℝ≥0∞) s
have pos₁ : ∀ a ∈ sᶜ, ENNReal.ofReal (g a) = 0
Tactic: apply lintegral_le_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
⊢ ENNReal.ofReal (g x) ≤ 1
have pos : g x ≤ ENNReal.toReal 1
Tactic: apply ENNReal.ofReal_le_of_le_toReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
⊢ g x ≤ ENNReal.toReal 1
have pos : ∀ (H : x ∈ s), g x ≤ ENNReal.toReal 1
Tactic: by_cases H : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
pos : ∀ (H : x ∈ s), g x ≤ ENNReal.toReal 1
⊢ g x ≤ ENNReal.toReal 1
have neg : ∀ (H : x ∉ s), g x ≤ ENNReal.toReal 1
Tactic: by_cases H : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H_1 : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
H : x ∉ s
⊢ g x ≤ ENNReal.toReal 1
have apply : g x ≤ 0
Tactic: apply le_trans _ zero_le_one
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
⊢ IntegrableOn f (iUnion s) μ
have refine : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ) ∞
Tactic: refine ⟨AEStronglyMeasurable.iUnion fun i => (hi i).1, (lintegral_iUnion_le _ _).trans_lt ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ) ∞
have B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
Tactic: have B := fun i => lintegral_coe_eq_integral (fun x : X => ‖f x‖₊) (hi i).norm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ) ∞
have simp_rw : LT.lt (α := ℝ≥0∞) (∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, (↑‖f a‖₊ : ℝ) ∂μ)) ∞
Tactic: simp_rw [enorm_eq_nnnorm, tsum_congr B]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) ⋯
have rw : Summable (α := ℝ) fun (a : ι) ↦ (↑(NNReal.mk (∫ (x : X) in s a, (↑‖f x‖₊ : ℝ) ∂μ) sorry) : ℝ)
Tactic: rw [← NNReal.summable_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
⊢ LT.lt (α := ℝ≥0∞) (∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, (↑‖f a‖₊ : ℝ) ∂μ)) ∞
have S' : Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) sorry
Tactic: have S' : Summable fun i : ι =>
      (NNReal.mk (∫ x : X in s i, ‖f x‖₊ ∂μ) (integral_nonneg fun x => NNReal.coe_nonneg _)) := by
    rw [← NNReal.summable_coe]; exact h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
S' : Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) ⋯
⊢ LT.lt (α := ℝ≥0∞) (∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, (↑‖f a‖₊ : ℝ) ∂μ)) ∞
have S'' : ∑' (a : ι), (↑(NNReal.mk (∫ (x : X) in s a, (↑‖f x‖₊ : ℝ) ∂μ) sorry) : ℝ≥0∞) =
  (↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, (↑‖f x‖₊ : ℝ) ∂μ) sorry) : ℝ≥0∞)
Tactic: have S'' := ENNReal.tsum_coe_eq S'.hasSum
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
S' : Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) ⋯
S'' :
  ∑' (a : ι), (↑(NNReal.mk (∫ (x : X) in s a, (↑‖f x‖₊ : ℝ) ∂μ) ⋯) : ℝ≥0∞) =
    (↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, (↑‖f x‖₊ : ℝ) ∂μ) ⋯) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, (↑‖f a‖₊ : ℝ) ∂μ)) ∞
have S''₁ : ∑' (a : ι), ENNReal.ofReal (∫ (x : X) in s a, ‖f x‖ ∂μ) =
  ENNReal.ofReal (↑(∑' (b : ι), NNReal.mk (∫ (x : X) in s b, ‖f x‖ ∂μ) sorry) : ℝ)
Tactic: simp_rw [ENNReal.coe_nnreal_eq, NNReal.coe_mk, coe_nnnorm] at S''
Cleared hypotheses: S''
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace X
inst_3 : BorelSpace X
inst_4 : T2Space X
inst_5 : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
⊢ IntegrableOn.{u_1, u_3} (ε := E) (⇑f : (a : X) → E) (⋃ (i : ι), (↑(s i) : Set X)) μ
have i : ∀ (i : ι),
  ∫ (x : X) in (↑(s i) : Set X), norm.{u_3} (E := E) ((f : (a : X) → E) x : E) ∂μ ≤
    ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
Tactic: refine
    integrableOn_iUnion_of_summable_integral_norm
      (fun i => (map_continuous f).continuousOn.integrableOn_compact (s i).isCompact)
      (.of_nonneg_of_le (fun ι => integral_nonneg fun x => norm_nonneg _) (fun i => ?_) hf)