awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
⊢ integral μ f = integral μ g

Tactic:
setToSimpleFunc_congr (weightedSMul μ) (fun _ _ => weightedSMul_null) weightedSMul_union hf h

Premises used: MeasureTheory.weightedSMul_null, MeasureTheory.weightedSMul, MeasureTheory.weightedSMul_union, MeasureTheory.SimpleFunc.integral, MeasureTheory.SimpleFunc.setToSimpleFunc_congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)

Tactic:
have : f =ᵐ[μ] f.map (ENNReal.toReal ∘ ENNReal.ofReal) :=
    h_pos.mono fun a h => (ENNReal.toReal_ofReal h).symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
this : (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)
rw : integral μ f = integral μ (map (ENNReal.toReal ∘ ENNReal.ofReal) f)
hg0 : ENNReal.ofReal 0 = 0
ht : ∀ (b : ℝ), ENNReal.ofReal b ≠ ∞
⊢ integral μ f = (∫⁻ (a : α), ENNReal.ofReal ((f : (a : α) → ℝ) a) ∂μ).toReal

Tactic:
rw [← integral_eq_lintegral' hf]

Premises used: MeasureTheory.SimpleFunc.integral_eq_lintegral'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
this : (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)
⊢ integral μ f = integral μ (map (ENNReal.toReal ∘ ENNReal.ofReal) f)

Tactic:
integral_congr hf this

Premises used: MeasureTheory.SimpleFunc.integral_congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
this : (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)
⊢ ENNReal.ofReal 0 = 0

Tactic:
ENNReal.ofReal_zero

Premises used: ENNReal.ofReal_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
this : (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)
⊢ ∀ (b : ℝ), ENNReal.ofReal b ≠ ∞

Tactic:
fun b => ENNReal.ofReal_ne_top

Premises used: ENNReal.ofReal_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ
hf : Integrable (ε := ℝ) (⇑f : (a : α) → ℝ) μ
h_pos : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : α) → ℝ)
this : (ae μ).EventuallyEq (β := ℝ) (⇑f : (a : α) → ℝ) (⇑(map (ENNReal.toReal ∘ ENNReal.ofReal) f) : (a : α) → ℝ)
⊢ integral μ f = integral μ (map (ENNReal.toReal ∘ ENNReal.ofReal) f)

Tactic:
exacts [integral_congr hf this, ENNReal.ofReal_zero, fun b => ENNReal.ofReal_ne_top]

Premises used: MeasureTheory.SimpleFunc.integral_congr, ENNReal.ofReal_zero, ENNReal.ofReal_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
⊢ integral μ (f + g) = integral μ f + integral μ g

Tactic:
setToSimpleFunc_add _ weightedSMul_union hf hg

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_add, MeasureTheory.weightedSMul_union, MeasureTheory.SimpleFunc.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ integral μ (-f) = -integral μ f

Tactic:
setToSimpleFunc_neg _ weightedSMul_union hf

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_neg, MeasureTheory.weightedSMul_union, MeasureTheory.SimpleFunc.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f g : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
hg : Integrable.{u_2, u_1} (ε := E) (⇑g : (a : α) → E) μ
⊢ integral μ (f - g) = integral μ f - integral μ g

Tactic:
setToSimpleFunc_sub _ weightedSMul_union hf hg

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_sub, MeasureTheory.weightedSMul_union, MeasureTheory.SimpleFunc.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : DistribSMul 𝕜 E
inst_3 : SMulCommClass ℝ 𝕜 E
c : 𝕜
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ integral μ (c • f) = c • integral μ f

Tactic:
setToSimpleFunc_smul _ weightedSMul_union weightedSMul_smul c hf

Premises used: MeasureTheory.weightedSMul_smul, MeasureTheory.SimpleFunc.setToSimpleFunc_smul, MeasureTheory.weightedSMul_union, MeasureTheory.SimpleFunc.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_3 : NormedSpace ℝ E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
rw :
  C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖ =
    C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) • ‖x‖
⊢ C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖ = C * integral μ (map norm f)

Tactic:
rw [map_integral f norm hf norm_zero]

Premises used: Norm.norm, norm_zero, MeasureTheory.SimpleFunc.map_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_3 : NormedSpace ℝ E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖ =
    C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) • ‖x‖

Tactic:
simp_rw [smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ ‖integral μ f‖ ≤ integral μ (map norm f)

Tactic:
(norm_setToSimpleFunc_le_integral_norm _ (fun s _ _ => ?_) hf).trans (one_mul _).le

Premises used: Eq.le, MeasureTheory.SimpleFunc.integral, LE.le.trans, MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_integral_norm, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
refine :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        norm.{u_2} (E := E →L[ℝ] E) (weightedSMul μ s) ≤ 1 * μ.real s
⊢ ‖integral μ f‖ ≤ integral μ (map norm f)

Tactic:
refine (norm_setToSimpleFunc_le_integral_norm _ (fun s _ _ => ?_) hf).trans (one_mul _).le

Premises used: Eq.le, LE.le.trans, MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_integral_norm, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ norm.{u_2} (E := E →L[ℝ] E) (weightedSMul μ s) ≤ 1 * μ.real s

Tactic:
(norm_weightedSMul_le s).trans (one_mul _).symm.le

Premises used: Eq.le, MeasureTheory.norm_weightedSMul_le, LE.le.trans, Eq.symm, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ norm.{u_2} (E := E →L[ℝ] E) (weightedSMul μ s) ≤ 1 * μ.real s

Tactic:
exact (norm_weightedSMul_le s).trans (one_mul _).symm.le

Premises used: Eq.le, MeasureTheory.norm_weightedSMul_le, LE.le.trans, Eq.symm, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) (μ + ν)
simp_rw :
  setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f
⊢ integral (μ + ν) f = integral μ f + integral ν f

Tactic:
simp_rw [integral_def]

Premises used: MeasureTheory.SimpleFunc.integral_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) (μ + ν)
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f

Tactic:
setToSimpleFunc_add_left'
    (weightedSMul μ) (weightedSMul ν) (weightedSMul (μ + ν)) (fun s _ hμνs => ?_) hf

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_add_left', MeasureTheory.weightedSMul, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) (μ + ν)
refine :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (hμνs : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        weightedSMul (μ + ν) s = HAdd.hAdd (α := E →L[ℝ] E) (weightedSMul μ s) (weightedSMul ν s)
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f

Tactic:
refine setToSimpleFunc_add_left'
    (weightedSMul μ) (weightedSMul ν) (weightedSMul (μ + ν)) (fun s _ hμνs => ?_) hf

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_add_left', MeasureTheory.weightedSMul, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) (μ + ν)
s : Set α
h : MeasurableSet s
hμνs : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [lt_top_iff_ne_top, Measure.coe_add, Pi.add_apply, ENNReal.add_ne_top] at hμνs

Premises used: MeasureTheory.Measure.coe_add, lt_top_iff_ne_top, Pi.add_apply, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) (μ + ν)
s : Set α
h : MeasurableSet s
hμνs :
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw rw₁ :
  HAdd.hAdd (α := E →L[ℝ] E) (weightedSMul μ s) (weightedSMul ν s) =
    HAdd.hAdd (α := E →L[ℝ] E) (weightedSMul μ s) (weightedSMul ν s)
⊢ weightedSMul (μ + ν) s = HAdd.hAdd (α := E →L[ℝ] E) (weightedSMul μ s) (weightedSMul ν s)

Tactic:
rw [weightedSMul_add_measure _ _ hμνs.1 hμνs.2]

Premises used: MeasureTheory.weightedSMul_add_measure, And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
rw : LE.le (α := F) 0 (∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
⊢ 0 ≤ integral μ f

Tactic:
rw [integral_eq]

Premises used: MeasureTheory.SimpleFunc.integral_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
h : ∀ i ∈ f.range, 0 ≤ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i
⊢ LE.le (α := F) 0 (∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)

Tactic:
apply Finset.sum_nonneg

Premises used: Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
h :
  ∀ (x : α),
    0 ≤
      HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F)
⊢ ∀ i ∈ f.range, 0 ≤ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i

Tactic:
rw [forall_mem_range]

Premises used: MeasureTheory.SimpleFunc.forall_mem_range
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
pos :
  ∀ (hy : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)),
    0 ≤
      HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
        ((f : (a : α) → F) y : F)
neg :
  ∀ (hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)),
    0 ≤
      HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
        ((f : (a : α) → F) y : F)
⊢ 0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
      ((f : (a : α) → F) y : F)

Tactic:
by_cases hy : 0 ≤ f y

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
⊢ 0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
      ((f : (a : α) → F) y : F)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
this :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ 0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
      ((f : (a : α) → F) y : F)

Tactic:
simp [this, measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
neg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ 0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
      ((f : (a : α) → F) y : F)

Tactic:
suffices μ (f ⁻¹' {f y}) = 0 by simp [this, measureReal_def]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
neg :
  LE.le (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
le_of_le_of_eq (measure_mono fun x hx ↦ ?_) (ae_iff.mp hf)

Premises used: le_of_le_of_eq, MeasureTheory.ae_iff, MeasureTheory.measure_mono, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
neg :
  ∀ (x : α)
    (hx :
      Membership.mem (γ := Set α)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) x),
    Membership.mem (γ := Set α) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} x
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
refine le_of_le_of_eq (measure_mono fun x hx ↦ ?_) (ae_iff.mp hf)

Premises used: le_of_le_of_eq, MeasureTheory.ae_iff, MeasureTheory.measure_mono, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
x : α
hx :
  Membership.mem (γ := Set α) (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F)))
    x
⊢ Eq.{u_3 + 1} (α := F) ((f : (a : α) → F) x : F) ((f : (a : α) → F) y : F)

Tactic:
simp only [Set.mem_preimage, mem_singleton_iff, mem_setOf_eq] at hx ⊢

Premises used: Set.mem_setOf_eq, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
x : α
hx : Eq.{u_3 + 1} (α := F) ((f : (a : α) → F) x : F) ((f : (a : α) → F) y : F)
⊢ ¬LE.le.{u_3} (α := F) (0 x : F) ((f : (a : α) → F) x : F)

Tactic:
hx ▸ hy

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
x : α
hx : Eq.{u_3 + 1} (α := F) ((f : (a : α) → F) x : F) ((f : (a : α) → F) y : F)
⊢ ¬LE.le.{u_3} (α := F) (0 x : F) ((f : (a : α) → F) x : F)

Tactic:
exact hx ▸ hy
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f g : α →ₛ F
h : EventuallyLE.{u_1, u_3} (β := F) (ae μ) (⇑f : (a : α) → F) (⇑g : (a : α) → F)
hf : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) μ
hg : Integrable.{u_3, u_1} (ε := F) (⇑g : (a : α) → F) μ
rw : 0 ≤ integral μ (g - f)
⊢ integral μ f ≤ integral μ g

Tactic:
rw [← sub_nonneg, ← integral_sub hg hf]

Premises used: MeasureTheory.SimpleFunc.integral_sub, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f g : α →ₛ F
h : EventuallyLE.{u_1, u_3} (β := F) (ae μ) (⇑f : (a : α) → F) (⇑g : (a : α) → F)
hf : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) μ
hg : Integrable.{u_3, u_1} (ε := F) (⇑g : (a : α) → F) μ
⊢ 0 ≤ᶠ[ae μ] HSub.hSub (α := α → F) (⇑g : (a : α) → F) (⇑f : (a : α) → F)

Tactic:
rw [← sub_nonneg_ae] at h

Premises used: MeasureTheory.sub_nonneg_ae