awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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 (∫ (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)
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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 (∫ (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

Premises used: ENNReal.ofReal_one, mul_one
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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}
rw : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}

Tactic:
rw [← key]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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}
e_f : ∀ (ω : α), ENNReal.ofReal (f ω) = ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ

Tactic:
congr with ω
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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)

Tactic:
simp only [intervalIntegral.integral_const, sub_zero, smul_eq_mul, mul_one]

Premises used: sub_zero, smul_eq_mul, mul_one, intervalIntegral.integral_const
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
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))
⊢ ∫⁻ (ω : α), 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:
rw [lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn]

Premises used: MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
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))
⊢ ∫⁻ (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:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
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))
⊢ (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:
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f]
    with t ht

Premises used: Set.Ioi, MeasureTheory.meas_le_ae_eq_meas_lt, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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∞)
h 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))
⊢ 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]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
rw :
  ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} =
    ∫⁻ (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}

Tactic:
rw [lintegral_eq_lintegral_meas_le μ f_nn f_mble]

Premises used: MeasureTheory.lintegral_eq_lintegral_meas_le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
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}
⊢ ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} =
    ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
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∞)
⊢ (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:
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f]
    with t ht

Premises used: Set.Ioi, MeasureTheory.meas_le_ae_eq_meas_lt, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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∞)
h h₁ :
  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:
rw [ht]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (ω : α), 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
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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}
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞

Tactic:
have lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞ := Integrable.lintegral_lt_top f_intble
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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 ω) ∂μ < ∞
⊢ ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞

Tactic:
simp only [← key, lhs_finite]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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 ω) ∂μ < ∞
⊢ ∫⁻ (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]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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} < ∞
⊢ ∀ 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
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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∞)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ).toReal =
    (∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}).toReal

Tactic:
(ENNReal.toReal_eq_toReal_iff' lhs_finite.ne rhs_finite.ne).mpr key

Premises used: Iff.mpr, ENNReal.toReal_eq_toReal_iff', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
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
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})

Tactic:
convert! (ENNReal.toReal_eq_toReal_iff' lhs_finite.ne rhs_finite.ne).mpr key

Premises used: Iff.mpr, ENNReal.toReal_eq_toReal_iff', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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∞)
⊢ ∫ (ω : α), f ω ∂μ = (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ).toReal

Tactic:
integral_eq_lintegral_of_nonneg_ae f_nn f_intble.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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∞)
⊢ ∫ (ω : α), f ω ∂μ = (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ).toReal

Tactic:
exact integral_eq_lintegral_of_nonneg_ae f_nn f_intble.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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}
h₂ :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : α | t < f a})
    (Measure.restrict volume (Ioi 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

Tactic:
have aux := @integral_eq_lintegral_of_nonneg_ae _ _ ((volume : Measure ℝ).restrict (Set.Ioi 0))
      (fun t ↦ μ.real {a : α | t < f a}) ?_ ?_
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
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
⊢ (@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:
rw [aux]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
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}
⊢ (∫⁻ (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:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
h :
  EqOn (β := ℝ≥0∞) (fun (x : ℝ) ↦ ENNReal.ofReal (μ.real {a : α | x < f a}))
    (fun (x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | x < f a}) (Ioi 0)
⊢ ∫⁻ (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:
apply setLIntegral_congr_fun measurableSet_Ioi

Premises used: MeasureTheory.setLIntegral_congr_fun, measurableSet_Ioi
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
⊢ EqOn (β := ℝ≥0∞) (fun (x : ℝ) ↦ ENNReal.ofReal (μ.real {a : α | x < f a}))
    (fun (x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | x < f a}) (Ioi 0)

Tactic:
fun t t_pos ↦ ENNReal.ofReal_toReal (rhs_integrand_finite t t_pos).ne

Premises used: MeasureTheory.Measure.real, ENNReal.ofReal_toReal, Set.EqOn, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
⊢ EqOn (β := ℝ≥0∞) (fun (x : ℝ) ↦ ENNReal.ofReal (μ.real {a : α | x < f a}))
    (fun (x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | x < f a}) (Ioi 0)

Tactic:
exact fun t t_pos ↦ ENNReal.ofReal_toReal (rhs_integrand_finite t t_pos).ne

Premises used: ENNReal.ofReal_toReal, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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∞)
x : ℝ
⊢ LE.le (α := ℝ) (0 x) ((fun (t : ℝ) ↦ μ.real {a : α | t < f a}) x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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∞)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (t : ℝ) ↦ μ.real {a : α | t < f a}

Tactic:
exact Eventually.of_forall (fun x ↦ by positivity)

Premises used: Filter.Eventually.of_forall