α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
set cst := fun t : ℝ => (1 : ℝ)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
have cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t := fun _ _ =>
  intervalIntegrable_const
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, cst t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (cst t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
have key :=
  lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble cst_intble
    (eventually_of_forall fun _ => zero_le_one)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key : (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key :
  (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, cst t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (cst t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
simp_rw [ENNReal.ofReal_one, mul_one] at key
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key : (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key : (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
rw [← key]
case e_f.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key : (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
ω : α
⊢ ENNReal.ofReal (f ω) = ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key : (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ) = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ
congr with ω
no goals
case e_f.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun t => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key : (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ) = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
ω : α
⊢ ENNReal.ofReal (f ω) = ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1)
simp only [intervalIntegral.integral_const, sub_zero, Algebra.id.smul_eq_mul, mul_one]