α : Type u_1
β : Type ?u.980208
γ : Type ?u.980211
δ : Type ?u.980214
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hg_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
h_le : g ≤ᵐ[μ] f
⊢ ((∫⁻ (a : α), f a - g a ∂μ) + ∫⁻ (a : α), g a ∂μ) = ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.980208
γ : Type ?u.980211
δ : Type ?u.980214
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hg_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
h_le : g ≤ᵐ[μ] f
⊢ (∫⁻ (a : α), f a - g a ∂μ) = (∫⁻ (a : α), f a ∂μ) - ∫⁻ (a : α), g a ∂μ
refine' ENNReal.eq_sub_of_add_eq hg_fin _
α : Type u_1
β : Type ?u.980208
γ : Type ?u.980211
δ : Type ?u.980214
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hg_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
h_le : g ≤ᵐ[μ] f
⊢ (∫⁻ (a : α), f a - g a + g a ∂μ) = ∫⁻ (a : α), f a ∂μ
α : Type u_1
β : Type ?u.980208
γ : Type ?u.980211
δ : Type ?u.980214
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hg_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
h_le : g ≤ᵐ[μ] f
⊢ ((∫⁻ (a : α), f a - g a ∂μ) + ∫⁻ (a : α), g a ∂μ) = ∫⁻ (a : α), f a ∂μ
rw [← lintegral_add_right' _ hg]
no goals
α : Type u_1
β : Type ?u.980208
γ : Type ?u.980211
δ : Type ?u.980214
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
hg_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
h_le : g ≤ᵐ[μ] f
⊢ (∫⁻ (a : α), f a - g a + g a ∂μ) = ∫⁻ (a : α), f a ∂μ
exact lintegral_congr_ae (h_le.mono fun x hx => tsub_add_cancel_of_le hx)