case intro.intro.intro
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
⊢ (∫⁻ (a : α), f a ∂μ) ≤ ∫⁻ (a : α), g a ∂μ
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ (∫⁻ (a : α), f a ∂μ) ≤ ∫⁻ (a : α), g a ∂μ
rcases exists_measurable_superset_of_null h with ⟨t, hts, ht, ht0⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
⊢ (∫⁻ (a : α), f a ∂μ) ≤ ∫⁻ (a : α), g a ∂μ
case intro.intro.intro
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
⊢ (∫⁻ (a : α), f a ∂μ) ≤ ∫⁻ (a : α), g a ∂μ
have : ∀ᵐ x ∂μ, x ∉ t := measure_zero_iff_ae_nmem.1 ht0
case intro.intro.intro
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
⊢ (⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => f a), SimpleFunc.lintegral g μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => g a), SimpleFunc.lintegral g_1 μ
case intro.intro.intro
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
⊢ (∫⁻ (a : α), f a ∂μ) ≤ ∫⁻ (a : α), g a ∂μ
rw [lintegral, lintegral]
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
⊢ ↑(restrict s (tᶜ)) ≤ fun a => g a

case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
⊢ SimpleFunc.lintegral s μ ≤ SimpleFunc.lintegral (restrict s (tᶜ)) μ
case intro.intro.intro
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
⊢ (⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => f a), SimpleFunc.lintegral g μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞) (_ : ↑g_1 ≤ fun a => g a), SimpleFunc.lintegral g_1 μ
refine' iSup_le fun s => iSup_le fun hfs => le_iSup_of_le (s.restrict (tᶜ)) <| le_iSup_of_le _ _
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
a : α
⊢ ↑(restrict s (tᶜ)) a ≤ (fun a => g a) a
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
⊢ ↑(restrict s (tᶜ)) ≤ fun a => g a
intro a
case neg
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h✝ : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
a : α
h : ¬a ∈ t
⊢ ↑s a ≤ g a
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
a : α
⊢ ↑(restrict s (tᶜ)) a ≤ (fun a => g a) a
by_cases h : a ∈ t <;> simp [h, restrict_apply s ht.compl, ht.compl]
no goals
case neg
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h✝ : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
a : α
h : ¬a ∈ t
⊢ ↑s a ≤ g a
exact le_trans (hfs a) (_root_.by_contradiction fun hnfg => h (hts hnfg))
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
a : α
hnt : ¬a ∈ t
⊢ ↑s a = ↑(restrict s (tᶜ)) a
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
⊢ SimpleFunc.lintegral s μ ≤ SimpleFunc.lintegral (restrict s (tᶜ)) μ
refine' le_of_eq (SimpleFunc.lintegral_congr <| this.mono fun a hnt => _)
case pos
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
a : α
hnt : ¬a ∈ t
hat : a ∈ t
⊢ ↑s a = 0
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
a : α
hnt : ¬a ∈ t
⊢ ↑s a = ↑(restrict s (tᶜ)) a
by_cases hat : a ∈ t <;> simp [hat, restrict_apply s ht.compl]
no goals
case pos
α : Type u_1
β : Type ?u.290555
γ : Type ?u.290558
δ : Type ?u.290561
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a => f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : ↑↑μ t = 0
this : ∀ᵐ (x : α) ∂μ, ¬x ∈ t
s : α →ₛ ℝ≥0∞
hfs : ↑s ≤ fun a => f a
a : α
hnt : ¬a ∈ t
hat : a ∈ t
⊢ ↑s a = 0
exact (hnt hat).elim