-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite
    (μ : Measure α) [SFinite μ]
    (f_nn : 0 ≤ f) (f_mble : Measurable f)
    (g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t) (g_mble : Measurable g)
    (g_nn : ∀ t > 0, 0 ≤ g t) :
    ∫⁻ ω, ENNReal.ofReal (∫ t in (0)..f ω, g t) ∂μ =
      ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t)

Proof state:
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => (Ioc 0 (f x)).indicator (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x => 1) s * (Ici s).indicator (fun x => 1) (f x)
⊢ ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun t => ENNReal.ofReal (g t)) s ∂μ =
    (Ioi 0).indicator (fun t => μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

Tactic:
simp_rw [aux₁]

Result:
case h.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => (Ioc 0 (f x)).indicator (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x => 1) s * (Ici s).indicator (fun x => 1) (f x)
⊢ ∫⁻ (x : α), ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x => 1) s * (Ici s).indicator (fun x => 1) (f x) ∂μ =
    (Ioi 0).indicator (fun t => μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
⊢ (Ioc 0 (f a)).indicator (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x => 1) s * (Ici s).indicator (fun x => 1) (f a)

Tactic:
have : s ∉ Ioi (0 : ℝ) := h'

Result:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
this : s ∉ Ioi 0
⊢ (Ioc 0 (f a)).indicator (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x => 1) s * (Ici s).indicator (fun x => 1) (f a)

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h h_copy : s ∉ Ioc 0 (f a)
⊢ (Ioc 0 (f a)).indicator (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x => 1) s * (Ici s).indicator (fun x => 1) (f a)

Tactic:
simp only [mem_Ioc, not_and, not_le] at h

Result:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
⊢ (Ioc 0 (f a)).indicator (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x => 1) s * (Ici s).indicator (fun x => 1) (f a)

Proof state:
case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => (Ioc 0 (f x)).indicator (fun t => ENNReal.ofReal (g t)) y) =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2)
⊢ AEMeasurable ({p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2)) (μ.prod volume)

Tactic:
have mble₀ : MeasurableSet {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := by
  simpa only [mem_univ, Pi.zero_apply, true_and] using
    measurableSet_region_between_oc measurable_zero f_mble MeasurableSet.univ

Result:
case hf
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => (Ioc 0 (f x)).indicator (fun t => ENNReal.ofReal (g t)) y) =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2)
mble₀ : MeasurableSet {p | p.2 ∈ Ioc 0 (f p.1)}
⊢ AEMeasurable ({p | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2)) (μ.prod volume)