-- Mathlib/MeasureTheory/Integral/Layercake.lean
lemma Integrable.integral_eq_integral_Ioc_meas_le {f : α → ℝ} {M : ℝ}
    (f_intble : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) (f_bdd : f ≤ᵐ[μ] (fun _ ↦ M)) :
    ∫ ω, f ω ∂μ = ∫ t in Ioc 0 M, ENNReal.toReal (μ {a : α | t ≤ f a})

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
obs : μ {a | M < f a} = 0
⊢ μ {a | t ≤ f a} = 0 ∨ μ {a | t ≤ f a} = ⊤

Tactic:
exact Or.inl <| measure_mono_null (fun a ha ↦ lt_of_lt_of_le htM ha) obs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
obs : μ {a | M < f a} = 0
⊢ (μ {a | t ≤ f a}).toReal = 0

Tactic:
rw [ENNReal.toReal_eq_zero_iff]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
obs : μ {a | M < f a} = 0
⊢ μ {a | t ≤ f a} = 0 ∨ μ {a | t ≤ f a} = ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
⊢ M < t

Tactic:
simp_all only [mem_diff, mem_Ioi, mem_Ioc, not_and, not_le]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
⊢ (μ {a | t ≤ f a}).toReal = 0

Tactic:
have htM : M < t := by simp_all only [mem_diff, mem_Ioi, mem_Ioc, not_and, not_le]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ (μ {a | t ≤ f a}).toReal = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ ∀ᵐ (a : α) ∂μ, a ∉ {a | M < f a}

Tactic:
filter_upwards [f_bdd] with a ha using not_lt.mpr ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ μ {a | M < f a} = 0

Tactic:
rw [measure_zero_iff_ae_nmem]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ ∀ᵐ (a : α) ∂μ, a ∉ {a | M < f a}

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ (μ {a | t ≤ f a}).toReal = 0

Tactic:
have obs : μ {a | M < f a} = 0 := by
  rw [measure_zero_iff_ae_nmem]
  filter_upwards [f_bdd] with a ha using not_lt.mpr ha

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
obs : μ {a | M < f a} = 0
⊢ (μ {a | t ≤ f a}).toReal = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 \ Ioc 0 M → (μ {a | x ≤ f a}).toReal = 0

Tactic:
apply Eventually.of_forall (fun t ht ↦ ?_)

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
⊢ (μ {a | t ≤ f a}).toReal = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioc 0 M, (μ {a | t ≤ f a}).toReal

Tactic:
rw [f_intble.integral_eq_integral_meas_le f_nn]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
⊢ ∫ (t : ℝ) in Ioi 0, (μ {a | t ≤ f a}).toReal = ∫ (t : ℝ) in Ioc 0 M, (μ {a | t ≤ f a}).toReal

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
⊢ ∫ (t : ℝ) in Ioi 0, (μ {a | t ≤ f a}).toReal = ∫ (t : ℝ) in Ioc 0 M, (μ {a | t ≤ f a}).toReal

Tactic:
rw [setIntegral_eq_of_subset_of_ae_diff_eq_zero
    nullMeasurableSet_Ioi Ioc_subset_Ioi_self ?_]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun x => M
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 \ Ioc 0 M → (μ {a | x ≤ f a}).toReal = 0