-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem Integrable.integral_eq_integral_meas_lt
    (f_intble : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) :
    ∫ ω, f ω ∂μ = ∫ t in Set.Ioi 0, ENNReal.toReal (μ {a : α | t < f a})

Proof state:
case h.e'_3
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
⊢ ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal = (∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}).toReal

Tactic:
have aux := @integral_eq_lintegral_of_nonneg_ae _ _ ((volume : Measure ℝ).restrict (Set.Ioi 0))
  (fun t ↦ ENNReal.toReal (μ {a : α | t < f a})) ?_ ?_

Result:
case h.e'_3.refine_3
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
aux :
  ∫ (a : ℝ) in Ioi 0, (μ {a_1 | a < f a_1}).toReal =
    (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ {a_1 | a < f a_1}).toReal).toReal
⊢ ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal = (∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}).toReal

case h.e'_3.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
⊢ 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] fun t => (μ {a | t < f a}).toReal

case h.e'_3.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
⊢ AEStronglyMeasurable (fun t => (μ {a | t < f a}).toReal) (volume.restrict (Ioi 0))

Proof state:
case h.e'_3.refine_3.e_a
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
aux :
  ∫ (a : ℝ) in Ioi 0, (μ {a_1 | a < f a_1}).toReal =
    (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ {a_1 | a < f a_1}).toReal).toReal
⊢ ∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ {a_1 | a < f a_1}).toReal = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}

Tactic:
apply setLIntegral_congr_fun measurableSet_Ioi (Eventually.of_forall _)

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
aux :
  ∫ (a : ℝ) in Ioi 0, (μ {a_1 | a < f a_1}).toReal =
    (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ {a_1 | a < f a_1}).toReal).toReal
⊢ ∀ x ∈ Ioi 0, ENNReal.ofReal (μ {a | x < f a}).toReal = μ {a | x < f a}

Proof state:
case h.e'_3.refine_2.hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
⊢ Measurable fun t => μ {a | t < f a}

Tactic:
exact Antitone.measurable (fun _ _ hst ↦ measure_mono (fun _ h ↦ lt_of_le_of_lt hst h))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal

Tactic:
have rhs_integrand_finite : ∀ (t : ℝ), t > 0 → μ {a | t < f a} < ∞ :=
  fun t ht ↦ measure_gt_lt_top f_intble ht

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal

Proof state:
case h.e'_3.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
⊢ AEStronglyMeasurable (fun t => (μ {a | t < f a}).toReal) (volume.restrict (Ioi 0))

Tactic:
apply Measurable.aestronglyMeasurable

Result:
case h.e'_3.refine_2.hf
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
⊢ Measurable fun t => (μ {a | t < f a}).toReal

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤

Tactic:
simp only [← key, lhs_finite]

Result:
no goals

Proof state:
case h.e'_3.refine_3
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
aux :
  ∫ (a : ℝ) in Ioi 0, (μ {a_1 | a < f a_1}).toReal =
    (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ {a_1 | a < f a_1}).toReal).toReal
⊢ ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal = (∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}).toReal

Tactic:
rw [aux]

Result:
case h.e'_3.refine_3
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤
aux :
  ∫ (a : ℝ) in Ioi 0, (μ {a_1 | a < f a_1}).toReal =
    (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ {a_1 | a < f a_1}).toReal).toReal
⊢ (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ {a_1 | a < f a_1}).toReal).toReal =
    (∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}).toReal