-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem lintegral_comp_eq_lintegral_meas_le_mul_of_measurable (μ : Measure α)
    (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 pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (volume.restrict (Ioi 0))] 0
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
have B : ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) = 0 := by
  have : (fun t ↦ μ {a : α | t ≤ f a} * ENNReal.ofReal (g t))
    =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0 := by
      filter_upwards [H1] with t ht using by simp [ht]
  simp [lintegral_congr_ae this]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (volume.restrict (Ioi 0))] 0
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = 0
B : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = 0
⊢ ∫⁻ (ω : α), 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 α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ⊤
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ⊤
⊢ ∫⁻ (x : α) in {a | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0 ..s, g t) ∂μ ≤
    ∫⁻ (ω : α) in {a | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ

Tactic:
apply setLIntegral_mono' (measurableSet_lt measurable_const f_mble) (fun a ha ↦ ?_)

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ⊤
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ⊤
a : α
ha : a ∈ {a | s < f a}
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..s, g t) ≤ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f a, g t)

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (volume.restrict (Ioi 0))] 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
have A : ∫⁻ ω, ENNReal.ofReal (∫ t in (0)..f ω, g t) ∂μ = 0 := by
  have : ∀ ω, ∫ t in (0)..f ω, g t = ∫ t in (0)..f ω, 0 := by
    intro ω
    simp_rw [intervalIntegral.integral_of_le (f_nonneg ω)]
    apply integral_congr_ae
    exact ae_restrict_of_ae_restrict_of_subset Ioc_subset_Ioi_self H1
  simp [this]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (volume.restrict (Ioi 0))] 0
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (volume.restrict (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a | M < f a}
this : SigmaFinite ν
A :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂ν
t : ℝ
ht : g t = 0 t
⊢ μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ν {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
simp [ht]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ⊤
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ⊤
⊢ ⊤ = ∫⁻ (x : α) in {a | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0 ..s, g t) ∂μ

Tactic:
simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
  h's, ne_eq, ENNReal.ofReal_eq_zero, not_le]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (volume.restrict (Ioi 0))] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ⊤
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ⊤
⊢ ⊤ = ENNReal.ofReal (∫ (t : ℝ) in 0 ..s, g t) * ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
H1 : ¬BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
n : ℕ
⊢ g =ᶠ[ae (volume.restrict (Ioc 0 ↑n))] 0

Tactic:
rcases not_bddAbove_iff.1 H1 n with ⟨s, hs, ns⟩

Result:
case intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
H1 : ¬BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
n : ℕ
s : ℝ
hs : s ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
ns : ↑n < s
⊢ g =ᶠ[ae (volume.restrict (Ioc 0 ↑n))] 0