awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
⊢ let ν := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ;
  ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ

Tactic:
set ν := μ.withDensity (‖f ·‖ₑ) with hν

Premises used: MeasureTheory.Measure.withDensity, ENorm.enorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Tactic:
Metric.nhds_basis_closedBall.tendsto_right_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_right_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
refine :
  ∀ (ε : ℝ) (ε0 : 0 < ε),
    ∀ᶠ (x : ι) in atTop,
      Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) ε) (∫ (x : X) in s x, f x ∂μ)
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Tactic:
refine Metric.nhds_basis_closedBall.tendsto_right_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_right_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ
ε0 : 0 < ε
⊢ 0 ≤ ε

Tactic:
ε0.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ
ε0 : 0 < ε
lift :
  ∀ (ε : ℝ≥0) (ε0 : 0 < (↑ε : ℝ)),
    ∀ᶠ (x : ι) in atTop,
      Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) (↑ε : ℝ)) (∫ (x : X) in s x, f x ∂μ)
⊢ ∀ᶠ (x : ι) in atTop,
    Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) ε) (∫ (x : X) in s x, f x ∂μ)

Tactic:
lift ε to ℝ≥0 using ε0.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
⊢ ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
have : ∀ᶠ i in atTop, ν (s i) ∈ Icc (ν S - ε) (ν S + ε) :=
    tendsto_measure_iUnion_atTop h_mono (ENNReal.Icc_mem_nhds hfi'.ne (ENNReal.coe_pos.2 ε0).ne')
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
this :
  ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
h :
  ∀ (i : ι)
    (hi :
      Membership.mem (α := ℝ≥0∞)
        (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
          (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
        ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)),
    Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) (↑ε : ℝ)) (∫ (x : X) in s i, f x ∂μ)
⊢ ∀ᶠ (x : ι) in atTop,
    Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) (↑ε : ℝ)) (∫ (x : X) in s x, f x ∂μ)

Tactic:
filter_upwards [this] with i hi
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
this :
  ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi :
  Membership.mem (α := ℝ≥0∞)
    (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
    ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
h : (↑(nnnorm.{u_3} (E := E) (∫ (x : X) in S \ s i, f x ∂μ)) : ℝ≥0∞) ≤ (↑ε : ℝ≥0∞)
⊢ Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) (↑ε : ℝ)) (∫ (x : X) in s i, f x ∂μ)

Tactic:
rw [mem_closedBall_iff_norm', ← setIntegral_diff₀ (hsm i) hfi hsub, ← coe_nnnorm,
    NNReal.coe_le_coe, ← ENNReal.coe_le_coe]

Premises used: MeasureTheory.setIntegral_diff₀, mem_closedBall_iff_norm', ENNReal.coe_le_coe, coe_nnnorm, NNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
this :
  ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi :
  Membership.mem (α := ℝ≥0∞)
    (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
    ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ (↑(nnnorm.{u_3} (E := E) (∫ (x : X) in S \ s i, f x ∂μ)) : ℝ≥0∞) ≤ (↑ε : ℝ≥0∞)

Tactic:
(enorm_integral_le_lintegral_enorm _).trans ?_

Premises used: MeasureTheory.enorm_integral_le_lintegral_enorm, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
this :
  ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi :
  Membership.mem (α := ℝ≥0∞)
    (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
    ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
h : ∫⁻ (a : X) in S \ s i, ‖f a‖ₑ ∂μ ≤ (↑ε : ℝ≥0∞)
⊢ (↑(nnnorm.{u_3} (E := E) (∫ (x : X) in S \ s i, f x ∂μ)) : ℝ≥0∞) ≤ (↑ε : ℝ≥0∞)

Tactic:
refine (enorm_integral_le_lintegral_enorm _).trans ?_

Premises used: MeasureTheory.enorm_integral_le_lintegral_enorm, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
this :
  ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi :
  Membership.mem (α := ℝ≥0∞)
    (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
    ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ NullMeasurableSet (s i) ν

Tactic:
have hsm' : NullMeasurableSet (s i) ν := (hsm i).mono_ac (withDensity_absolutelyContinuous ..)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
this :
  ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi :
  Membership.mem (α := ℝ≥0∞)
    (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
    ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hsm' : NullMeasurableSet (s i) ν
h :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) ≤
    (↑ε : ℝ≥0∞)
h₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (a : X) in S \ s i, ‖f a‖ₑ ∂μ ≤ (↑ε : ℝ≥0∞)

Tactic:
rw [← withDensity_apply₀ _ (hSm.diff (hsm _)), ← hν, measure_diff hsub hsm']

Premises used: MeasureTheory.withDensity_apply₀, MeasureTheory.measure_diff, MeasureTheory.NullMeasurableSet.diff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
this :
  ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi :
  Membership.mem (α := ℝ≥0∞)
    (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
    ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hsm' : NullMeasurableSet (s i) ν
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) ≤
    (↑ε : ℝ≥0∞)

Tactic:
tsub_le_iff_tsub_le.mp hi.1

Premises used: And.left, Iff.mp, tsub_le_iff_tsub_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
this :
  ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi :
  Membership.mem (α := ℝ≥0∞)
    (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
    ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hsm' : NullMeasurableSet (s i) ν
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(hi.2.trans_lt <| ENNReal.add_lt_top.2 ⟨hfi', ENNReal.coe_lt_top⟩).ne

Premises used: Iff.mpr, And.right, And.intro, ENNReal.add_lt_top, LE.le.trans_lt, ENNReal.coe_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
this :
  ∀ᶠ (i : ι) in atTop,
    Membership.mem (α := ℝ≥0∞)
      (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
        (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
      ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
i : ι
hi :
  Membership.mem (α := ℝ≥0∞)
    (Icc (HSub.hSub (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞))
      (HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (↑ε : ℝ≥0∞)))
    ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hsm' : NullMeasurableSet (s i) ν
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) ≤
    (↑ε : ℝ≥0∞)

Tactic:
exacts [tsub_le_iff_tsub_le.mp hi.1,
    (hi.2.trans_lt <| ENNReal.add_lt_top.2 ⟨hfi', ENNReal.coe_lt_top⟩).ne]

Premises used: Iff.mpr, And.right, And.left, And.intro, Iff.mp, tsub_le_iff_tsub_le, ENNReal.add_lt_top, LE.le.trans_lt, ENNReal.coe_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hfi : IntegrableOn f (⋃ (n : ι), s n) μ
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ))

Tactic:
tendsto_setIntegral_of_monotone₀ (hsm · |>.nullMeasurableSet) h_mono hfi

Premises used: MeasureTheory.tendsto_setIntegral_of_monotone₀, MeasurableSet.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hfi : ∃ (i : ι), IntegrableOn f (s i) μ
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))

Tactic:
.of_neBot_imp fun hne ↦ ?_

Premises used: Filter.Tendsto.of_neBot_imp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hfi : ∃ (i : ι), IntegrableOn f (s i) μ
⊢ NeBot.{u_5} (α := ι) atTop

Tactic:
refine .of_neBot_imp fun hne ↦ ?_
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hfi : ∃ (i : ι), IntegrableOn f (s i) μ
hne : NeBot.{u_5} (α := ι) atTop
⊢ IsDirectedOrder ι

Tactic:
have := (atTop_neBot_iff.mp hne).2
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hfi : ∃ (i : ι), IntegrableOn f (s i) μ
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
rcases :
  ∀ (i₀ : ι) (hi₀ : IntegrableOn f (s i₀) μ),
    Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))

Tactic:
rcases hfi with ⟨i₀, hi₀⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))

Tactic:
this.congr' <| (eventually_ge_atTop i₀).mono fun i hi ↦ ?_

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop, Filter.Tendsto.congr'