-- 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:
α : 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
⊢ ∀ t > 0, IntervalIntegrable G volume 0 t

Tactic:
refine fun t t_pos => ⟨(g_intble t t_pos).1.congr_fun_ae (g_eq_G_on t), ?_⟩

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
t : ℝ
t_pos : t > 0
⊢ IntegrableOn G (Ioc t 0) volume

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

Tactic:
have G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t := by
  refine fun t t_pos => ⟨(g_intble t t_pos).1.congr_fun_ae (g_eq_G_on t), ?_⟩
  rw [Ioc_eq_empty_of_le t_pos.lt.le]
  exact integrableOn_empty

Result:
case 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
⊢ ∫⁻ (ω : α), 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
⊢ (fun a => μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a)) =ᶠ[ae (volume.restrict (Ioi 0))] fun a =>
    μ {a_1 | a ≤ F a_1} * ENNReal.ofReal (G a)

Tactic:
filter_upwards [g_eq_G] with t 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 h.e_r
α : 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 ω
⊢ ∫ (t : ℝ) in 0 ..F ω, g t = ∫ (t : ℝ) in 0 ..F ω, G t

Tactic:
refine intervalIntegral.integral_congr_ae ?_

Result:
case h.e_r
α : 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 ω
⊢ ∀ᵐ (x : ℝ), x ∈ Ι 0 (F ω) → g x = G x

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
t : ℝ
t_pos : t > 0
⊢ IntegrableOn G (Ioc t 0) volume

Tactic:
rw [Ioc_eq_empty_of_le t_pos.lt.le]

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
t : ℝ
t_pos : t > 0
⊢ IntegrableOn G ∅ volume

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
t : ℝ
t_pos : t > 0
⊢ IntegrableOn G ∅ volume

Tactic:
exact integrableOn_empty

Result:
no goals

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
ω : α
hω : f ω = AEMeasurable.mk f f_mble ω
h'ω : 0 ω ≤ f ω
⊢ f ω = f ω ⊔ 0

Tactic:
exact (max_eq_left h'ω).symm

Result:
no goals