awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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
hfi : IntegrableOn f (⋃ (n : ι), s n) μ
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ))
have hfi' : ∫⁻ (x : X) in ⋃ (n : ι), s n, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
Tactic: have hfi' : ∫⁻ x in ⋃ n, s n, ‖f x‖₊ ∂μ < ∞ := hfi.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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
hfi : IntegrableOn f (⋃ (n : ι), s n) μ
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
hfi' : ∫⁻ (x : X) in ⋃ (n : ι), s n, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ))
have set : let S : Set X := ⋃ (i : ι), s i;
∀ (hfi : IntegrableOn f S μ) (hfi' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞),
  Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
Tactic: set S := ⋃ i, s i
Cleared hypotheses: hfi, hfi'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
have hSm : NullMeasurableSet S μ
Tactic: have hSm : NullMeasurableSet S μ := MeasurableSet.iUnion_of_monotone h_mono hsm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
hSm : NullMeasurableSet S μ
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
have hsub : ∀ {i : ι}, s i ⊆ S
Tactic: have hsub {i} : s i ⊆ S := subset_iUnion s i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
have hfi'₁ : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← withDensity_apply₀ _ hSm] at hfi'
Cleared hypotheses: hfi', hSm, hsub
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
have hν : let ν := μ.withDensity fun (x : X) ↦ ‖f x‖ₑ;
ν = μ.withDensity fun (x : X) ↦ ‖f x‖ₑ
Tactic: set ν := μ.withDensity (‖f ·‖ₑ) with hν
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ))
have 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 ∂μ)
Tactic: refine Metric.nhds_basis_closedBall.tendsto_right_iff.2 fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 < ε
⊢ ∀ᶠ (x : ι) in atTop,
    Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) ε) (∫ (x : X) in s x, f x ∂μ)
have 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 ∂μ)
Tactic: lift ε to ℝ≥0 using ε0.le
Cleared hypotheses: ε, ε0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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 < (↑ε : ℝ)
⊢ ∀ᶠ (x : ι) in atTop,
    Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) (↑ε : ℝ)) (∫ (x : X) in s x, f x ∂μ)
have 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∞)
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')
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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∞)
⊢ ∀ᶠ (x : ι) in atTop,
    Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) (↑ε : ℝ)) (∫ (x : X) in s x, f x ∂μ)
have 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 ∂μ)
Tactic: filter_upwards [this] with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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∞)
⊢ Membership.mem (γ := Set E) (Metric.closedBall (∫ (x : X) in S, f x ∂μ) (↑ε : ℝ)) (∫ (x : X) in s i, f x ∂μ)
have h : (↑(nnnorm.{u_3} (E := E) (∫ (x : X) in S \ s i, f x ∂μ)) : ℝ≥0∞) ≤ (↑ε : ℝ≥0∞)
Tactic: rw [mem_closedBall_iff_norm', ← setIntegral_diff₀ (hsm i) hfi hsub, ← coe_nnnorm,
    NNReal.coe_le_coe, ← ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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∞)
have h : ∫⁻ (a : X) in S \ s i, ‖f a‖ₑ ∂μ ≤ (↑ε : ℝ≥0∞)
Tactic: refine (enorm_integral_le_lintegral_enorm _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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∞)
⊢ ∫⁻ (a : X) in S \ s i, ‖f a‖ₑ ∂μ ≤ (↑ε : ℝ≥0∞)
have hsm' : NullMeasurableSet (s i) ν
Tactic: have hsm' : NullMeasurableSet (s i) ν := (hsm i).mono_ac (withDensity_absolutelyContinuous ..)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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) ν
⊢ ∫⁻ (a : X) in S \ s i, ‖f a‖ₑ ∂μ ≤ (↑ε : ℝ≥0∞)
have h : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) ≤
  (↑ε : ℝ≥0∞)
Tactic: rw [← withDensity_apply₀ _ (hSm.diff (hsm _)), ← hν, measure_diff hsub hsm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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∞)
⊢ ∫⁻ (a : X) in S \ s i, ‖f a‖ₑ ∂μ ≤ (↑ε : ℝ≥0∞)
have h₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← withDensity_apply₀ _ (hSm.diff (hsm _)), ← hν, measure_diff hsub hsm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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 ∂μ))
have hne : NeBot.{u_5} (α := ι) atTop
Tactic: refine .of_neBot_imp fun hne ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))
have this : IsDirectedOrder ι
Tactic: have := (atTop_neBot_iff.mp hne).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ι
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))
have 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 ∂μ))
Tactic: rcases hfi with ⟨i₀, hi₀⟩
Cleared hypotheses: hfi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ))
have h : ∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ =
  HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)
Tactic: convert! this.congr' <| (eventually_ge_atTop i₀).mono fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)))
h :
  ∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ =
    HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, 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 ∂μ))
have convert_2 : ∀ (i : ι) (hi : i₀ ≤ i),
  HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s i, f x ∂μ) = ∫ (x : X) in s i, f x ∂μ
Tactic: convert! this.congr' <| (eventually_ge_atTop i₀).mono fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)))
⊢ ∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ =
    HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)
have rw : MeasurableSet.{u_1} (α := X) (⋂ (i : ι), s i)
Tactic: rw [← diff_iInter, setIntegral_diff _ hi₀ (iInter_subset _ _), sub_sub_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)))
i : ι
hi : i₀ ≤ i
⊢ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s i, f x ∂μ) = ∫ (x : X) in s i, f x ∂μ
have convert_2 : ∫ (x : X) in s i₀, f x ∂μ - HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i, f x ∂μ) =
  ∫ (x : X) in s i, f x ∂μ
Tactic: rw [setIntegral_diff (hsm i) hi₀ (h_anti hi), sub_sub_cancel]