awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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 : α × ℝ
⊢ 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)
have 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))
Tactic: cases p with | mk p_fst p_snd => ?_
Cleared hypotheses: p
-- 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)
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))
have 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))
Tactic: rw [Function.uncurry_apply_pair]
-- 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)
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))
have 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))
Tactic: by_cases h : p_snd ∈ Ioc 0 (f p_fst)
-- 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)
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))
⊢ 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))
have 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))
Tactic: by_cases h : p_snd ∈ Ioc 0 (f p_fst)
-- 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)
p_fst : α
p_snd : ℝ
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))
have h' : 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
-- 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)
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)
⊢ 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))
have pos : (Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd = ENNReal.ofReal (g (p_fst, p_snd).2)
Tactic: rw [Set.indicator_of_mem h', Set.indicator_of_mem 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)
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)
⊢ 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))
have pos₁ : ENNReal.ofReal (g p_snd) = ENNReal.ofReal (g (p_fst, p_snd).2)
Tactic: rw [Set.indicator_of_mem h', Set.indicator_of_mem 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
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)
⊢ 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))
have h' : (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
-- 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)
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)}
⊢ 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))
have neg : Eq (α := ℝ≥0∞) ((Ioc 0 (f p_fst)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) p_snd) 0
Tactic: rw [Set.indicator_of_notMem h', Set.indicator_of_notMem 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)
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
⊢ 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))
have neg₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [Set.indicator_of_notMem h', Set.indicator_of_notMem 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
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)
⊢ AEMeasurable (α := α × ℝ) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (Function.uncurry fun (a : α) ↦ (Ioc 0 (f a)).indicator fun (t : ℝ) ↦ ENNReal.ofReal (g t)) (μ.prod volume)
have 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))
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]
-- 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)
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))
⊢ AEMeasurable (α := α × ℝ) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (indicator {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)} fun (p : α × ℝ) ↦ ENNReal.ofReal (g p.2)) (μ.prod volume)
have mble₀ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
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
⊢ ∫⁻ (ω : α), 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 f_nonneg : ∀ (ω : α), 0 ≤ f ω
Tactic: have f_nonneg : ∀ ω, 0 ≤ f ω := fun ω ↦ f_nn ω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
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 ω
⊢ ∫⁻ (ω : α), 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 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))
Tactic: by_cases H1 : g =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
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))
⊢ ∫⁻ (ω : α), 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 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))
Tactic: by_cases H1 : g =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
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)
have 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)
Tactic: simp_rw [intervalIntegral.integral_of_le (f_nonneg ω)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
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 (α := ℝ) (@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)
have h : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 (f ω)))] fun (a : ℝ) ↦ 0
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
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
have this : ∀ (ω : α), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
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) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have A : ∫⁻ (ω : α), 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
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
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) 0
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = 0 x) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                Eq (α := ℝ≥0∞)
                  ((fun (t : ℝ) ↦
                      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)))
                    x)
                  (0 x))
              x}
          x}
    a
Tactic: filter_upwards [H1] with t ht using by simp [ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
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
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ g x = 0 x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  Eq (α := ℝ≥0∞)
                    ((fun (t : ℝ) ↦
                        HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞)
                          (ENNReal.ofReal (g t)))
                      x)
                    (0 x))
                x}
            x}
      a
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) 0
have h₁ : ∀ (a : ℝ),
  g a = 0 a → HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a_2 : α | a ≤ f a_2} : ℝ≥0∞) (ENNReal.ofReal (g a)) = 0 a
Tactic: filter_upwards [H1] with t ht using by simp [ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
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 : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    0
have this : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ≥0∞)
  (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) 0
Tactic: have : (fun t ↦ μ {a : α | t ≤ f a} * ENNReal.ofReal (g t))
        =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0 := by
          filter_upwards [H1] with t ht using by simp [ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
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
⊢ ∫⁻ (ω : α), 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 B : ∫⁻ (t : ℝ) in Ioi 0, HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
  0
Tactic: have B : ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) = 0 := by
      have : (fun t ↦ μ {a : α | t ≤ f a} * ENNReal.ofReal (g t))
        =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0 := by
          filter_upwards [H1] with t ht using by simp [ht]
      simp [lintegral_congr_ae this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
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
B :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    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))
have pos : 0 =
  ∫⁻ (t : ℝ) in Ioi 0, HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: rw [A, B]