awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
e_a : ∀ (x : X) (hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x} x), ‖f x‖ = f x
⊢ Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ)

Tactic:
refine setIntegral_congr_fun₀ h_meas fun x hx => ?_

Premises used: MeasureTheory.setIntegral_congr_fun₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x} x
rw : 0 ≤ f x
⊢ ‖f x‖ = f x

Tactic:
rw [Real.norm_eq_abs, abs_eq_self.mpr _]

Premises used: Iff.mpr, abs_eq_self, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x} x
⊢ 0 ≤ f x

Tactic:
hx

Premises used: Set.Mem
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x} x
⊢ 0 ≤ f x

Tactic:
exact hx
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
e_a : Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) (-∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, f x ∂μ)
⊢ HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, f x ∂μ)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
e_a : Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) (∫ (a : X) in {x : X | 0 ≤ f x}ᶜ, -f a ∂μ)
⊢ Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) (-∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, f x ∂μ)

Tactic:
rw [← integral_neg]

Premises used: MeasureTheory.integral_neg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) (∫ (a : X) in {x : X | 0 ≤ f x}ᶜ, -f a ∂μ)

Tactic:
setIntegral_congr_fun₀ h_meas.compl fun x hx => ?_

Premises used: MeasureTheory.NullMeasurableSet.compl, MeasureTheory.setIntegral_congr_fun₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
e_a : ∀ (x : X) (hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x}ᶜ x), ‖f x‖ = -f x
⊢ Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) (∫ (a : X) in {x : X | 0 ≤ f x}ᶜ, -f a ∂μ)

Tactic:
refine setIntegral_congr_fun₀ h_meas.compl fun x hx => ?_

Premises used: MeasureTheory.NullMeasurableSet.compl, MeasureTheory.setIntegral_congr_fun₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x}ᶜ x
rw : f x ≤ 0
⊢ ‖f x‖ = -f x

Tactic:
rw [Real.norm_eq_abs, abs_eq_neg_self.mpr _]

Premises used: Iff.mpr, abs_eq_neg_self, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x}ᶜ x
⊢ ¬0 ≤ f x

Tactic:
rw [Set.mem_compl_iff, Set.notMem_setOf_iff] at hx

Premises used: Set.notMem_setOf_iff, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : ¬0 ≤ f x
linarith : 0 < f x → f x - 0 + (0 - f x) = 0
⊢ f x ≤ 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
rw :
  HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {a : X | ¬0 ≤ f a}, f x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
⊢ HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, f x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | f x ≤ 0}, f x ∂μ)

Tactic:
rw [← setIntegral_neg_eq_setIntegral_nonpos hfi.1, compl_setOf]

Premises used: MeasureTheory.setIntegral_neg_eq_setIntegral_nonpos, And.left, Set.compl_setOf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {a : X | ¬0 ≤ f a}, f x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)

Tactic:
simp only [not_le]

Premises used: not_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set X
μ : Measure X
inst_2 : CompleteSpace E
c : E
rw : (μ.restrict s).real univ • c = μ.real s • c
rw₁ rw₂ : μ.real s • c = μ.real s • c
⊢ ∫ (x : X) in s, c ∂μ = μ.real s • c

Tactic:
rw [integral_const, measureReal_restrict_apply_univ]

Premises used: MeasureTheory.integral_const, MeasureTheory.measureReal_restrict_apply_univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : CompleteSpace E
e : E
s : Set X
s_meas : MeasurableSet s
rw : ∫ (x : X) in s, e ∂μ = μ.real s • e
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, e ∂μ) (∫ (x : X) in s, e ∂μ)
⊢ ∫ (x : X), s.indicator (fun (x : X) ↦ e) x ∂μ = μ.real s • e

Tactic:
rw [integral_indicator s_meas, ← setIntegral_const]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.setIntegral_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), s.indicator 1 x ∂μ = μ.real s

Tactic:
(integral_indicator_const 1 hs).trans ((smul_eq_mul ..).trans (mul_one _))

Premises used: MeasureTheory.integral_indicator_const, smul_eq_mul, mul_one, OfNat.ofNat, Eq.trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set X
μ : Measure X
inst_2 : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e : E
rw rw₁ :
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, t.indicator (fun (x : X) ↦ e) x ∂μ)
    (∫ (x : X) in s, t.indicator (fun (x : X) ↦ e) x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)
    (∫ (x : X) in s, t.indicator (fun (x : X) ↦ e) x ∂μ)

Tactic:
rw [setIntegral_congr_ae hs (indicatorConstLp_coeFn.mono fun x hx _ => hx)]

Premises used: MeasureTheory.setIntegral_congr_ae, Filter.Eventually.mono, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set X
μ : Measure X
inst_2 : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e : E
rw : (μ.restrict s).real t • e = μ.real (t ∩ s) • e
rw₁ rw₂ : μ.real (t ∩ s) • e = μ.real (t ∩ s) • e
⊢ ∫ (x : X) in s, t.indicator (fun (x : X) ↦ e) x ∂μ = μ.real (t ∩ s) • e

Tactic:
rw [integral_indicator_const _ ht, measureReal_restrict_apply ht]

Premises used: MeasureTheory.integral_indicator_const, MeasureTheory.measureReal_restrict_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : Set X
μ : Measure X
inst_2 : CompleteSpace E
p : ℝ≥0∞
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e : E
rw rw₁ :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)
    (∫ (x : X), (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)
    (∫ (x : X) in univ, (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)

Tactic:
rw [setIntegral_univ]

Premises used: MeasureTheory.setIntegral_univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : Set X
μ : Measure X
inst_2 : CompleteSpace E
p : ℝ≥0∞
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e : E
rw rw₁ : μ.real t • e = μ.real t • e
⊢ μ.real (t ∩ univ) • e = μ.real t • e

Tactic:
rw [inter_univ]

Premises used: Set.inter_univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst_2 : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable (m₀ := inst_2) f (Measure.map g μ)
hg : AEMeasurable g μ
rw : LE.le (α := Measure Y) (Measure.map g (μ.restrict (g ⁻¹' s))) (Measure.map g μ)
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ inst_2 (Measure.restrict (Measure.map g μ) s) fun (y : Y) ↦ f y)
    (∫ (x : X) in g ⁻¹' s, f (g x) ∂μ)

Tactic:
rw [Measure.restrict_map_of_aemeasurable hg hs,
    integral_map (hg.mono_measure Measure.restrict_le_self) (hf.mono_measure _)]

Premises used: MeasureTheory.integral_map, MeasureTheory.Measure.restrict_map_of_aemeasurable, MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.restrict_le_self, AEMeasurable.mono_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst_2 : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable (m₀ := inst_2) f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ LE.le (α := Measure Y) (Measure.map g (μ.restrict (g ⁻¹' s))) (Measure.map g μ)

Tactic:
Measure.map_mono_of_aemeasurable Measure.restrict_le_self hg

Premises used: MeasureTheory.Measure.map_mono_of_aemeasurable, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst_2 : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable (m₀ := inst_2) f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ LE.le (α := Measure Y) (Measure.map g (μ.restrict (g ⁻¹' s))) (Measure.map g μ)

Tactic:
exact Measure.map_mono_of_aemeasurable Measure.restrict_le_self hg

Premises used: MeasureTheory.Measure.map_mono_of_aemeasurable, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
x : MeasurableSpace Y
f : X → Y
hf : MeasurableEmbedding f
g : Y → E
s : Set Y
rw :
  Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ x (Measure.map f (μ.restrict (f ⁻¹' s))) fun (y : Y) ↦ g y)
    (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ) (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ x (Measure.restrict (Measure.map f μ) s) fun (y : Y) ↦ g y)
    (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ)

Tactic:
rw [hf.restrict_map, hf.integral_map]

Premises used: MeasurableEmbedding.integral_map, MeasurableEmbedding.restrict_map
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : TopologicalSpace X
inst_3 : BorelSpace X
Y : Type u_5
inst_4 : MeasurableSpace Y
inst_5 : TopologicalSpace Y
inst_6 : BorelSpace Y
g : X → Y
f : Y → E
s : Set Y
hg : IsClosedEmbedding g
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ inst_4 (Measure.restrict (Measure.map g μ) s) fun (y : Y) ↦ f y)
    (∫ (x : X) in g ⁻¹' s, f (g x) ∂μ)

Tactic:
hg.measurableEmbedding.setIntegral_map _ _

Premises used: Topology.IsClosedEmbedding.measurableEmbedding, MeasurableEmbedding.setIntegral_map
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
x : MeasurableSpace Y
f : X → Y
ν : Measure Y
h₁ : MeasurePreserving f μ ν
h₂ : MeasurableEmbedding f
g : Y → E
s : Set Y
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ) (∫ (y : Y) in s, g y ∂ν)

Tactic:
(h₁.restrict_preimage_emb h₂ s).integral_comp h₂ _

Premises used: MeasureTheory.MeasurePreserving.integral_comp, MeasureTheory.MeasurePreserving.restrict_preimage_emb
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
x : MeasurableSpace Y
f : X → Y
ν : Measure Y
h₁ : MeasurePreserving f μ ν
h₂ : MeasurableEmbedding f
g : Y → E
s : Set X
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : Y) in f '' s, g y ∂ν) (∫ (x : X) in s, g (f x) ∂μ)

Tactic:
Eq.symm <| (h₁.restrict_image_emb h₂ s).integral_comp h₂ _

Premises used: MeasureTheory.MeasurePreserving.integral_comp, MeasureTheory.MeasurePreserving.restrict_image_emb, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst_2 : MeasurableSpace Y
e : X ≃ᵐ Y
f : Y → E
s : Set Y
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ inst_2 (Measure.restrict (Measure.map (⇑e : (a : X) → Y) μ) s) fun (y : Y) ↦ f y)
    (∫ (x : X) in (⇑e : (a : X) → Y) ⁻¹' s, f ((e : (a : X) → Y) x) ∂μ)

Tactic:
e.measurableEmbedding.setIntegral_map f s

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.setIntegral_map
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← Measure.restrict_apply_univ] at *

Premises used: MeasureTheory.Measure.restrict_apply_univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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) ∂μ.restrict s, ‖f x‖ ≤ C
hs₁ : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C

Tactic:
rw [← Measure.restrict_apply_univ] at *

Premises used: MeasureTheory.Measure.restrict_apply_univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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∞) ((μ.restrict s : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ IsFiniteMeasure (μ.restrict s)

Tactic:
haveI : IsFiniteMeasure (μ.restrict s) := ⟨hs⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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∞) ((μ.restrict s : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
this : IsFiniteMeasure (μ.restrict s)
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s

Tactic:
simpa using norm_integral_le_of_norm_le_const hC

Premises used: MeasureTheory.norm_integral_le_of_norm_le_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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
pos : ∀ (hfm : AEStronglyMeasurable f (μ.restrict s)), norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
neg : ∀ (hfm : ¬AEStronglyMeasurable f (μ.restrict s)), norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s

Tactic:
by_cases hfm : AEStronglyMeasurable f (μ.restrict s)

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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)
pos : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s

Tactic:
apply norm_setIntegral_le_of_norm_le_const_ae hs

Premises used: MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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)
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
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C

Tactic:
filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3

Premises used: MeasureTheory.AEStronglyMeasurable.ae_mem_imp_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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
h : ‖f a‖ ≤ C
⊢ ‖AEStronglyMeasurable.mk f hfm a‖ ≤ C

Tactic:
rw [← h2 h3]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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
⊢ ‖f a‖ ≤ C

Tactic:
h1 h3
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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
⊢ ‖f a‖ ≤ C

Tactic:
exact h1 h3
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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

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
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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}
a : X
h1 : f a = AEStronglyMeasurable.mk f hfm a
h : ‖AEStronglyMeasurable.mk f hfm a‖ ≤ C → ‖f a‖ ≤ C
⊢ ‖AEStronglyMeasurable.mk f hfm a‖ ≤ C → ‖f a‖ ≤ C

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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}
h : ∀ (a : X) (h1 : f a = AEStronglyMeasurable.mk f hfm a), ‖AEStronglyMeasurable.mk f hfm a‖ ≤ C → ‖f a‖ ≤ C
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C

Tactic:
filter_upwards [hfm.ae_eq_mk, (ae_restrict_iff B).2 A] with _ h1 _

Premises used: Iff.mpr, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_restrict_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
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}
a : X
h1 : f a = AEStronglyMeasurable.mk f hfm a
h_1 h h₁ h₂ h₃ : ‖AEStronglyMeasurable.mk f hfm a‖ ≤ C
⊢ ‖f a‖ ≤ C

Tactic:
rwa [h1]