awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
aux₁ :
  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)
h :
  ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (_x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a}) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (t : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}) s
⊢ ENNReal.ofReal (g s) *
      indicator (Ioi 0)
        (fun (_x : ℝ) ↦
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞))
        s =
    indicator (Ioi 0) (fun (t : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}) s * ENNReal.ofReal (g s)

Tactic:
simp_rw [mul_comm _ (ENNReal.ofReal _), one_mul]

Premises used: ENNReal.ofReal, mul_comm, one_mul
-- 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 : ℝ
aux₁ :
  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)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (_x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a}) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (t : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a}) s

Tactic:
rfl
-- 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 :
  ∀ (p : α × ℝ),
    Eq (α := ℝ≥0∞)
      (Function.uncurry (fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y) p)
      (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) p)
⊢ Eq.{u_1 + 1} (α := α × ℝ → ℝ≥0∞)
    (Function.uncurry fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2))

Tactic:
funext p
-- 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)
p_fst : α
p_snd : ℝ
⊢ Eq (α := ℝ≥0∞)
    (Function.uncurry (fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y)
      (p_fst, p_snd))
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd))

Tactic:
?_
-- 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)
p : α × ℝ
h :
  ∀ (p_fst : α) (p_snd : ℝ),
    Eq (α := ℝ≥0∞)
      (Function.uncurry (fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y)
        (p_fst, p_snd))
      (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd))
⊢ Eq (α := ℝ≥0∞)
    (Function.uncurry (fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y) p)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) p)

Tactic:
cases p with | mk p_fst p_snd => ?_

Premises used: Filter.mk
-- 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)
p_fst : α
p_snd : ℝ
h :
  Eq (α := ℝ≥0∞) ((Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd))
⊢ Eq (α := ℝ≥0∞)
    (Function.uncurry (fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y)
      (p_fst, p_snd))
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd))

Tactic:
rw [Function.uncurry_apply_pair]

Premises used: Function.uncurry_apply_pair
-- 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)
p_fst : α
p_snd : ℝ
pos :
  ∀ (h : p_snd ∈ Ioc 0 (f p_fst)),
    Eq (α := ℝ≥0∞) ((Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd)
      (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd))
neg :
  ∀ (h : p_snd ∉ Ioc 0 (f p_fst)),
    Eq (α := ℝ≥0∞) ((Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd)
      (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd))
⊢ Eq (α := ℝ≥0∞) ((Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd))

Tactic:
by_cases h : p_snd ∈ Ioc 0 (f p_fst)

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)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
⊢ Membership.mem (γ := Set (α × ℝ)) {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (p_fst, p_snd)

Tactic:
have h' : (p_fst, p_snd) ∈ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := 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)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
h' : Membership.mem (γ := Set (α × ℝ)) {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (p_fst, p_snd)
pos : (Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd = ENNReal.ofReal (g (p_fst, p_snd).2)
pos₁ pos₂ : ENNReal.ofReal (g p_snd) = ENNReal.ofReal (g (p_fst, p_snd).2)
⊢ Eq (α := ℝ≥0∞) ((Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd))

Tactic:
rw [Set.indicator_of_mem h', Set.indicator_of_mem h]

Premises used: Set.indicator_of_mem
-- 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)
p_fst : α
p_snd : ℝ
h : p_snd ∉ Ioc 0 (f p_fst)
⊢ (p_fst, p_snd) ∉ {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)}

Tactic:
have h' : (p_fst, p_snd) ∉ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := 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)
p_fst : α
p_snd : ℝ
h : p_snd ∉ Ioc 0 (f p_fst)
h' : (p_fst, p_snd) ∉ {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)}
neg : Eq (α := ℝ≥0∞) ((Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd) 0
neg₁ neg₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} (fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd))

Tactic:
rw [Set.indicator_of_notMem h', Set.indicator_of_notMem h]

Premises used: Set.indicator_of_notMem
-- 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)
⊢ Eq.{u_1 + 1} (α := α × ℝ → ℝ≥0∞)
    (Function.uncurry fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2))

Tactic:
have aux₂ :
    (Function.uncurry fun (x : α) (y : ℝ) =>
        (Ioc 0 (f x)).indicator (fun t : ℝ => ENNReal.ofReal (g t)) y) =
      {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2) := by
    funext p
    cases p with | mk p_fst p_snd => ?_
    rw [Function.uncurry_apply_pair]
    by_cases h : p_snd ∈ Ioc 0 (f p_fst)
    · have h' : (p_fst, p_snd) ∈ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h
      rw [Set.indicator_of_mem h', Set.indicator_of_mem h]
    · have h' : (p_fst, p_snd) ∉ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h
      rw [Set.indicator_of_notMem h', Set.indicator_of_notMem 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)
aux₂ :
  Eq.{u_1 + 1} (α := α × ℝ → ℝ≥0∞)
    (Function.uncurry fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2))
⊢ MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)}

Tactic:
simpa only [mem_univ, Pi.zero_apply, true_and] using
      measurableSet_region_between_oc measurable_zero f_mble MeasurableSet.univ

Premises used: Pi.zero_apply, measurableSet_region_between_oc, measurable_zero, Set.mem_univ, true_and, MeasurableSet.univ
-- 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)
aux₂ :
  Eq.{u_1 + 1} (α := α × ℝ → ℝ≥0∞)
    (Function.uncurry fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2))
⊢ MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)}

Tactic:
have mble₀ : MeasurableSet {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := by
    simpa only [mem_univ, Pi.zero_apply, true_and] using
      measurableSet_region_between_oc measurable_zero f_mble MeasurableSet.univ
-- 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)
aux₂ :
  Eq.{u_1 + 1} (α := α × ℝ → ℝ≥0∞)
    (Function.uncurry fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2))
mble₀ : MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)}
⊢ AEMeasurable (α := α × ℝ) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (μ.prod volume)

Tactic:
(ENNReal.measurable_ofReal.comp (g_mble.comp measurable_snd)).aemeasurable.indicator₀
    mble₀.nullMeasurableSet

Premises used: ENNReal.ofNNReal, Measurable.aemeasurable, Measurable.comp, ENNReal.ofReal, MeasurableSet.nullMeasurableSet, WithTop.some, AEMeasurable.indicator₀, measurable_snd, ENNReal.measurable_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
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  Eq.{u_1 + 1} (α := α × ℝ → ℝ≥0∞)
    (Function.uncurry fun (x : α) (y : ℝ) ↦ (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) y)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2))
mble₀ : MeasurableSet.{u_1} (α := α × ℝ) {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)}
⊢ AEMeasurable (α := α × ℝ) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (μ.prod volume)

Tactic:
exact (ENNReal.measurable_ofReal.comp (g_mble.comp measurable_snd)).aemeasurable.indicator₀
    mble₀.nullMeasurableSet

Premises used: Measurable.aemeasurable, Measurable.comp, MeasurableSet.nullMeasurableSet, AEMeasurable.indicator₀, measurable_snd, ENNReal.measurable_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
⊢ ∀ (ω : α), 0 ≤ f ω

Tactic:
have f_nonneg : ∀ ω, 0 ≤ f ω := fun ω ↦ f_nn ω
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
pos :
  ∀ (H1 : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0),
    ∫⁻ (ω : α), 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))
neg :
  ∀ (H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0),
    ∫⁻ (ω : α), 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))
⊢ ∫⁻ (ω : α), 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:
by_cases H1 : g =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0

Premises used: Set.Ioi, 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 ≤ 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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
ω : α
simp_rw :
  Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (t : ℝ) ↦ g t)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (t : ℝ) ↦ 0)
⊢ Eq (α := ℝ) (∫ (t : ℝ) in 0..f ω, g t) (∫ (t : ℝ) in 0..f ω, 0)

Tactic:
simp_rw [intervalIntegral.integral_of_le (f_nonneg ω)]

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
ω : α
h : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] fun (a : ℝ) ↦ 0
⊢ Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (t : ℝ) ↦ g t)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 (f ω))) fun (t : ℝ) ↦ 0)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
ω : α
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] fun (a : ℝ) ↦ 0

Tactic:
ae_restrict_of_ae_restrict_of_subset Ioc_subset_Ioi_self H1

Premises used: Filter.EventuallyEq, Set.Ioc_subset_Ioi_self, MeasureTheory.ae_restrict_of_ae_restrict_of_subset
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
ω : α
⊢ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] fun (a : ℝ) ↦ 0

Tactic:
exact ae_restrict_of_ae_restrict_of_subset Ioc_subset_Ioi_self H1

Premises used: Set.Ioc_subset_Ioi_self, MeasureTheory.ae_restrict_of_ae_restrict_of_subset
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
⊢ ∀ (ω : α), Eq (α := ℝ) (∫ (t : ℝ) in 0..f ω, g t) (∫ (t : ℝ) in 0..f ω, 0)

Tactic:
have : ∀ ω, ∫ t in 0..f ω, g t = ∫ t in 0..f ω, 0 := by
        intro ω
        simp_rw [intervalIntegral.integral_of_le (f_nonneg ω)]
        apply integral_congr_ae
        exact ae_restrict_of_ae_restrict_of_subset Ioc_subset_Ioi_self H1
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
this : ∀ (ω : α), Eq (α := ℝ) (∫ (t : ℝ) in 0..f ω, g t) (∫ (t : ℝ) in 0..f ω, 0)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0

Tactic:
have A : ∫⁻ ω, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ = 0 := by
      have : ∀ ω, ∫ t in 0..f ω, g t = ∫ t in 0..f ω, 0 := by
        intro ω
        simp_rw [intervalIntegral.integral_of_le (f_nonneg ω)]
        apply integral_congr_ae
        exact ae_restrict_of_ae_restrict_of_subset Ioc_subset_Ioi_self H1
      simp [this]
-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
t : ℝ
ht : g t = 0 t
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) = 0 t

Tactic:
simp [ht]