-- 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 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 : ℝ
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)
h : ¬0 < s
⊢ (Ioi 0).indicator (fun x => 1) s ≠ ⊤

Tactic:
simp [h]

Result:
no goals

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

Tactic:
rw [lintegral_one, Measure.restrict_apply MeasurableSet.univ, univ_inter, indicator_mul_left,
  mul_assoc,
  show
    (Ioi 0).indicator (fun _x : ℝ => (1 : ℝ≥0∞)) s * μ {a : α | s ≤ f a} =
      (Ioi 0).indicator (fun _x : ℝ => 1 * μ {a : α | s ≤ f a}) s
    by by_cases h : 0 < s <;> simp [h]]

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 * μ {a | s ≤ f a}) s =
    (Ioi 0).indicator (fun t => μ {a | t ≤ f a}) s * ENNReal.ofReal (g 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)
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:
simp only [h_copy, h h', indicator_of_not_mem, not_false_iff, mem_Ici, not_le, mul_zero]

Result:
no goals

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)
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)
⊢ (Ioi 0).indicator (fun _x => 1) s * μ {a | s ≤ f a} = (Ioi 0).indicator (fun _x => 1 * μ {a | s ≤ f a}) s

Tactic:
by_cases h : 0 < s <;> simp [h]

Result:
no goals

Proof state:
case e_r
α : 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
⊢ ∫ (t : ℝ) in 0 ..f ω, g t = ∫ (x : ℝ) in Ioc 0 (f ω), g x ∂volume

Tactic:
exact intervalIntegral.integral_of_le (f_nn ω)

Result:
no goals

Proof state:
case inr
α : 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
t : ℝ
ht : 0 ≤ t
h : 0 < t
⊢ IntervalIntegrable g volume 0 t

Tactic:
exact g_intble t h

Result:
no goals

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
⊢ ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t

Tactic:
intro t ht

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
t : ℝ
ht : 0 ≤ t
⊢ IntervalIntegrable g volume 0 t

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)
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)

Tactic:
rw [Set.indicator_of_mem h', Set.indicator_of_mem h]

Result:
no goals