awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
inl :
  ∀ (h_eq : a = b),
    |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have inr : ∀ (h_ne : a ≠ b),
  |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
Tactic: rcases eq_or_ne a b with h_eq | h_ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have ud : UniqueDiffOn ℝ [[a, b]]
Tactic: have ud : UniqueDiffOn ℝ [[a, b]] := uniqueDiffOn_Icc (inf_lt_sup.mpr h_ne)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
ud : UniqueDiffOn ℝ [[a, b]]
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have h_df : DifferentiableOn ℝ f [[a, b]]
Tactic: have h_df : DifferentiableOn ℝ f [[a, b]] := ContDiffOn.differentiableOn h_f_c2 two_ne_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
ud : UniqueDiffOn ℝ [[a, b]]
h_df : DifferentiableOn ℝ f [[a, b]]
⊢ DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
have rw : DifferentiableOn ℝ (iteratedDerivWithin 1 f [[a, b]]) [[a, b]]
Tactic: rw [← iteratedDerivWithin_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
ud : UniqueDiffOn ℝ [[a, b]]
h_df : DifferentiableOn ℝ f [[a, b]]
⊢ LT.lt (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 2
have norm_cast : LT.lt (α := ℕ) 1 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
ud : UniqueDiffOn ℝ [[a, b]]
h_df : DifferentiableOn ℝ f [[a, b]]
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
Tactic: have h_ddf : DifferentiableOn ℝ (derivWithin f [[a, b]]) [[a, b]] := by
    rw [← iteratedDerivWithin_one]
    exact ContDiffOn.differentiableOn_iteratedDerivWithin h_f_c2 (by norm_cast) ud
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
R : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun (t : R) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ g a}
⊢ Set.Countable.{u_2} (α := R)
    {t : R |
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ g a} : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < g a} : ℝ≥0∞)}
have apply : Subset.{u_2} (α := Set R)
  {t : R |
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ g a} : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < g a} : ℝ≥0∞)}
  {x : R | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}
Tactic: apply (countable_image_gt_image_Ioi F).mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
R : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun (t : R) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ g a}
t : R
ht :
  Membership.mem (γ := Set R)
    {t : R |
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ g a} : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < g a} : ℝ≥0∞)}
    t
⊢ Membership.mem (γ := Set R) {x : R | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z} t
have this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < g a} : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ g a} : ℝ≥0∞)
Tactic: have : μ {a | t < g a} < μ {a | t ≤ g a} :=
    lt_of_le_of_ne (measure_mono (fun a ha ↦ le_of_lt ha)) (Ne.symm ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
t : ℝ
ht : 0 ≤ t
⊢ IntervalIntegrable g volume 0 t
have inl : ∀ (h : 0 = t), IntervalIntegrable g volume 0 t
Tactic: rcases eq_or_lt_of_le ht with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
t : ℝ
ht : 0 ≤ t
inl : ∀ (h : 0 = t), IntervalIntegrable g volume 0 t
⊢ IntervalIntegrable g volume 0 t
have inr : ∀ (h : 0 < t), IntervalIntegrable g volume 0 t
Tactic: rcases eq_or_lt_of_le ht with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 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 g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
Tactic: have g_intble' : ∀ t : ℝ, 0 ≤ t → IntervalIntegrable g volume 0 t := by
    intro t ht
    rcases eq_or_lt_of_le ht with h | h
    · simp [← h]
    · exact g_intble t h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] g
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ | x ∈ Ioc 0 (f ω) → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ g x) x} x} a
Tactic: filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))]
        with x hx using g_nn x hx.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ | x ∈ Ioc 0 (f ω) → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ g x) x} x} a
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] g
have h₁ : ∀ a ∈ Ioc 0 (f ω), 0 a ≤ g a
Tactic: filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))]
        with x hx using g_nn x hx.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
have g_ae_nn : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] g
Tactic: have g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g := by
      filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))]
        with x hx using g_nn x hx.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
have rw : ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) =
  ENNReal.ofReal (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (x : ℝ) ↦ g x)
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) =
    ENNReal.ofReal (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (x : ℝ) ↦ g x)
have e_r : Eq (α := ℝ) (∫ (t : ℝ) in 0..f ω, g t)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (x : ℝ) ↦ g x)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → 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 integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
Tactic: have integrand_eq : ∀ ω,
      ENNReal.ofReal (∫ t in 0..f ω, g t) = ∫⁻ t in Ioc 0 (f ω), ENNReal.ofReal (g t) := by
    intro ω
    have g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g := by
      filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))]
        with x hx using g_nn x hx.1
    rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]
    congr
    exact intervalIntegral.integral_of_le (f_nn ω)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), 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 rw : ∫⁻ (a : α), ∫⁻ (t : ℝ) in Ioc 0 (f a), 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_congr integrand_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (a : α), ∫⁻ (t : ℝ) in Ioc 0 (f a), ENNReal.ofReal (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 : α), ∫⁻ (a_1 : ℝ), (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) a_1 ∂μ =
  ∫⁻ (t : ℝ) in Ioi 0, HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: simp_rw [← lintegral_indicator measurableSet_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (a : α), ∫⁻ (a_1 : ℝ), (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) a_1 ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have rw : ∫⁻ (y : ℝ), ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y ∂μ =
  ∫⁻ (a : ℝ),
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) a
Tactic: rw [← lintegral_indicator measurableSet_Ioi, lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
rw :
  ∫⁻ (y : ℝ), ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y ∂μ =
    ∫⁻ (a : ℝ),
      indicator (Ioi 0)
        (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)))
        a
⊢ ∫⁻ (a : α), ∫⁻ (a_1 : ℝ), (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) a_1 ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have hf : AEMeasurable (α := α × ℝ) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
  (Function.uncurry fun (a : α) ↦ (Ioc 0 (f a)).indicator fun (t : ℝ) ↦ ENNReal.ofReal (g t)) (μ.prod volume)
Tactic: rw [← lintegral_indicator measurableSet_Ioi, lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (y : ℝ), ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y ∂μ =
    ∫⁻ (a : ℝ),
      indicator (Ioi 0)
        (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)))
        a
have h : Eq (α := (y : ℝ) → ℝ≥0∞) (fun (y : ℝ) ↦ ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y ∂μ)
  fun (a : ℝ) ↦
  indicator (Ioi 0)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) a
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ Eq (α := (y : ℝ) → ℝ≥0∞) (fun (y : ℝ) ↦ ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y ∂μ)
    fun (a : ℝ) ↦
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) a
have h : ∀ (s : ℝ),
  ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
Tactic: funext s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
⊢ Eq.{u_1 + 1} (α := (x : α) → ℝ≥0∞) (fun (x : α) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s)
    fun (x : α) ↦
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f x)
have h : ∀ (a : α),
  (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
Tactic: funext a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
⊢ (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
have pos : ∀ (h : s ∈ Ioc 0 (f a)),
  (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
Tactic: by_cases h : s ∈ Ioc (0 : ℝ) (f a)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
pos :
  ∀ (h : s ∈ Ioc 0 (f a)),
    (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
      ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
⊢ (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
have neg : ∀ (h : s ∉ Ioc 0 (f a)),
  (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
Tactic: by_cases h : s ∈ Ioc (0 : ℝ) (f a)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h h_copy : s ∉ Ioc 0 (f a)
⊢ (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
have h₁ : 0 < s → f a < s
Tactic: simp only [mem_Ioc, not_and, not_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
⊢ (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
have pos : ∀ (h' : 0 < s),
  (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
Tactic: by_cases h' : 0 < s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst_1 : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
pos :
  ∀ (h' : 0 < s),
    (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
      ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
⊢ (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
have neg : ∀ (h' : ¬0 < s),
  (Ioc 0 (f a)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)
Tactic: by_cases h' : 0 < s