-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem lintegral_comp_eq_lintegral_meas_le_mul_of_measurable (μ : 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, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t)

Proof state:
case intro.intro.intro
α : 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 (volume.restrict (Ioi 0))] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M_nonneg : 0 ≤ M
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
I : ∀ (n : ℕ), g =ᶠ[ae (volume.restrict (Ioc 0 (u n)))] 0
⊢ g =ᶠ[ae (volume.restrict (Ioo 0 M))] 0

Tactic:
have : g =ᵐ[volume.restrict (⋃ n, Ioc (0 : ℝ) (u n))] 0 := (ae_restrict_iUnion_iff _ _).2 I

Result:
case intro.intro.intro
α : 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 (volume.restrict (Ioi 0))] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M_nonneg : 0 ≤ M
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
I : ∀ (n : ℕ), g =ᶠ[ae (volume.restrict (Ioc 0 (u n)))] 0
this : g =ᶠ[ae (volume.restrict (⋃ n, Ioc 0 (u n)))] 0
⊢ g =ᶠ[ae (volume.restrict (Ioo 0 M))] 0

Proof state:
α : 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 (volume.restrict (Ioi 0))] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (volume.restrict (Ioc 0 M))] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
I : ν {a | f a ≤ M} = 0
H3 : ∫ (x : ℝ) in Ioc 0 (u n), g x ∂volume ≤ 0
g_nn_ae : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioc 0 (u n)), 0 ≤ g t
Ig : ∫ (t : ℝ) in Ioc 0 (u n), g t = 0
J : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioc 0 (u n)), g t = 0
this : u n ≤ M
⊢ False

Tactic:
exact lt_irrefl _ (this.trans_lt (uM n))

Result:
no goals

Proof state:
α : 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 (volume.restrict (Ioi 0))] 0
⊢ ∀ (ω : α), ∫ (t : ℝ) in 0 ..f ω, g t = ∫ (t : ℝ) in 0 ..f ω, 0

Tactic:
intro ω

Result:
α : 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 (volume.restrict (Ioi 0))] 0
ω : α
⊢ ∫ (t : ℝ) in 0 ..f ω, g t = ∫ (t : ℝ) in 0 ..f ω, 0

Proof state:
case neg
α : 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 (volume.restrict (Ioi 0))] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M_nonneg : 0 ≤ M
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
have hgM : g =ᵐ[volume.restrict (Ioc (0 : ℝ) M)] 0 := by
  rw [← restrict_Ioo_eq_restrict_Ioc]
  obtain ⟨u, -, uM, ulim⟩ : ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < M) ∧ Tendsto u atTop (𝓝 M) :=
    exists_seq_strictMono_tendsto M
  have I : ∀ n, g =ᵐ[volume.restrict (Ioc (0 : ℝ) (u n))] 0 := by
    intro n
    obtain ⟨s, hs, uns⟩ : ∃ s, g =ᶠ[ae (Measure.restrict volume (Ioc 0 s))] 0 ∧ u n < s :=
      exists_lt_of_lt_csSup (Set.nonempty_of_mem zero_mem) (uM n)
    exact ae_restrict_of_ae_restrict_of_subset (Ioc_subset_Ioc_right uns.le) hs
  have : g =ᵐ[volume.restrict (⋃ n, Ioc (0 : ℝ) (u n))] 0 := (ae_restrict_iUnion_iff _ _).2 I
  apply ae_restrict_of_ae_restrict_of_subset _ this
  rintro x ⟨x_pos, xM⟩
  obtain ⟨n, hn⟩ : ∃ n, x < u n := ((tendsto_order.1 ulim).1 _ xM).exists
  exact mem_iUnion.2 ⟨n, ⟨x_pos, hn.le⟩⟩

Result:
case neg
α : 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 (volume.restrict (Ioi 0))] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
M_bdd : BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M : ℝ := sSup {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
zero_mem : 0 ∈ {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
M_nonneg : 0 ≤ M
hgM : g =ᶠ[ae (volume.restrict (Ioc 0 M))] 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Proof state:
α : 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 ω
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
H1 : ¬BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
this : ∀ (n : ℕ), g =ᶠ[ae (volume.restrict (Ioc 0 ↑n))] 0
Hg : g =ᶠ[ae (volume.restrict (⋃ n, Ioc 0 ↑n))] 0
⊢ g =ᶠ[ae (volume.restrict (Ioi 0))] 0

Tactic:
have : (⋃ (n : ℕ), (Ioc (0 : ℝ) n)) = Ioi 0 :=
  iUnion_Ioc_eq_Ioi_self_iff.2 (fun x _ ↦ exists_nat_ge x)

Result:
α : 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 ω
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0 ..s, g t → μ {a | s < f a} ≠ ⊤
H1 : ¬BddAbove {s | g =ᶠ[ae (volume.restrict (Ioc 0 s))] 0}
this✝ : ∀ (n : ℕ), g =ᶠ[ae (volume.restrict (Ioc 0 ↑n))] 0
Hg : g =ᶠ[ae (volume.restrict (⋃ n, Ioc 0 ↑n))] 0
this : ⋃ n, Ioc 0 ↑n = Ioi 0
⊢ g =ᶠ[ae (volume.restrict (Ioi 0))] 0

Proof state:
α : 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 (volume.restrict (Ioi 0))] 0
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = 0
⊢ (fun t => μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =ᶠ[ae (volume.restrict (Ioi 0))] 0

Tactic:
filter_upwards [H1] with t ht using by simp [ht]

Result:
no goals