-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem lintegral_comp_eq_lintegral_meas_le_mul (μ : Measure α) (f_nn : 0 ≤ᵐ[μ] f)
    (f_mble : AEMeasurable f μ) (g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t)
    (g_nn : ∀ᵐ t ∂volume.restrict (Ioi 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 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
ω : α
fω_nn : f ω = F ω
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0 ..F ω, G t)

Tactic:
rw [fω_nn]

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
ω : α
fω_nn : f ω = F ω
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..F ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0 ..F ω, G t)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
eq₂ : ∀ᵐ (ω : α) ∂μ, ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = 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)

Tactic:
simp_rw [lintegral_congr_ae eq₂, eq₁]

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
eq₂ : ∀ᵐ (ω : α) ∂μ, ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0 ..F ω, G t)
⊢ ∫⁻ (a : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..F a, 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 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
t : ℝ
ht : g t = G t
⊢ μ {a | t ≤ f a} * ENNReal.ofReal (g t) = μ {a | t ≤ F a} * ENNReal.ofReal (G t)

Tactic:
rw [ht]

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
t : ℝ
ht : g t = G t
⊢ μ {a | t ≤ f a} * ENNReal.ofReal (G t) = μ {a | t ≤ F a} * ENNReal.ofReal (G t)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
have eq₁ :
  ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ t in Ioi 0, μ {a : α | t ≤ F a} * ENNReal.ofReal (G t) := by
  apply lintegral_congr_ae
  filter_upwards [g_eq_G] with t ht
  rw [ht]
  congr 1
  apply measure_congr
  filter_upwards [f_eq_F] with a ha using by simp [setOf, ha]

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᶠ[ae μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (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 α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
⊢ ∃ F, Measurable F ∧ 0 ≤ F ∧ f =ᶠ[ae μ] F

Tactic:
refine ⟨fun ω ↦ max (f_mble.mk f ω) 0, f_mble.measurable_mk.max measurable_const,
    fun ω ↦ le_max_right _ _, ?_⟩

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (volume.restrict (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (volume.restrict (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
⊢ f =ᶠ[ae μ] fun ω => AEMeasurable.mk f f_mble ω ⊔ 0