-- 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 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) ∂ν
⊢ (fun a => μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a)) =ᶠ[ae (volume.restrict (Ioc 0 M))] fun a =>
    ν {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a)

Tactic:
filter_upwards [hgM] with t ht

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

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

Tactic:
have B1 : ∫⁻ t in Ioc 0 M, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t)
     = ∫⁻ t in Ioc 0 M, ν {a : α | t ≤ f a} * ENNReal.ofReal (g t) := by
  apply lintegral_congr_ae
  filter_upwards [hgM] with t ht
  simp [ht]

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
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) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioc 0 M, ν {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (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
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}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
⊢ ∀ (i : ℕ), ν ((fun n => {a | f a ≤ M} ∪ {a | u n < f a}) i) < ⊤

Tactic:
intro n

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
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}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
⊢ ν ((fun n => {a | f a ≤ M} ∪ {a | u n < f a}) n) < ⊤

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
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}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
I : ν {a | f a ≤ M} = 0
J : μ {a | u n < f a} < ⊤
⊢ ν {a | u n < f a} < ⊤

Tactic:
apply lt_of_le_of_lt _ J

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
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}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
I : ν {a | f a ≤ M} = 0
J : μ {a | u n < f a} < ⊤
⊢ ν {a | u n < f a} ≤ μ {a | u n < f a}