-- 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:
α : 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)
⊢ ∫⁻ (a : α), ∫⁻ (t : ℝ) in Ioc 0 (f a), ENNReal.ofReal (g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
simp_rw [← lintegral_indicator measurableSet_Ioc]

Result:
α : 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)
⊢ ∫⁻ (a : α), ∫⁻ (a_1 : ℝ), (Ioc 0 (f a)).indicator (fun t => ENNReal.ofReal (g t)) a_1 ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Proof state:
α : 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
ω : α
g_ae_nn : 0 ≤ᶠ[ae (volume.restrict (Ioc 0 (f ω)))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]

Result:
α : 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
ω : α
g_ae_nn : 0 ≤ᶠ[ae (volume.restrict (Ioc 0 (f ω)))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ENNReal.ofReal (∫ (x : ℝ) in Ioc 0 (f ω), g x ∂volume)

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 : α), 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

Tactic:
rw [lintegral_const_mul']

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)
⊢ ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x => 1) s * ∫⁻ (a : α), (Ici s).indicator (fun x => 1) (f a) ∂μ =
    (Ioi 0).indicator (fun t => μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

case h.h.hr
α : 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)
⊢ ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x => 1) s ≠ ⊤

Proof state:
case pos
α : 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)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
⊢ (Ioc 0 (f p_fst)).indicator (fun t => ENNReal.ofReal (g t)) p_snd =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator (fun p => ENNReal.ofReal (g p.2)) (p_fst, p_snd)

Tactic:
have h' : (p_fst, p_snd) ∈ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h

Result:
case pos
α : 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)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
h' : (p_fst, p_snd) ∈ {p | p.2 ∈ Ioc 0 (f p.1)}
⊢ (Ioc 0 (f p_fst)).indicator (fun t => ENNReal.ofReal (g t)) p_snd =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator (fun p => ENNReal.ofReal (g p.2)) (p_fst, p_snd)

Proof state:
α : 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)
⊢ (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)

Tactic:
funext p

Result:
case 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)
p : α × ℝ
⊢ Function.uncurry (fun x y => (Ioc 0 (f x)).indicator (fun t => ENNReal.ofReal (g t)) y) p =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator (fun p => ENNReal.ofReal (g p.2)) p