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 α
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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
⊢ ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have apply : ∀ (t : ℝ) (ht : t ∈ Ioi M),
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: apply setLIntegral_congr_fun measurableSet_Ioi (fun t 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
t : ℝ
ht : t ∈ Ioi M
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have rw : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | t ≤ f a} ∩ {a : α | M < f a}) : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: rw [Measure.restrict_apply (measurableSet_le measurable_const f_mble)]
-- 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
t : ℝ
ht : t ∈ Ioi M
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | t ≤ f a} ∩ {a : α | M < f a}) : ℝ≥0∞)
      (ENNReal.ofReal (g t))
have e_a : Eq.{u_1 + 1} (α := α → Prop) (fun (a : α) ↦ t ≤ f a) ({a : α | t ≤ f a} ∩ {a : α | M < f a})
Tactic: congr 3
-- 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have B2 : ∫⁻ (t : ℝ) in Ioi M, HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
  ∫⁻ (t : ℝ) in Ioi M, HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: have B2 : ∫⁻ t in Ioi M, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t)
              = ∫⁻ t in Ioi M, ν {a : α | t ≤ f a} * ENNReal.ofReal (g t) := by
      apply setLIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
      rw [Measure.restrict_apply (measurableSet_le measurable_const f_mble)]
      congr 3
      exact (inter_eq_left.2 (fun a ha ↦ (mem_Ioi.1 ht).trans_le ha)).symm
-- 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
B2 :
  ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have I : Ioi 0 = Ioc 0 M ∪ Ioi M
Tactic: have I : Ioi (0 : ℝ) = Ioc (0 : ℝ) M ∪ Ioi M := (Ioc_union_Ioi_eq_Ioi M_nonneg).symm
-- 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
B2 :
  ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
I : Ioi 0 = Ioc 0 M ∪ Ioi M
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have J : Disjoint (Ioc 0 M) (Ioi M)
Tactic: have J : Disjoint (Ioc 0 M) (Ioi M) := Ioc_disjoint_Ioi le_rfl
-- 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
B2 :
  ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
I : Ioi 0 = Ioc 0 M ∪ Ioi M
J : Disjoint (Ioc 0 M) (Ioi M)
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have rw : ∫⁻ (t : ℝ) in Ioc 0 M ∪ Ioi M,
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
  ∫⁻ (t : ℝ) in Ioc 0 M ∪ Ioi M,
    HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: rw [I, lintegral_union measurableSet_Ioi J, lintegral_union measurableSet_Ioi J, B1, B2]
-- 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
B2 :
  ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
I : Ioi 0 = Ioc 0 M ∪ Ioi M
J : Disjoint (Ioc 0 M) (Ioi M)
rw :
  ∫⁻ (t : ℝ) in Ioc 0 M ∪ Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioc 0 M ∪ Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have rw₁ : ∫⁻ (a : ℝ) in Ioc 0 M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a ≤ f a_1} : ℝ≥0∞) (ENNReal.ofReal (g a)) ∂volume +
    ∫⁻ (a : ℝ) in Ioi M,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a ≤ f a_1} : ℝ≥0∞) (ENNReal.ofReal (g a)) ∂volume =
  ∫⁻ (t : ℝ) in Ioc 0 M ∪ Ioi M,
    HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: rw [I, lintegral_union measurableSet_Ioi J, lintegral_union measurableSet_Ioi J, B1, B2]
-- 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, 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 B : ∫⁻ (t : ℝ) in Ioi 0, HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
  ∫⁻ (t : ℝ) in Ioi 0, HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: have B : ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t)
           = ∫⁻ t in Ioi 0, ν {a : α | t ≤ f a} * ENNReal.ofReal (g t) := by
    have B1 : ∫⁻ t in Ioc 0 M, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t)
         = ∫⁻ t in Ioc 0 M, ν {a : α | t ≤ f a} * ENNReal.ofReal (g t) := by
      apply lintegral_congr_ae
      filter_upwards [hgM] with t ht
      simp [ht]
    have B2 : ∫⁻ t in Ioi M, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t)
              = ∫⁻ t in Ioi M, ν {a : α | t ≤ f a} * ENNReal.ofReal (g t) := by
      apply setLIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
      rw [Measure.restrict_apply (measurableSet_le measurable_const f_mble)]
      congr 3
      exact (inter_eq_left.2 (fun a ha ↦ (mem_Ioi.1 ht).trans_le ha)).symm
    have I : Ioi (0 : ℝ) = Ioc (0 : ℝ) M ∪ Ioi M := (Ioc_union_Ioi_eq_Ioi M_nonneg).symm
    have J : Disjoint (Ioc 0 M) (Ioi M) := Ioc_disjoint_Ioi le_rfl
    rw [I, lintegral_union measurableSet_Ioi J, lintegral_union measurableSet_Ioi J, B1, B2]
-- 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
H2 :
  ∀ (s : ℝ) (_ : s > 0) (_ : LT.lt (α := ℝ) 0 (∫ (t : ℝ) in 0..s, g t)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | s < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
M_bdd : BddAbove (α := ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
M : ℝ := sSup {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0}
zero_mem : Membership.mem (γ := Set ℝ) {s : ℝ | g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 s))] 0} 0
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a : α | M < f a}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
have neg : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν =
  ∫⁻ (t : ℝ) in Ioi 0, HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))
Tactic: rw [A, B]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ ∃ (G : ℝ → ℝ), Measurable G ∧ 0 ≤ G ∧ g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
have refine : AEMeasurable (_m := Real.measurableSpace) g (Measure.restrict volume (Ioi 0))
Tactic: refine AEMeasurable.exists_measurable_nonneg ?_ g_nn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 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 obtain : ∀ (G : ℝ → ℝ) (G_mble : Measurable G) (G_nn : 0 ≤ G)
  (g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G),
  ∫⁻ (ω : α), 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: obtain ⟨G, G_mble, G_nn, g_eq_G⟩ : ∃ G : ℝ → ℝ, Measurable G ∧ 0 ≤ G
      ∧ g =ᵐ[volume.restrict (Ioi 0)] G := by
    refine AEMeasurable.exists_measurable_nonneg ?_ g_nn
    exact aemeasurable_Ioi_of_forall_Ioc fun t ht => (g_intble t ht).1.1.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] G
⊢ ∫⁻ (ω : α), 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 g_eq_G_on : ∀ (t : ℝ), g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 t))] G
Tactic: have g_eq_G_on : ∀ t, g =ᵐ[volume.restrict (Ioc 0 t)] G := fun t =>
    ae_mono (Measure.restrict_mono Ioc_subset_Ioi_self le_rfl) g_eq_G