awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) μ
h₁ : 0 ≤ᶠ[ae μ] HSub.hSub (α := α → F) (⇑g : (a : α) → F) (⇑f : (a : α) → F)
⊢ Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) μ

Tactic:
rw [← sub_nonneg_ae] at h

Premises used: MeasureTheory.sub_nonneg_ae
-- 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) μ
h₁ : 0 ≤ᶠ[ae μ] HSub.hSub (α := α → F) (⇑g : (a : α) → F) (⇑f : (a : α) → F)
hf₁ : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) μ
⊢ Integrable.{u_3, u_1} (ε := F) (⇑g : (a : α) → F) μ

Tactic:
rw [← sub_nonneg_ae] at h

Premises used: MeasureTheory.sub_nonneg_ae
-- 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 : 0 ≤ᶠ[ae μ] HSub.hSub (α := α → F) (⇑g : (a : α) → F) (⇑f : (a : α) → F)
hf : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) μ
hg : Integrable.{u_3, u_1} (ε := F) (⇑g : (a : α) → F) μ
⊢ 0 ≤ integral μ (g - f)

Tactic:
integral_nonneg h

Premises used: MeasureTheory.SimpleFunc.integral_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 : 0 ≤ᶠ[ae μ] HSub.hSub (α := α → F) (⇑g : (a : α) → F) (⇑f : (a : α) → F)
hf : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) μ
hg : Integrable.{u_3, u_1} (ε := F) (⇑g : (a : α) → F) μ
⊢ 0 ≤ integral μ (g - f)

Tactic:
exact integral_nonneg h

Premises used: MeasureTheory.SimpleFunc.integral_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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
simp :
  LE.le (α := F) (∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
    (∑ x ∈ f.range, ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
⊢ integral μ f ≤ integral ν f

Tactic:
simp only [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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
h :
  ∀ i ∈ f.range,
    μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i ≤
      ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i
⊢ LE.le (α := F) (∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
    (∑ x ∈ f.range, ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)

Tactic:
apply Finset.sum_le_sum

Premises used: Finset.sum_le_sum
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
h :
  ∀ (x : α),
    HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F) ≤
      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,
    μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i ≤
      ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i

Tactic:
simp only [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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
pos :
  ∀ (hx : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
    HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F) ≤
      HSMul.hSMul (β := F)
        (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F)
neg :
  ∀ (hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
    HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F) ≤
      HSMul.hSMul (β := F)
        (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)

Tactic:
by_cases hx : 0 ≤ f x

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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
pos :
  ∀ (hx : Eq.{u_3 + 1} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
    HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F) ≤
      HSMul.hSMul (β := F)
        (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F)
pos₁ :
  ∀ (hx : LT.lt.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
    HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F) ≤
      HSMul.hSMul (β := F)
        (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)

Tactic:
obtain (hx | hx) := hx.eq_or_lt

Premises used: LE.le.eq_or_lt
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx_1 : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
hx : Eq.{u_3 + 1} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)

Tactic:
simp [← hx]
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx_1 : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
hx : LT.lt.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
pos :
  HSMul.hSMul (β := F)
      (ENNReal.toReal
        ((μ : (a : Set α) → ℝ≥0∞)
          (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F)))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ENNReal.toReal
        ((ν : (a : Set α) → ℝ≥0∞)
          (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F)))))
      ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)

Tactic:
simp only [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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx_1 : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
hx : LT.lt.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
pos :
  Ne (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (β := F)
      (ENNReal.toReal
        ((μ : (a : Set α) → ℝ≥0∞)
          (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F)))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ENNReal.toReal
        ((ν : (a : Set α) → ℝ≥0∞)
          (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F)))))
      ((f : (a : α) → F) x : F)

Tactic:
gcongr
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx_1 : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
hx : LT.lt.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ Ne (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
integrable_iff.mp hfν (f x) hx.ne' |>.ne

Premises used: MeasureTheory.SimpleFunc.integrable_iff, LT.lt.ne', Iff.mp, DFunLike.coe, LT.lt.ne
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx_1 : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
hx : LT.lt.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ Ne (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact integrable_iff.mp hfν (f x) hx.ne' |>.ne

Premises used: MeasureTheory.SimpleFunc.integrable_iff, LT.lt.ne', Iff.mp, DFunLike.coe, LT.lt.ne
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
this :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simpa using (hμν _ |>.trans_eq this)

Premises used: LE.le.trans_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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
this :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
have A : μ (f ⁻¹' {f x}) = 0 := by simpa using (hμν _ |>.trans_eq this)
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
this :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
A :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)

Tactic:
simp [measureReal_def, A, this]

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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
neg :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)

Tactic:
suffices ν (f ⁻¹' {f x}) = 0 by
      have A : μ (f ⁻¹' {f x}) = 0 := by simpa using (hμν _ |>.trans_eq this)
      simp [measureReal_def, A, this]
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
neg :
  LE.le (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero, ← ae_iff.mp hf]

Premises used: MeasureTheory.ae_iff, Iff.mp, 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ LE.le (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} : ℝ≥0∞)

Tactic:
measure_mono fun y hy ↦ ?_

Premises used: MeasureTheory.measure_mono
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
neg :
  ∀ (y : α)
    (hy :
      Membership.mem (γ := Set α)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) y),
    Membership.mem (γ := Set α) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} y
⊢ LE.le (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} : ℝ≥0∞)

Tactic:
refine measure_mono fun y hy ↦ ?_

Premises used: MeasureTheory.measure_mono
-- 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
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
y : α
hy :
  Membership.mem (γ := Set α) (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F)))
    y
⊢ Membership.mem (γ := Set α) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} y

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc E 1 μ)
rw :
  Eq (α := ℝ) (∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc f) : (a : α) → E) {x}) * ‖x‖)
    (∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc f) : (a : α) → E) {x}) • ‖x‖)
⊢ ‖f‖ = SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Tactic:
rw [norm_eq_sum_mul f, (toSimpleFunc f).map_integral norm (SimpleFunc.integrable f) norm_zero]

Premises used: Norm.norm, norm_zero, MeasureTheory.Lp.simpleFunc.toSimpleFunc, MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul, MeasureTheory.L1.SimpleFunc.integrable, MeasureTheory.SimpleFunc.map_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc E 1 μ)
⊢ Eq (α := ℝ) (∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc f) : (a : α) → E) {x}) * ‖x‖)
    (∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc 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
F : Type u_3
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
rcases :
  ∀ (f : ↥(Lp ℝ 1 μ)) (s : α →ₛ ℝ) (hsf : AEEqFun.mk (⇑s : (a : α) → ℝ) ⋯ = (↑f : α →ₘ[μ] ℝ)),
    Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ)
      (Lp.posPart
        (↑(Subtype.mk (p := fun (x : ↥(Lp ℝ 1 μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ) x)
              f ⋯) :
          ↥(Lp ℝ 1 μ)))
⊢ Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ) (Lp.posPart (↑f : ↥(Lp ℝ 1 μ)))

Tactic:
rcases f with ⟨f, s, hsf⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : α →ₛ ℝ
hsf : AEEqFun.mk (⇑s : (a : α) → ℝ) ⋯ = (↑f : α →ₘ[μ] ℝ)
h :
  AEEqFun.mk (⇑s.posPart : (a : α) → ℝ) ⋯ =
    (↑(Lp.posPart
          (↑(Subtype.mk (p := fun (x : ↥(Lp ℝ 1 μ)) ↦
                Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ) x) f ⋯) :
            ↥(Lp ℝ 1 μ))) :
      α →ₘ[μ] ℝ)
⊢ Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ)
    (Lp.posPart
      (↑(Subtype.mk (p := fun (x : ↥(Lp ℝ 1 μ)) ↦ Membership.mem (γ := AddSubgroup ↥(Lp ℝ 1 μ)) (simpleFunc ℝ 1 μ) x) f
            ⋯) :
        ↥(Lp ℝ 1 μ)))

Tactic:
use s.posPart

Premises used: MeasureTheory.SimpleFunc.posPart