awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
n : ℕ
hn : Membership.mem (γ := Set α) {x : α | u n ≤ f x} x
⊢ 0 < f x

Tactic:
(bu n).1.trans_le hn

Premises used: And.left, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
n : ℕ
hn : Membership.mem (γ := Set α) {x : α | u n ≤ f x} x
⊢ 0 < f x

Tactic:
exact (bu n).1.trans_le hn

Premises used: And.left, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | f x ≠ 0} (⋃ (n : ℕ), {x : α | u n ≤ f x})

Tactic:
have u_union : {x | f x ≠ 0} = ⋃ n, {x | u n ≤ f x} := by
    ext x
    rw [mem_iUnion, mem_setOf_eq, ← pos_iff_ne_zero]
    rw [ENNReal.tendsto_atTop_zero] at tu
    constructor <;> intro h'
    · obtain ⟨n, hn⟩ := tu _ h'; use n, hn _ le_rfl
    · obtain ⟨n, hn⟩ := h'; exact (bu n).1.trans_le hn
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
u_union : Eq.{u_1 + 1} (α := Set α) {x : α | f x ≠ 0} (⋃ (n : ℕ), {x : α | u n ≤ f x})
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), {x : α | u i ≤ f x}) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have res := measure_iUnion_null_iff.mpr fun n ↦ meas_levels_0 _ (bu n).1
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
u_union : Eq.{u_1 + 1} (α := Set α) {x : α | f x ≠ 0} (⋃ (n : ℕ), {x : α | u n ≤ f x})
res : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), {x : α | u i ≤ f x}) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (res : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)), f =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
rwa [← u_union] at res
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
lintegral_eq_zero_iff' hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_eq_zero_iff'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.restrict s)
⊢ ∫⁻ (a : α) in s, f a ∂μ = 0 ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0

Tactic:
(lintegral_eq_zero_iff' hf).trans (ae_restrict_iff' hs)

Premises used: MeasureTheory.lintegral_eq_zero_iff', Iff.trans, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α) in s, f a ∂μ = 0 ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0

Tactic:
setLIntegral_eq_zero_iff' hs hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.setLIntegral_eq_zero_iff'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ 0 < ∫⁻ (a : α), f a ∂μ ↔ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)

Tactic:
simp [pos_iff_ne_zero, hf, Filter.EventuallyEq, ae_iff, Function.support]

Premises used: Filter.EventuallyEq, MeasureTheory.ae_iff, Function.support, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞)
rw₁ rw₂ :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞)
⊢ 0 < ∫⁻ (a : α) in s, f a ∂μ ↔ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞)

Tactic:
rw [lintegral_pos_iff_support hf, Measure.restrict_apply (measurableSet_support hf)]

Premises used: measurableSet_support, MeasureTheory.Measure.restrict_apply, MeasureTheory.lintegral_pos_iff_support
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
rcases :
  ∀ (ε₂ : ℝ≥0∞) (hε₂0 : 0 < ε₂) (hε₂ε : ε₂ < ε),
    ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
⊢ ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

Tactic:
rcases exists_between (pos_iff_ne_zero.mpr hε) with ⟨ε₂, hε₂0, hε₂ε⟩

Premises used: Iff.mpr, exists_between, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
rcases :
  ∀ (ε₁ : ℝ≥0∞) (hε₁0 : 0 < ε₁) (hε₁₂ : ε₁ < ε₂),
    ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
⊢ ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

Tactic:
rcases exists_between hε₂0 with ⟨ε₁, hε₁0, hε₁₂⟩

Premises used: exists_between
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
rcases :
  ∀ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) →
      ∀
        (hφ :
          ∀ (ψ : α →ₛ ℝ≥0),
            (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁),
        ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
⊢ ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

Tactic:
rcases exists_simpleFunc_forall_lintegral_sub_lt_of_pos h hε₁0.ne' with ⟨φ, _, hφ⟩

Premises used: MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
rcases :
  ∀ (C : ℝ≥0) (hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C),
    ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
⊢ ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

Tactic:
rcases φ.exists_forall_le with ⟨C, hC⟩

Premises used: MeasureTheory.SimpleFunc.exists_forall_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
right : ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ < ε
⊢ ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

Tactic:
use (ε₂ - ε₁) / C, ENNReal.div_pos_iff.2 ⟨(tsub_pos_iff_lt.2 hε₁₂).ne', ENNReal.coe_ne_top⟩

Premises used: Iff.mpr, tsub_pos_iff_lt, ENNReal.div_pos_iff, HSub.hSub, LT.lt.ne', And.intro, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
⊢ ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ < ε

Tactic:
fun s hs => lt_of_le_of_lt ?_ hε₂ε

Premises used: lt_of_le_of_lt
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
right : ∀ (s : Set α) (hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)), ∫⁻ (x : α) in s, f x ∂μ ≤ ε₂
⊢ ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ < ε

Tactic:
refine fun s hs => lt_of_le_of_lt ?_ hε₂ε

Premises used: lt_of_le_of_lt
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
right :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral (μ.restrict s) ≤ ε₂
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ε₂

Tactic:
simp only [lintegral_eq_nnreal, iSup_le_iff]

Premises used: MeasureTheory.lintegral_eq_nnreal, iSup_le_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
rw :
  (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral (μ.restrict s)
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s)

Tactic:
rw [← SimpleFunc.add_lintegral, ← SimpleFunc.map_add @ENNReal.coe_add]

Premises used: MeasureTheory.SimpleFunc.map_add, ENNReal.coe_add, MeasureTheory.SimpleFunc.add_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral (μ.restrict s)

Tactic:
SimpleFunc.lintegral_mono (fun x => ?_) le_rfl

Premises used: le_rfl, MeasureTheory.SimpleFunc.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
refine :
  ∀ (x : α),
    LE.le (α := ℝ≥0∞) ((SimpleFunc.map ofNNReal ψ : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
      ((SimpleFunc.map ofNNReal (φ + (ψ - φ)) : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral (μ.restrict s)

Tactic:
refine SimpleFunc.lintegral_mono (fun x => ?_) le_rfl

Premises used: le_rfl, MeasureTheory.SimpleFunc.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
x : α
⊢ LE.le (α := ℝ≥0∞) ((SimpleFunc.map ofNNReal ψ : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
    ((SimpleFunc.map ofNNReal (φ + (ψ - φ)) : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
simp only [add_tsub_eq_max, le_max_right, coe_map, Function.comp_apply, SimpleFunc.coe_add,
        SimpleFunc.coe_sub, Pi.add_apply, Pi.sub_apply, ENNReal.coe_max (φ x) (ψ x)]

Premises used: le_max_right, MeasureTheory.SimpleFunc.coe_add, ENNReal.coe_max, MeasureTheory.SimpleFunc.coe_map, Pi.add_apply, MeasureTheory.SimpleFunc.coe_sub, Function.comp_apply, DFunLike.coe, Pi.sub_apply, add_tsub_eq_max
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
bc : (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤ ε₁
⊢ (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + ε₁

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤ ε₁

Tactic:
le_trans ?_ (hφ _ hψ).le

Premises used: LT.lt.le, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
bc : (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ
⊢ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤ ε₁

Tactic:
refine le_trans ?_ (hφ _ hψ).le

Premises used: LT.lt.le, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ

Tactic:
SimpleFunc.lintegral_mono le_rfl Measure.restrict_le_self

Premises used: le_rfl, MeasureTheory.Measure.restrict_le_self, MeasureTheory.SimpleFunc.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ

Tactic:
exact SimpleFunc.lintegral_mono le_rfl Measure.restrict_le_self

Premises used: le_rfl, MeasureTheory.Measure.restrict_le_self, MeasureTheory.SimpleFunc.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
bc : SimpleFunc.map ofNNReal φ ≤ const α (↑C : ℝ≥0∞)
⊢ (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + ε₁ ≤
    SimpleFunc.lintegral (const α (↑C : ℝ≥0∞)) (μ.restrict s) + ε₁

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ SimpleFunc.map ofNNReal φ ≤ const α (↑C : ℝ≥0∞)

Tactic:
fun x ↦ ENNReal.coe_le_coe.2 (hC x)

Premises used: Iff.mpr, ENNReal.ofNNReal, ENNReal.coe_le_coe, WithTop.some
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ SimpleFunc.map ofNNReal φ ≤ const α (↑C : ℝ≥0∞)

Tactic:
exact fun x ↦ ENNReal.coe_le_coe.2 (hC x)

Premises used: Iff.mpr, ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ SimpleFunc.lintegral (const α (↑C : ℝ≥0∞)) (μ.restrict s) + ε₁ =
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε₁

Tactic:
simp only [← SimpleFunc.lintegral_eq_lintegral, coe_const, lintegral_const,
        Measure.restrict_apply, MeasurableSet.univ, univ_inter, Function.const]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply, Set.univ_inter, Function.const, MeasureTheory.SimpleFunc.coe_const, MeasurableSet.univ, MeasureTheory.SimpleFunc.lintegral_eq_lintegral