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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
have h : ∀ (a : X) (h1 : a ∈ s → ‖f a‖ ≤ C) (h2 : a ∈ s → f a = AEStronglyMeasurable.mk f hfm a) (h3 : a ∈ s),
  ‖AEStronglyMeasurable.mk f hfm a‖ ≤ C
Tactic: filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
a : X
h1 : a ∈ s → ‖f a‖ ≤ C
h2 : a ∈ s → f a = AEStronglyMeasurable.mk f hfm a
h3 : a ∈ s
⊢ ‖AEStronglyMeasurable.mk f hfm a‖ ≤ C
have h : ‖f a‖ ≤ C
Tactic: rw [← h2 h3]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
have A : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
Tactic: have A : ∀ᵐ x : X ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C := by
      filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3
      rw [← h2 h3]
      exact h1 h3
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
A : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
have B : MeasurableSet.{u_1} (α := X) {x : X | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}
Tactic: have B : MeasurableSet {x | ‖hfm.mk f x‖ ≤ C} :=
      hfm.stronglyMeasurable_mk.norm.measurable measurableSet_Iic
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
A : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C
B : MeasurableSet.{u_1} (α := X) {x : X | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
have h : ∀ (a : X) (h1 : f a = AEStronglyMeasurable.mk f hfm a), ‖AEStronglyMeasurable.mk f hfm a‖ ≤ C → ‖f a‖ ≤ C
Tactic: filter_upwards [hfm.ae_eq_mk, (ae_restrict_iff B).2 A] with _ h1 _
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
have neg : norm.{u_3} (E := E) 0 ≤ C * μ.real s
Tactic: rw [integral_non_aestronglyMeasurable hfm]
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ ∃ᵐ (x : X) ∂μ, x ∈ s
have apply : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply frequently_ae_mem_iff.mpr
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have contrapose : ∀ (hfm : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), AEStronglyMeasurable f (μ.restrict s)
Tactic: contrapose hfm
Cleared hypotheses: hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ norm.{u_3} (E := E) 0 ≤ C * μ.real s
have this : ∃ᵐ (x : X) ∂μ, x ∈ s
Tactic: have : ∃ᵐ (x : X) ∂μ, x ∈ s := by
      apply frequently_ae_mem_iff.mpr
      contrapose hfm
      simp [Measure.restrict_eq_zero.mpr hfm]
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this : ∃ᵐ (x : X) ∂μ, x ∈ s
⊢ norm.{u_3} (E := E) 0 ≤ C * μ.real s
have neg : ∀ (x : X) (hx : x ∈ s) (h'x : x ∈ s → ‖f x‖ ≤ C), norm.{u_3} (E := E) 0 ≤ C * μ.real s
Tactic: rcases (this.and_eventually hC).exists with ⟨x, hx, h'x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this : ∃ᵐ (x : X) ∂μ, x ∈ s
x : X
hx : x ∈ s
h'x : x ∈ s → ‖f x‖ ≤ C
⊢ norm.{u_3} (E := E) 0 ≤ C * μ.real s
have this₁ : 0 ≤ C
Tactic: have : 0 ≤ C := (norm_nonneg _).trans (h'x hx)
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this_1 : ∃ᵐ (x : X) ∂μ, x ∈ s
x : X
hx : x ∈ s
h'x : x ∈ s → ‖f x‖ ≤ C
this : 0 ≤ C
⊢ norm.{u_3} (E := E) 0 ≤ C * μ.real s
have neg : 0 ≤ C * μ.real s
Tactic: simp only [norm_zero, ge_iff_le]
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
⊢ HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
have rw : ∫ (x : X), f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in sᶜ, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
rw : ∫ (x : X), f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in sᶜ, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
have rw₁ : ∫ (x : X), f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
rw : ∫ (x : X), f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in sᶜ, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
rw₁ : ∫ (x : X), f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
have rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X), f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
⊢ ‖HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)‖ ≤ μ.real sᶜ * C
have h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
Tactic: have h0 : ∫ (x : X), f x ∂μ - ∫ x in s, f x ∂μ = ∫ x in sᶜ, f x ∂μ := by
    rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
⊢ ‖HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)‖ ≤ μ.real sᶜ * C
have h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
Tactic: have h1 : ∫ x in sᶜ, ‖f x‖ ∂μ ≤ ∫ _ in sᶜ, C ∂μ :=
    integral_mono_ae hf1.norm.restrict (integrable_const C) (ae_restrict_of_ae hf)
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
⊢ ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
have rw : μ.real sᶜ • C = μ.real sᶜ * C
Tactic: rw [setIntegral_const C, smul_eq_mul]
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
rw : μ.real sᶜ • C = μ.real sᶜ * C
⊢ ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
have rw₁ : μ.real sᶜ * C = μ.real sᶜ * C
Tactic: rw [setIntegral_const C, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
⊢ ‖HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)‖ ≤ μ.real sᶜ * C
have h2 : ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
Tactic: have h2 : ∫ _ in sᶜ, C ∂μ = μ.real sᶜ * C := by
    rw [setIntegral_const C, smul_eq_mul]
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
h2 : ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
⊢ ‖HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)‖ ≤ μ.real sᶜ * C
have rw : norm.{u_3} (E := E) (∫ (x : X) in sᶜ, f x ∂μ) ≤ ∫ (x : X) in sᶜ, C ∂μ
Tactic: rw [h0, ← h2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : X) in s, f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (support f ∩ s) : ℝ≥0∞)
have rw : NullMeasurableSet (support f) (μ.restrict s)
Tactic: rw [integral_pos_iff_support_of_nonneg_ae hf hfi, Measure.restrict_apply₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
have refine : ∫⁻ (a : X) in {x : X | R < f x}, enorm (E := ℝ) ((fun (x : X) ↦ R) a) ∂μ ≤ ∫⁻ (a : X) in {x : X | R < f x}, ‖f a‖ₑ ∂μ
Tactic: refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ hfint.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (a : X) in {x : X | R < f x}, enorm (E := ℝ) ((fun (x : X) ↦ R) a) ∂μ ≤ ∫⁻ (a : X) in {x : X | R < f x}, ‖f a‖ₑ ∂μ
have refine : ∀ (x : X) (hx : Membership.mem (γ := Set X) {x : X | R < f x} x), enorm (E := ℝ) ((fun (x : X) ↦ R) x) ≤ ‖f x‖ₑ
Tactic: refine setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
x : X
hx : Membership.mem (γ := Set X) {x : X | R < f x} x
⊢ enorm (E := ℝ) ((fun (x : X) ↦ R) x) ≤ ‖f x‖ₑ
have simp : NNReal.mk R hR ≤ NNReal.mk (f x) sorry
Tactic: simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR, enorm_eq_nnnorm,
      Real.nnnorm_of_nonneg (hR.trans <| le_of_lt hx)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.real {x : X | R < f x} * R < ∫ (x : X) in {x : X | R < f x}, f x ∂μ
have this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
Tactic: have : IntegrableOn (fun _ => R) {x | ↑R < f x} μ := by
    refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ hfint.2⟩
    refine setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_
    simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR, enorm_eq_nnnorm,
      Real.nnnorm_of_nonneg (hR.trans <| le_of_lt hx)]
    exact le_of_lt hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
⊢ μ.real {x : X | R < f x} * R < ∫ (x : X) in {x : X | R < f x}, f x ∂μ
have rw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((μ : (a : Set X) → ℝ≥0∞) ((support (M := ℝ) fun (a : X) ↦ f a - R) ∩ {x : X | R < f x}) : ℝ≥0∞)
Tactic: rw [← sub_pos, ← smul_eq_mul, ← setIntegral_const, ← integral_sub hfint this,
    setIntegral_pos_iff_support_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((support (M := ℝ) fun (a : X) ↦ f a - R) ∩ {x : X | R < f x}) : ℝ≥0∞)
⊢ μ.real {x : X | R < f x} * R < ∫ (x : X) in {x : X | R < f x}, f x ∂μ
have hf : (ae (μ.restrict {x : X | R < f x})).EventuallyLE (β := ℝ) 0 fun (a : X) ↦ f a - R
Tactic: rw [← sub_pos, ← smul_eq_mul, ← setIntegral_const, ← integral_sub hfint this,
    setIntegral_pos_iff_support_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((support (M := ℝ) fun (a : X) ↦ f a - R) ∩ {x : X | R < f x}) : ℝ≥0∞)
hf : (ae (μ.restrict {x : X | R < f x})).EventuallyLE (β := ℝ) 0 fun (a : X) ↦ f a - R
⊢ μ.real {x : X | R < f x} * R < ∫ (x : X) in {x : X | R < f x}, f x ∂μ
have hfi : IntegrableOn (ε := ℝ) (fun (a : X) ↦ f a - R) {x : X | R < f x} μ
Tactic: rw [← sub_pos, ← smul_eq_mul, ← setIntegral_const, ← integral_sub hfint this,
    setIntegral_pos_iff_support_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((support (M := ℝ) fun (a : X) ↦ f a - R) ∩ {x : X | R < f x}) : ℝ≥0∞)
have hμ₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞)
Tactic: rw [← pos_iff_ne_zero] at hμ
Cleared hypotheses: hμ, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((support (M := ℝ) fun (a : X) ↦ f a - R) ∩ {x : X | R < f x}) : ℝ≥0∞)
have rwa : Subset.{u_1} (α := Set X) {x : X | R < f x} (support (M := ℝ) fun (a : X) ↦ f a - R)
Tactic: rwa [Set.inter_eq_self_of_subset_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
⊢ (ae (μ.restrict {x : X | R < f x})).EventuallyLE (β := ℝ) 0 fun (a : X) ↦ f a - R
have hf : ∀ᵐ (x : X) ∂μ, Membership.mem (γ := Set X) {x : X | R < f x} x → 0 ≤ f x - R
Tactic: rw [Pi.zero_def, EventuallyLE, ae_restrict_iff₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
hf : ∀ᵐ (x : X) ∂μ, Membership.mem (γ := Set X) {x : X | R < f x} x → 0 ≤ f x - R
⊢ (ae (μ.restrict {x : X | R < f x})).EventuallyLE (β := ℝ) 0 fun (a : X) ↦ f a - R
have hf₁ : NullMeasurableSet {x : X | 0 ≤ f x - R} (μ.restrict {x : X | R < f x})
Tactic: rw [Pi.zero_def, EventuallyLE, ae_restrict_iff₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
f : X → E
hf_meas : StronglyMeasurable f
s : Set X
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, f x ∂μ.trim hm)
have rwa : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂(μ.restrict s).trim hm) (∫ (x : X) in s, f x ∂μ.trim hm)
Tactic: rwa [integral_trim hm hf_meas, restrict_trim hm μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
f : X → E
hf_meas : StronglyMeasurable f
s : Set X
hs : MeasurableSet s
rwa : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂(μ.restrict s).trim hm) (∫ (x : X) in s, f x ∂μ.trim hm)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, f x ∂μ.trim hm)
have rwa₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂(μ.restrict s).trim hm) (∫ (x : X), f x ∂(μ.restrict s).trim hm)
Tactic: rwa [integral_trim hm hf_meas, restrict_trim hm μ]
-- 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 μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ico x y, f t ∂μ) (∫ (t : X) in Ioc x y, f t ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ioo x y, f t ∂μ) (∫ (t : X) in Ioc x y, f t ∂μ)
Tactic: rw [integral_Ico_eq_integral_Ioo, integral_Ioc_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
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
inst_3 : NoAtoms μ
rw : Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ioo x y, f t ∂μ) (∫ (t : X) in Ioc x y, f t ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ico x y, f t ∂μ) (∫ (t : X) in Ioc 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_Ico_eq_integral_Ioo, integral_Ioc_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
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
inst_3 : NoAtoms μ
⊢ 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 Ico x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)
Tactic: rw [integral_Icc_eq_integral_Ico, integral_Ico_eq_integral_Ioo]