α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : MeasureTheory.Measure α
β : Type ?u.997875
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t < f a} * ENNReal.ofReal (g t)
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : MeasureTheory.Measure α
β : Type ?u.997875
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t < f a} * ENNReal.ofReal (g t)
rw [lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn]
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : MeasureTheory.Measure α
β : Type ?u.997875
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ (fun a => ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a)) =ᵐ[Measure.restrict volume (Ioi 0)] fun a =>
    ↑↑μ {a_1 | a < f a_1} * ENNReal.ofReal (g a)
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : MeasureTheory.Measure α
β : Type ?u.997875
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t < f a} * ENNReal.ofReal (g t)
apply lintegral_congr_ae
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : MeasureTheory.Measure α
β : Type ?u.997875
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
t : ℝ
ht : ↑↑μ {a | t ≤ f a} = ↑↑μ {a | t < f a}
⊢ ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ↑↑μ {a | t < f a} * ENNReal.ofReal (g t)
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : MeasureTheory.Measure α
β : Type ?u.997875
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ (fun a => ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a)) =ᵐ[Measure.restrict volume (Ioi 0)] fun a =>
    ↑↑μ {a_1 | a < f a_1} * ENNReal.ofReal (g a)
filter_upwards [Measure.meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f_mble] with t ht
no goals
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : MeasureTheory.Measure α
β : Type ?u.997875
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
t : ℝ
ht : ↑↑μ {a | t ≤ f a} = ↑↑μ {a | t < f a}
⊢ ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ↑↑μ {a | t < f a} * ENNReal.ofReal (g t)
rw [ht]