awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ

Tactic:
have : Antitone fun n ↦ ∫⁻ x, f n x ∂μ := fun i j hij ↦
    lintegral_mono_ae (h_anti.mono fun x hx ↦ hx hij)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨅ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (⨅ (n : ℕ), ∫⁻ (x : α), f n x ∂μ))
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
rw [key]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨅ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (⨅ (n : ℕ), ∫⁻ (x : α), f n x ∂μ))

Tactic:
tendsto_atTop_iInf this

Premises used: tendsto_atTop_iInf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨅ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (⨅ (n : ℕ), ∫⁻ (x : α), f n x ∂μ))

Tactic:
exact tendsto_atTop_iInf this

Premises used: tendsto_atTop_iInf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
suffices : ∫⁻ (x : α), F x ∂μ = ⨅ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
suffices key : ∫⁻ x, F x ∂μ = ⨅ n, ∫⁻ x, f n x ∂μ by
    rw [key]
    exact tendsto_atTop_iInf this
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
rw : ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ⨅ (n : ℕ), ∫⁻ (x : α), f n x ∂μ

Tactic:
rw [← lintegral_iInf' hf h_anti h0]

Premises used: MeasureTheory.lintegral_iInf'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
refine : F =ᶠ[ae μ] fun (a : α) ↦ ⨅ (n : ℕ), f n a
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
a : α
hx_anti : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n a
hx_tendsto : Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 (F a))
⊢ F a = ⨅ (n : ℕ), f n a

Tactic:
tendsto_nhds_unique hx_tendsto (tendsto_atTop_iInf hx_anti)

Premises used: tendsto_atTop_iInf, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))) x} x →
                Membership.mem (γ := Set α)
                  {x : α | (fun (x : α) ↦ F x = (fun (a : α) ↦ (⨅ (n : ℕ), f n a : ℝ≥0∞)) x) x} x}
            x}
      a
h₁ h₂ :
  ∀ (a : α) (hx_anti : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n a)
    (hx_tendsto : Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 (F a))), F a = ⨅ (n : ℕ), f n a
⊢ F =ᶠ[ae μ] fun (a : α) ↦ ⨅ (n : ℕ), f n a

Tactic:
filter_upwards [h_anti, h_tendsto] with _ hx_anti hx_tendsto
    using tendsto_nhds_unique hx_tendsto (tendsto_atTop_iInf hx_anti)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
pos :
  ∀ (hf₀ : ∫⁻ (a : α), f a ∂μ = 0),
    ∃ (s : Set α),
      MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
neg :
  ∀ (hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0),
    ∃ (s : Set α),
      MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
⊢ ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Tactic:
by_cases hf₀ : ∫⁻ a, f a ∂μ = 0
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : 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]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Tactic:
exact ⟨∅, .empty, by simp, by simpa [hf₀, pos_iff_ne_zero]⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ (g : α →ₛ ℝ≥0∞) (_ : (⇑g : (a : α) → ℝ≥0∞) ≤ f), ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ

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

Premises used: MeasureTheory.lintegral_def, ENNReal.sub_lt_self, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
obtain :
  ∀ (g : α →ₛ ℝ≥0∞) (hgf : (⇑g : (a : α) → ℝ≥0∞) ≤ f) (hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ),
    ∃ g ≤ f,
      Measurable g ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
          ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∃ g ≤ f,
    Measurable g ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∫⁻ (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ε
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : (⇑g : (a : α) → ℝ≥0∞) ≤ f
hgε rwa rwa₁ rwa₂ rwa₃ : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), (g : (a : α) → ℝ≥0∞) a ∂μ

Tactic:
rwa [g.lintegral_eq_lintegral]

Premises used: MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : (⇑g : (a : α) → ℝ≥0∞) ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
refine : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support (M := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ g ≤ f,
    Measurable g ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ

Tactic:
refine ⟨g, hgf, g.measurable, ?_, by rwa [g.lintegral_eq_lintegral]⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : (⇑g : (a : α) → ℝ≥0∞) ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support (M := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞)) : ℝ≥0∞) (∞ : ℝ≥0∞)

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

Premises used: MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top, Set.Mem, Filter.Eventually, setOf, MeasureTheory.SimpleFunc.FinMeasSupp, Eq.rec, Filter.EventuallyEq, ne_top_of_le_ne_top, MeasureTheory.lintegral_mono, Function.support, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : (⇑g : (a : α) → ℝ≥0∞) ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support (M := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞)) : ℝ≥0∞) (∞ : ℝ≥0∞)

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

Premises used: MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top, ne_top_of_le_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
neg :
  ∀ (g : α → ℝ≥0∞) (hgf : g ≤ f) (hg_meas : Measurable g)
    (hgsupp : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ),
    ∃ (s : Set α),
      MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
⊢ ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (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
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : 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 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

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

Premises used: measurableSet_support, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : 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 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
neg : ∫⁻ (a : α) in (support g)ᶜ, f a ∂μ < ε
⊢ ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε

Tactic:
refine ⟨_, measurableSet_support hg_meas, hgsupp, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : 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 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
x : α
⊢ x ∈ (support g)ᶜ → f x = (fun (a : α) ↦ f a - g a) x

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : 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 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α) in (support g)ᶜ, f a - g a ∂μ ≤ ∫⁻ (a : α), f a - g a ∂μ

Tactic:
setLIntegral_le_lintegral _ _

Premises used: MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : 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 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ

Tactic:
lintegral_sub hg_meas (ne_top_of_le_ne_top hf <| lintegral_mono hgf) (ae_of_all _ hgf)

Premises used: ne_top_of_le_ne_top, MeasureTheory.lintegral_mono, MeasureTheory.ae_of_all, MeasureTheory.lintegral_sub
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : 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 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ < ε

Tactic:
ENNReal.sub_lt_of_lt_add (lintegral_mono hgf) <|
      ENNReal.lt_add_of_sub_lt_left (.inl hf) hgε

Premises used: ENNReal.lt_add_of_sub_lt_left, MeasureTheory.lintegral_mono, ENNReal.sub_lt_of_lt_add, Or.inl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : 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 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞)
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 <| 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ε

Premises used: ENNReal.lt_add_of_sub_lt_left, measurableSet_support, MeasureTheory.setLIntegral_congr_fun, MeasurableSet.compl, ne_top_of_le_ne_top, MeasureTheory.lintegral_mono, MeasureTheory.ae_of_all, Function.support, ENNReal.sub_lt_of_lt_add, MeasureTheory.lintegral_sub, Or.inl, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
obtain :
  ∀ (g : α → ℝ≥0∞) (hmg : Measurable g) (hgf : g ≤ f) (hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ),
    ∃ (g : α → ℝ≥0∞),
      Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞),
    Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
obtain ⟨g, hmg, hgf, hifg⟩ := exists_measurable_le_lintegral_eq (μ := μ) f

Premises used: MeasureTheory.exists_measurable_le_lintegral_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
right : ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞),
    Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
use g, hmg, hgf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
fun s hms ↦ le_antisymm ?_ (lintegral_mono hgf)

Premises used: le_antisymm, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
right : ∀ (s : Set α) (hms : MeasurableSet s), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
⊢ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
refine fun s hms ↦ le_antisymm ?_ (lintegral_mono hgf)

Premises used: le_antisymm, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
right : ∫⁻ (a : α), g a ∂μ - ∫⁻ (x : α) in sᶜ, f x ∂μ ≤ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α) in sᶜ, g x ∂μ
right₁ : ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞
right₂ : ∫⁻ (x : α) in sᶜ, f x ∂μ ≠ ∞
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
rw [← compl_compl s, setLIntegral_compl hms.compl, setLIntegral_compl hms.compl, hifg]

Premises used: compl_compl, MeasureTheory.setLIntegral_compl, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
right : ∀ (x : α), g x ≤ f x
⊢ ∫⁻ (a : α), g a ∂μ - ∫⁻ (x : α) in sᶜ, f x ∂μ ≤ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α) in sᶜ, g x ∂μ

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
x : α
⊢ g x ≤ f x

Tactic:
apply hgf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
right :
  ∀ (hf : ∫⁻ (a : α), g a ∂μ ≠ ∞) (hmg : Measurable g) (hgf : g ≤ f) (hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ)
    (s : Set α) (hms : MeasurableSet s), ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞
⊢ ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞

Tactic:
rw [hifg] at hf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : ∫⁻ (a : α), g a ∂μ ≠ ∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞

Tactic:
ne_top_of_le_ne_top hf (setLIntegral_le_lintegral _ _)

Premises used: ne_top_of_le_ne_top, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : ∫⁻ (a : α), g a ∂μ ≠ ∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞

Tactic:
exact ne_top_of_le_ne_top hf (setLIntegral_le_lintegral _ _)

Premises used: ne_top_of_le_ne_top, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (x : α) in sᶜ, f x ∂μ ≠ ∞

Tactic:
ne_top_of_le_ne_top hf (setLIntegral_le_lintegral _ _)

Premises used: ne_top_of_le_ne_top, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (x : α) in sᶜ, f x ∂μ ≠ ∞

Tactic:
exact ne_top_of_le_ne_top hf (setLIntegral_le_lintegral _ _)

Premises used: ne_top_of_le_ne_top, MeasureTheory.setLIntegral_le_lintegral