-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem exists_setLintegral_compl_lt {f : α → ℝ≥0∞} (hf : ∫⁻ a, f a ∂μ ≠ ∞)
    {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ s : Set α, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ a in sᶜ, f a ∂μ < ε

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : μ (support g) < ⊤
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
a✝ : α
⊢ a✝ ∈ (support g)ᶜ → f a✝ = f a✝ - g a✝

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : μ (support g) < ⊤
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∀ a ∈ (support g)ᶜ, f a = f a - g a

Tactic:
intro

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : μ (support g) < ⊤
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
a✝ : α
⊢ a✝ ∈ (support g)ᶜ → f a✝ = f a✝ - g a✝

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ g ≤ f, Measurable g ∧ μ (support g) < ⊤ ∧ ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ

Tactic:
obtain ⟨g, hgf, hgε⟩ : ∃ (g : α →ₛ ℝ≥0∞) (_ : g ≤ f), ∫⁻ a, f a ∂μ - ε < g.lintegral μ := by
  simpa only [← lt_iSup_iff, ← lintegral_def] using ENNReal.sub_lt_self hf hf₀ hε

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : ⇑g ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ ∃ g ≤ f, Measurable g ∧ μ (support g) < ⊤ ∧ ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : ⇑g ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ μ (support ⇑g) < ⊤

Tactic:
exact SimpleFunc.FinMeasSupp.of_lintegral_ne_top <| ne_top_of_le_ne_top hf <|
  g.lintegral_eq_lintegral μ ▸ lintegral_mono hgf

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ g, ∃ (_ : ⇑g ≤ f), ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ

Tactic:
simpa only [← lt_iSup_iff, ← lintegral_def] using ENNReal.sub_lt_self hf hf₀ hε

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Tactic:
exact ⟨∅, .empty, by simp, by simpa [hf₀, pos_iff_ne_zero]⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Tactic:
obtain ⟨g, hgf, hg_meas, hgsupp, hgε⟩ :
    ∃ g ≤ f, Measurable g ∧ μ (support g) < ∞ ∧ ∫⁻ a, f a ∂μ - ε < ∫⁻ a, g a ∂μ := by
  obtain ⟨g, hgf, hgε⟩ : ∃ (g : α →ₛ ℝ≥0∞) (_ : g ≤ f), ∫⁻ a, f a ∂μ - ε < g.lintegral μ := by
    simpa only [← lt_iSup_iff, ← lintegral_def] using ENNReal.sub_lt_self hf hf₀ hε
  refine ⟨g, hgf, g.measurable, ?_, by rwa [g.lintegral_eq_lintegral]⟩
  exact SimpleFunc.FinMeasSupp.of_lintegral_ne_top <| ne_top_of_le_ne_top hf <|
    g.lintegral_eq_lintegral μ ▸ lintegral_mono hgf

Result:
case neg.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : μ (support g) < ⊤
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Proof state:
case neg.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : μ (support g) < ⊤
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α) in (support g)ᶜ, f a ∂μ < ε

Tactic:
calc
  ∫⁻ a in (support g)ᶜ, f a ∂μ
    = ∫⁻ a in (support g)ᶜ, f a - g a ∂μ := setLIntegral_congr_fun
    (measurableSet_support hg_meas).compl <| ae_of_all _ <| by intro; simp_all
  _ ≤ ∫⁻ a, f a - g a ∂μ := setLIntegral_le_lintegral _ _
  _ = ∫⁻ a, f a ∂μ - ∫⁻ a, g a ∂μ :=
    lintegral_sub hg_meas (ne_top_of_le_ne_top hf <| lintegral_mono hgf) (ae_of_all _ hgf)
  _ < ε := ENNReal.sub_lt_of_lt_add (lintegral_mono hgf) <|
    ENNReal.lt_add_of_sub_lt_left (.inl hf) hgε

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ ∫⁻ (a : α) in ∅ᶜ, f a ∂μ < ε

Tactic:
simpa [hf₀, pos_iff_ne_zero]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ μ ∅ < ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : ⇑g ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ

Tactic:
rwa [g.lintegral_eq_lintegral]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Tactic:
by_cases hf₀ : ∫⁻ a, f a ∂μ = 0

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : ⇑g ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ ∃ g ≤ f, Measurable g ∧ μ (support g) < ⊤ ∧ ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ

Tactic:
refine ⟨g, hgf, g.measurable, ?_, by rwa [g.lintegral_eq_lintegral]⟩

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : ⇑g ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ μ (support ⇑g) < ⊤

Proof state:
case neg.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : μ (support g) < ⊤
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Tactic:
refine ⟨_, measurableSet_support hg_meas, hgsupp, ?_⟩

Result:
case neg.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : μ (support g) < ⊤
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α) in (support g)ᶜ, f a ∂μ < ε