awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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 ℝ (iteratedDerivWithin 1 f [[a, b]]) [[a, b]]

Tactic:
exact ContDiffOn.differentiableOn_iteratedDerivWithin h_f_c2 (by norm_cast) ud

Premises used: ContDiffOn.differentiableOn_iteratedDerivWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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]]

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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
trapezoidal_error_le h_df h_ddf fpp_bound N_nonzero

Premises used: trapezoidal_error_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
exact trapezoidal_error_le h_df h_ddf fpp_bound N_nonzero

Premises used: trapezoidal_error_le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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}
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}
⊢ 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∞)}

Tactic:
apply (countable_image_gt_image_Ioi F).mono

Premises used: Set.Countable.mono, countable_image_gt_image_Ioi
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
⊢ 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)
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < g a} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ g a} : ℝ≥0∞)
⊢ Membership.mem (γ := Set R) {x : R | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z} t

Tactic:
⟨μ {a | t < g a}, this, fun s hs ↦ measure_mono (fun a ha ↦ hs.trans_le ha)⟩

Premises used: Set.Mem, setOf, LT.lt.trans_le, And.intro, LT.lt, MeasureTheory.measure_mono, Exists.intro, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < g a} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ g a} : ℝ≥0∞)
⊢ Membership.mem (γ := Set R) {x : R | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z} t

Tactic:
exact ⟨μ {a | t < g a}, this, fun s hs ↦ measure_mono (fun a ha ↦ hs.trans_le ha)⟩
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
R : Type u_3
inst_1 : LinearOrder R
inst_2 : MeasurableSpace R
ν : Measure R
inst_3 : NoAtoms ν
g : α → R
⊢ (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (t : R) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ g a}) fun (t : R) ↦
    (μ : (a : Set α) → ℝ≥0∞) {a : α | t < g a}

Tactic:
Set.Countable.measure_zero (countable_meas_le_ne_meas_lt μ g) _

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, Set.Countable.measure_zero, MeasureTheory.countable_meas_le_ne_meas_lt
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
inr : ∀ (h : 0 < t), IntervalIntegrable g volume 0 t
⊢ IntervalIntegrable g volume 0 t

Tactic:
rcases eq_or_lt_of_le ht with h | h

Premises used: eq_or_lt_of_le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
h : 0 = t
⊢ IntervalIntegrable g volume 0 t

Tactic:
simp [← h]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
h : 0 < t
⊢ IntervalIntegrable g volume 0 t

Tactic:
g_intble t h
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
h : 0 < t
⊢ IntervalIntegrable g volume 0 t

Tactic:
exact g_intble t h
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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 : ℝ), 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
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
ω : α
x : ℝ
hx : x ∈ Ioc 0 (f ω)
⊢ 0 x ≤ g x

Tactic:
g_nn x hx.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
h₁ h₂ : ∀ (x : ℝ) (hx : x ∈ Ioc 0 (f ω)), 0 x ≤ g x
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] g

Tactic:
filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))]
        with x hx using g_nn x hx.1

Premises used: measurableSet_Ioc, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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

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
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
rw :
  ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) =
    ENNReal.ofReal (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (x : ℝ) ↦ g x)
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]

Premises used: And.left, MeasureTheory.ofReal_integral_eq_lintegral_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
e_r :
  Eq (α := ℝ) (∫ (t : ℝ) in 0..f ω, g t)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (x : ℝ) ↦ g x)
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) =
    ENNReal.ofReal (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (x : ℝ) ↦ g x)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
⊢ Eq (α := ℝ) (∫ (t : ℝ) in 0..f ω, g t)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (x : ℝ) ↦ g x)

Tactic:
intervalIntegral.integral_of_le (f_nn ω)

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
⊢ Eq (α := ℝ) (∫ (t : ℝ) in 0..f ω, g t)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (x : ℝ) ↦ g x)

Tactic:
exact intervalIntegral.integral_of_le (f_nn ω)

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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)

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 ω)
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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 :
  ∫⁻ (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))
⊢ ∫⁻ (ω : α), 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_congr integrand_eq]

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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)
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))
⊢ ∫⁻ (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:
simp_rw [← lintegral_indicator measurableSet_Ioc]

Premises used: MeasureTheory.lintegral_indicator, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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
hf :
  AEMeasurable (α := α × ℝ) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (Function.uncurry fun (a : α) ↦ (Ioc 0 (f a)).indicator fun (t : ℝ) ↦ ENNReal.ofReal (g t)) (μ.prod volume)
⊢ ∫⁻ (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:
rw [← lintegral_indicator measurableSet_Ioi, lintegral_lintegral_swap]

Premises used: measurableSet_Ioi, MeasureTheory.lintegral_indicator, MeasureTheory.lintegral_lintegral_swap
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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)
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
⊢ ∫⁻ (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:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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)
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
⊢ 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:
funext s
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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 : ℝ
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)
⊢ 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)

Tactic:
funext a
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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)
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)
⊢ (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)

Premises used: Set.Ioc, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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 : 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:
simp only [h, show s ∈ Ioi (0 : ℝ) from h.1, show f a ∈ Ici s from h.2, indicator_of_mem,
          mul_one]

Premises used: Set.indicator_of_mem, And.right, And.left, mul_one
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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 : s ∉ Ioc 0 (f a)
⊢ s ∉ Ioc 0 (f a)

Tactic:
have h_copy := h
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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)
⊢ 0 < s → f a < s

Tactic:
simp only [mem_Ioc, not_and, not_le] at h

Premises used: not_le, Set.mem_Ioc, not_and
-- Module: Mathlib.MeasureTheory.Integral.Layercake
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)
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)
⊢ (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