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 : ℝ
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)

Tactic:
simp only [h_copy, h h', indicator_of_notMem, not_false_iff, mem_Ici, not_le, mul_zero]

Premises used: not_le, MulZeroClass.mul_zero, Set.mem_Ici, Set.indicator_of_notMem, not_false_iff
-- 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
h' : ¬0 < s
⊢ s ∉ Ioi 0

Tactic:
have : s ∉ Ioi (0 : ℝ) := 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_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
this : s ∉ Ioi 0
⊢ (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 [this, h', indicator_of_notMem, not_false_iff, mul_zero,
            zero_mul, mem_Ioc, false_and]

Premises used: MulZeroClass.zero_mul, false_and, MulZeroClass.mul_zero, Set.mem_Ioc, Set.indicator_of_notMem, not_false_iff
-- 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 : ℝ
⊢ 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]
-- 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 :
  ∫⁻ (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
⊢ ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun (t : ℝ) ↦ ENNReal.ofReal (g t)) s ∂μ =
    indicator (Ioi 0)
      (fun (t : ℝ) ↦ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) s

Tactic:
simp_rw [aux₁]
-- 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 : ℝ) ↦ 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
h₁ : ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) 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

Tactic:
rw [lintegral_const_mul']

Premises used: MeasureTheory.lintegral_const_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)
h : Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s ≠ ∞

Tactic:
apply ENNReal.mul_ne_top ENNReal.ofReal_ne_top

Premises used: ENNReal.mul_ne_top, ENNReal.ofReal_ne_top
-- 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)
pos : ∀ (h : 0 < s), Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞
neg : ∀ (h : ¬0 < s), Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞
⊢ Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞

Tactic:
by_cases h : (0 : ℝ) < s

Premises used: 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 : ℝ
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 : 0 < s
⊢ Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞

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
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 : ¬0 < s
⊢ Ne (α := ℝ≥0∞) (indicator (Ioi 0) (fun (x : ℝ) ↦ 1) s) ∞

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
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 :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) (indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a)
⊢ 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

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 : ℝ
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)
neg :
  ∀ (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)

Tactic:
by_cases h : s ≤ f 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 : ℝ
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 : α
h : s ≤ f a
⊢ Eq (α := ℝ≥0∞) ((Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) (indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a)

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
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 : α
h : ¬s ≤ f a
⊢ Eq (α := ℝ≥0∞) ((Ici s).indicator (fun (x : ℝ) ↦ 1) (f a)) (indicator {a : α | s ≤ f a} (fun (x : α) ↦ 1) a)

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
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 : α), 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
⊢ 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:
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]]
-- 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 : ℝ) ↦ 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
h₁ : NullMeasurableSet {a : α | s ≤ f a} μ
⊢ 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:
rw [lintegral_indicator₀]

Premises used: MeasureTheory.lintegral_indicator₀
-- 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)
⊢ NullMeasurableSet {a : α | s ≤ f a} μ

Tactic:
f_mble.nullMeasurable measurableSet_Ici

Premises used: Set.Mem, setOf, Measurable.nullMeasurable, Set.preimage, measurableSet_Ici
-- 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)
⊢ NullMeasurableSet {a : α | s ≤ f a} μ

Tactic:
exact f_mble.nullMeasurable measurableSet_Ici

Premises used: Measurable.nullMeasurable, measurableSet_Ici
-- 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)
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
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
⊢ 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
-- 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 : 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:
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
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 : ¬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:
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
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 : ℝ) ↦
          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)
⊢ 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_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]]

Premises used: mul_assoc, MeasureTheory.Measure.restrict_apply, Set.univ_inter, Set.indicator_mul_left, MeasurableSet.univ, MeasureTheory.lintegral_one