-- Module: Mathlib.MeasureTheory.Integral.Layercake
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))] 0
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))
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))
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 =
    ∫⁻ (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
rw₃ :
  (∫⁻ (t : ℝ) in Ioc 0 M,
        HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (ENNReal.ofReal (g t))) +
      ∫⁻ (a : ℝ) in Ioi M,
        HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a_1 : α | a ≤ f a_1} : ℝ≥0∞) (ENNReal.ofReal (g a)) ∂volume =
    ∫⁻ (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
rw₄ rw₅ :
  (∫⁻ (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)) =
    ∫⁻ (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 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:
rw [I, lintegral_union measurableSet_Ioi J, lintegral_union measurableSet_Ioi J, B1, B2]

Premises used: MeasureTheory.lintegral_union, measurableSet_Ioi