awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 t))] G
⊢ ∀ t > 0, IntervalIntegrable G volume 0 t
have refine : ∀ (t : ℝ) (t_pos : t > 0), IntegrableOn (mα := Real.measurableSpace) G (Ioc t 0) volume
Tactic: refine fun t t_pos => ⟨(g_intble t t_pos).1.congr_fun_ae (g_eq_G_on t), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 t))] G
t : ℝ
t_pos : t > 0
⊢ IntegrableOn (mα := Real.measurableSpace) G (Ioc t 0) volume
have rw : IntegrableOn (mα := Real.measurableSpace) G ∅ volume
Tactic: rw [Ioc_eq_empty_of_le t_pos.lt.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 t))] G
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have G_intble : ∀ t > 0, IntervalIntegrable G volume 0 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
⊢ ∃ (F : α → ℝ), Measurable F ∧ 0 ≤ F ∧ f =ᶠ[ae μ] F
have refine : f =ᶠ[ae μ] fun (ω : α) ↦ max (AEMeasurable.mk f f_mble ω) 0
Tactic: refine ⟨fun ω ↦ max (f_mble.mk f ω) 0, f_mble.measurable_mk.max measurable_const,
        fun ω ↦ le_max_right _ _, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
⊢ f =ᶠ[ae μ] fun (ω : α) ↦ max (AEMeasurable.mk f f_mble ω) 0
have h : ∀ (ω : α) (hω : f ω = AEMeasurable.mk f f_mble ω) (h'ω : 0 ω ≤ f ω), f ω = max (AEMeasurable.mk f f_mble ω) 0
Tactic: filter_upwards [f_mble.ae_eq_mk, f_nn] with ω hω h'ω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 t))] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
ω : α
hω : f ω = AEMeasurable.mk f f_mble ω
h'ω : 0 ω ≤ f ω
⊢ f ω = max (AEMeasurable.mk f f_mble ω) 0
have h : f ω = max (f ω) 0
Tactic: rw [← hω]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have obtain : ∀ (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: obtain ⟨F, F_mble, F_nn, f_eq_F⟩ : ∃ F : α → ℝ, Measurable F ∧ 0 ≤ F ∧ f =ᵐ[μ] F := by
    refine ⟨fun ω ↦ max (f_mble.mk f ω) 0, f_mble.measurable_mk.max measurable_const,
        fun ω ↦ le_max_right _ _, ?_⟩
    filter_upwards [f_mble.ae_eq_mk, f_nn] with ω hω h'ω
    rw [← hω]
    exact (max_eq_left h'ω).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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 : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
have h : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
  (fun (a : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a ≤ f a_1} : ℝ≥0∞) (ENNReal.ofReal (g a)))
  fun (a : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a ≤ F a_1} : ℝ≥0∞) (ENNReal.ofReal (G a))
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
    (fun (a : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a ≤ f a_1} : ℝ≥0∞) (ENNReal.ofReal (g a)))
    fun (a : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a ≤ F a_1} : ℝ≥0∞) (ENNReal.ofReal (G a))
have h : ∀ (t : ℝ) (ht : g t = G t),
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
Tactic: filter_upwards [g_eq_G] with t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
have h : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (G t)) =
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (G t)) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞)
have h : {a : α | t ≤ f a} =ᶠ[ae μ] {a : α | t ≤ F a}
Tactic: apply measure_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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} =ᶠ[ae μ] {a : α | t ≤ F a}
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = F x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ {a : α | t ≤ f a} x = {a : α | t ≤ F a} x) x} x}
    a
Tactic: filter_upwards [f_eq_F] with a ha using by simp [setOf, ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = F x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ {a : α | t ≤ f a} x = {a : α | t ≤ F a} x) x} x}
      a
⊢ {a : α | t ≤ f a} =ᶠ[ae μ] {a : α | t ≤ F a}
have h₁ : ∀ (a : α), f a = F a → {a : α | t ≤ f a} a = {a : α | t ≤ F a} a
Tactic: filter_upwards [f_eq_F] with a ha using by simp [setOf, ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have eq₁ : ∫⁻ (t : ℝ) in Ioi 0, HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
  ∫⁻ (t : ℝ) in Ioi 0, HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
⊢ ∀ᵐ (ω : α) ∂μ, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)
have h : ∀ (ω : α) (fω_nn : f ω = F ω), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)
Tactic: filter_upwards [f_eq_F] with ω fω_nn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
ω : α
fω_nn : f ω = F ω
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)
have h : ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)
Tactic: rw [fω_nn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
ω : α
fω_nn : f ω = F ω
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)
have h : Eq (α := ℝ) (∫ (t : ℝ) in 0..F ω, g t) (∫ (t : ℝ) in 0..F ω, G t)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
ω : α
fω_nn : f ω = F ω
⊢ Eq (α := ℝ) (∫ (t : ℝ) in 0..F ω, g t) (∫ (t : ℝ) in 0..F ω, G t)
have h : ∀ᵐ (x : ℝ), x ∈ uIoc 0 (F ω) → g x = G x
Tactic: refine intervalIntegral.integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
ω : α
fω_nn : f ω = F ω
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (F ω) → g x = G x
have fω_nn₁ : 0 ≤ F ω
Tactic: have fω_nn : 0 ≤ F ω := F_nn ω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
ω : α
fω_nn_1 : f ω = F ω
fω_nn : 0 ≤ F ω
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (F ω) → g x = G x
have h : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc 0 (F ω)), g x = G x
Tactic: rw [uIoc_of_le fω_nn, ←
      ae_restrict_iff' (measurableSet_Ioc : MeasurableSet (Ioc (0 : ℝ) (F ω)))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : 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 : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have eq₂ : ∀ᵐ (ω : α) ∂μ, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)
Tactic: have eq₂ : ∀ᵐ ω ∂μ,
      ENNReal.ofReal (∫ t in 0..f ω, g t) = ENNReal.ofReal (∫ t in 0..F ω, G t) := by
    filter_upwards [f_eq_F] with ω fω_nn
    rw [fω_nn]
    congr 1
    refine intervalIntegral.integral_congr_ae ?_
    have fω_nn : 0 ≤ F ω := F_nn ω
    rw [uIoc_of_le fω_nn, ←
      ae_restrict_iff' (measurableSet_Ioc : MeasurableSet (Ioc (0 : ℝ) (F ω)))]
    exact g_eq_G_on (F ω)