awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
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)
have this : s ∉ Ioi 0
Tactic: have : s ∉ Ioi (0 : ℝ) := 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)
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
have 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)
Tactic: have aux₁ :
      (fun x => (Ioc 0 (f x)).indicator (fun t : ℝ => ENNReal.ofReal (g t)) s) = fun x =>
        ENNReal.ofReal (g s) * (Ioi (0 : ℝ)).indicator (fun _ => 1) s *
          (Ici s).indicator (fun _ : ℝ => (1 : ℝ≥0∞)) (f x) := by
      funext a
      by_cases h : s ∈ Ioc (0 : ℝ) (f a)
      · simp only [h, show s ∈ Ioi (0 : ℝ) from h.1, show f a ∈ Ici s from h.2, indicator_of_mem,
          mul_one]
      · have h_copy := h
        simp only [mem_Ioc, not_and, not_le] at h
        by_cases h' : 0 < s
        · simp only [h_copy, h h', indicator_of_notMem, not_false_iff, mem_Ici, not_le, mul_zero]
        · have : s ∉ Ioi (0 : ℝ) := h'
          simp only [this, h', indicator_of_notMem, not_false_iff, mul_zero,
            zero_mul, mem_Ioc, false_and]
-- 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 : ℝ
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)
⊢ ∫⁻ (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
have h : ∫⁻ (x : α),
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f x) ∂μ =
  indicator (Ioi 0)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
Tactic: simp_rw [aux₁]
-- 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 : ℝ
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)
⊢ ∫⁻ (x : α),
      ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f x) ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
have h : ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s *
    ∫⁻ (a : α), (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a) ∂μ =
  indicator (Ioi 0)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
Tactic: rw [lintegral_const_mul']
-- 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 : ℝ
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 : ℝ) ↦ 1) s *
      ∫⁻ (a : α), (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a) ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
⊢ ∫⁻ (x : α),
      ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * (Ici s).indicator (fun (x : ℝ) ↦ 1) (f x) ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
have h₁ : ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s ≠ ∞
Tactic: rw [lintegral_const_mul']
-- 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 : ℝ
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 : ℝ) ↦ 1) s ≠ ∞
have h : Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞
Tactic: apply ENNReal.mul_ne_top ENNReal.ofReal_ne_top
-- 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 : ℝ
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)
⊢ Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞
have pos : ∀ (h : 0 < s), Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞
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 : ℝ
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)
pos : ∀ (h : 0 < s), Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞
⊢ Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞
have neg : ∀ (h : ¬0 < s), Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞
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 : ℝ
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)
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) fun (a : α) ↦
    indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a
have h : ∀ (a : α), Eq (α := ℝ≥0∞) ((Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) (indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) 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 : ℝ
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)
a : α
⊢ Eq (α := ℝ≥0∞) ((Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) (indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a)
have pos : ∀ (h : s ≤ f a),
  Eq (α := ℝ≥0∞) ((Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) (indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a)
Tactic: by_cases h : s ≤ 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 : ℝ
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)
a : α
pos :
  ∀ (h : s ≤ f a),
    Eq (α := ℝ≥0∞) ((Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) (indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a)
⊢ Eq (α := ℝ≥0∞) ((Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) (indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a)
have neg : ∀ (h : ¬s ≤ f a),
  Eq (α := ℝ≥0∞) ((Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) (indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a)
Tactic: by_cases h : s ≤ 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 : ℝ
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 : ℝ) ↦ 1) s *
      ∫⁻ (a : α), (Ici s).indicator (fun (x : ℝ) ↦ 1) (f a) ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
have h : ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s *
    ∫⁻ (a : α), indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a ∂μ =
  indicator (Ioi 0)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
Tactic: simp_rw [show
        (fun a => (Ici s).indicator (fun _ : ℝ => (1 : ℝ≥0∞)) (f a)) = fun a =>
          {a : α | s ≤ f a}.indicator (fun _ => 1) a
        by funext a; by_cases h : s ≤ f a <;> simp [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 : ℝ
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 : ℝ) ↦ 1) s *
      ∫⁻ (a : α), indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
have h : ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s * ∫⁻ (a : α) in {a : α | s ≤ f a}, 1 ∂μ =
  indicator (Ioi 0)
    (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
Tactic: rw [lintegral_indicator₀]
-- 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 : ℝ
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 : ℝ) ↦ 1) s * ∫⁻ (a : α) in {a : α | s ≤ f a}, 1 ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s *
      ∫⁻ (a : α), indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
have h₁ : NullMeasurableSet {a : α | s ≤ f a} μ
Tactic: rw [lintegral_indicator₀]
-- 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 : ℝ
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)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (indicator (Ioi 0) (fun (_x : ℝ) ↦ 1) s : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞) =
    indicator (Ioi 0)
      (fun (_x : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞))
      s
have pos : ∀ (h : 0 < s),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (indicator (Ioi 0) (fun (_x : ℝ) ↦ 1) s : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞) =
    indicator (Ioi 0)
      (fun (_x : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞))
      s
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 : ℝ
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)
pos :
  ∀ (h : 0 < s),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (indicator (Ioi 0) (fun (_x : ℝ) ↦ 1) s : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞) =
      indicator (Ioi 0)
        (fun (_x : ℝ) ↦
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞))
        s
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (indicator (Ioi 0) (fun (_x : ℝ) ↦ 1) s : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞) =
    indicator (Ioi 0)
      (fun (_x : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞))
      s
have neg : ∀ (h : ¬0 < s),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (indicator (Ioi 0) (fun (_x : ℝ) ↦ 1) s : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞) =
    indicator (Ioi 0)
      (fun (_x : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s ≤ f a} : ℝ≥0∞))
      s
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 : ℝ
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 : ℝ) ↦ 1) s * ∫⁻ (a : α) in {a : α | s ≤ f a}, 1 ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s
have h : 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: rw [lintegral_one, Measure.restrict_apply MeasurableSet.univ, univ_inter, indicator_mul_left,
      mul_assoc,
      show
        (Ioi 0).indicator (fun _x : ℝ => (1 : ℝ≥0∞)) s * μ {a : α | s ≤ f a} =
          (Ioi 0).indicator (fun _x : ℝ => 1 * μ {a : α | s ≤ f a}) s
        by by_cases h : 0 < s <;> simp [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 : ℝ
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 : ℝ) ↦
          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)
have 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
Tactic: simp_rw [mul_comm _ (ENNReal.ofReal _), one_mul]
-- 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.{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))
have 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)
Tactic: funext p