α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
⊢ (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), g x - f x ∂μ) + ∫⁻ (x : α), f x ∂μ
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
⊢ ((∫⁻ (x : α), g x ∂μ) - ∫⁻ (x : α), f x ∂μ) ≤ ∫⁻ (x : α), g x - f x ∂μ
rw [tsub_le_iff_right]
case pos
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hfi : (∫⁻ (x : α), f x ∂μ) = ⊤
⊢ (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), g x - f x ∂μ) + ∫⁻ (x : α), f x ∂μ

case neg
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hfi : ¬(∫⁻ (x : α), f x ∂μ) = ⊤
⊢ (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), g x - f x ∂μ) + ∫⁻ (x : α), f x ∂μ
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
⊢ (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), g x - f x ∂μ) + ∫⁻ (x : α), f x ∂μ
by_cases hfi : (∫⁻ x, f x ∂μ) = ∞
case pos
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hfi : (∫⁻ (x : α), f x ∂μ) = ⊤
⊢ (∫⁻ (x : α), g x ∂μ) ≤ ⊤
case pos
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hfi : (∫⁻ (x : α), f x ∂μ) = ⊤
⊢ (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), g x - f x ∂μ) + ∫⁻ (x : α), f x ∂μ
rw [hfi, add_top]
no goals
case pos
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hfi : (∫⁻ (x : α), f x ∂μ) = ⊤
⊢ (∫⁻ (x : α), g x ∂μ) ≤ ⊤
exact le_top
case neg
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hfi : ¬(∫⁻ (x : α), f x ∂μ) = ⊤
⊢ (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (a : α), g a - f a + f a ∂μ
case neg
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hfi : ¬(∫⁻ (x : α), f x ∂μ) = ⊤
⊢ (∫⁻ (x : α), g x ∂μ) ≤ (∫⁻ (x : α), g x - f x ∂μ) + ∫⁻ (x : α), f x ∂μ
rw [← lintegral_add_right' _ hf]
no goals
case neg
α : Type u_1
β : Type ?u.981881
γ : Type ?u.981884
δ : Type ?u.981887
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hfi : ¬(∫⁻ (x : α), f x ∂μ) = ⊤
⊢ (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (a : α), g a - f a + f a ∂μ
exact lintegral_mono fun x => le_tsub_add