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
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))
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,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have simp_rw : ∫⁻ (a : α), ENNReal.ofReal (∫ (t : ℝ) in 0..F a, G t) ∂μ =
  ∫⁻ (t : ℝ) in Ioi 0, HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ F a} : ℝ≥0∞) (ENNReal.ofReal (G t))
Tactic: simp_rw [lintegral_congr_ae eq₂, eq₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun (x : ℝ) ↦ 1
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}
have cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
Tactic: have cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t := fun _ _ =>
    intervalIntegrable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun (x : ℝ) ↦ 1
cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}
have key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, cst t) ∂μ =
  ∫⁻ (t : ℝ) in Ioi 0,
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (cst t))
Tactic: have key :=
    lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble cst_intble
      (Eventually.of_forall fun _ => zero_le_one)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun (x : ℝ) ↦ 1
cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, cst t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (cst t))
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}
have key₁ : ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}
Tactic: simp_rw [cst, ENNReal.ofReal_one, mul_one] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun (x : ℝ) ↦ 1
cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}
have rw : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ
Tactic: rw [← key]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun (x : ℝ) ↦ 1
cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ
have e_f : ∀ (ω : α), ENNReal.ofReal (f ω) = ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1)
Tactic: congr with ω
-- 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
⊢ ∫⁻ (ω : α), 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 rw : ∫⁻ (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: rw [lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_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
⊢ ∫⁻ (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
⊢ (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 :
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)),
  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 [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f]
    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
t : ℝ
ht :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)
⊢ 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 : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
have rw : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} =
  ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
Tactic: rw [lintegral_eq_lintegral_meas_le μ f_nn f_mble]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
⊢ ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} =
    ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
have h : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
  (fun (a : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a ≤ f a_1}) fun (a : ℝ) ↦
  (μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a < f a_1}
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
    (fun (a : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a ≤ f a_1}) fun (a : ℝ) ↦
    (μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a < f a_1}
have h : ∀ (t : ℝ)
  (ht :
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)
Tactic: filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f]
    with t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
t : ℝ
ht :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})
have key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
Tactic: have key := lintegral_eq_lintegral_meas_lt μ f_nn f_intble.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})
have lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
Tactic: have lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞ := Integrable.lintegral_lt_top f_intble
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})
have rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
Tactic: have rhs_finite : ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a} < ∞ := by simp only [← key, lhs_finite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})
have rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have rhs_integrand_finite : ∀ (t : ℝ), t > 0 → μ {a | t < f a} < ∞ :=
    fun t ht ↦ measure_gt_lt_top f_intble ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})
have h : ∫ (ω : α), f ω ∂μ = (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ).toReal
Tactic: convert! (ENNReal.toReal_eq_toReal_iff' lhs_finite.ne rhs_finite.ne).mpr key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : ∫ (ω : α), f ω ∂μ = (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ).toReal
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})
have h₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    μ.real {a : α | t < f a}) =
  (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
Tactic: convert! (ENNReal.toReal_eq_toReal_iff' lhs_finite.ne rhs_finite.ne).mpr key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a}) =
    (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
have h : ∀
  (aux :
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        μ.real {a_1 : α | a < f a_1}) =
      (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1})).toReal),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a}) =
    (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
Tactic: have aux := @integral_eq_lintegral_of_nonneg_ae _ _ ((volume : Measure ℝ).restrict (Set.Ioi 0))
      (fun t ↦ μ.real {a : α | t < f a}) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀
    (aux :
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          μ.real {a_1 : α | a < f a_1}) =
        (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1})).toReal),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        μ.real {a : α | t < f a}) =
      (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a}) =
    (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
have h₁ : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (t : ℝ) ↦ μ.real {a : α | t < f a}
Tactic: have aux := @integral_eq_lintegral_of_nonneg_ae _ _ ((volume : Measure ℝ).restrict (Set.Ioi 0))
      (fun t ↦ μ.real {a : α | t < f a}) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀
    (aux :
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          μ.real {a_1 : α | a < f a_1}) =
        (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1})).toReal),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        μ.real {a : α | t < f a}) =
      (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
h₁ :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (t : ℝ) ↦ μ.real {a : α | t < f a}
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a}) =
    (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
have h₂ : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : α | t < f a})
  (Measure.restrict volume (Ioi 0))
Tactic: have aux := @integral_eq_lintegral_of_nonneg_ae _ _ ((volume : Measure ℝ).restrict (Set.Ioi 0))
      (fun t ↦ μ.real {a : α | t < f a}) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
aux :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      μ.real {a_1 : α | a < f a_1}) =
    (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1})).toReal
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a}) =
    (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
have h : (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1})).toReal =
  (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
Tactic: rw [aux]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
aux :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      μ.real {a_1 : α | a < f a_1}) =
    (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1})).toReal
⊢ (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1})).toReal =
    (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal
have h : ∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1}) =
  ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
aux :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      μ.real {a_1 : α | a < f a_1}) =
    (∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1})).toReal
⊢ ∫⁻ (a : ℝ) in Ioi 0, ENNReal.ofReal (μ.real {a_1 : α | a < f a_1}) =
    ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
have h : EqOn (β := ℝ≥0∞) (fun (x : ℝ) ↦ ENNReal.ofReal (μ.real {a : α | x < f a}))
  (fun (x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | x < f a}) (Ioi 0)
Tactic: apply setLIntegral_congr_fun measurableSet_Ioi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : α | t < f a})
    (Measure.restrict volume (Ioi 0))
have h : Measurable (β := ℝ) fun (t : ℝ) ↦ μ.real {a : α | t < f a}
Tactic: apply Measurable.aestronglyMeasurable