-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem tendsto_setIntegral_of_monotone
    {ι : Type*} [Preorder ι] [(atTop : Filter ι).IsCountablyGenerated]
    {s : ι → Set X} (hsm : ∀ i, MeasurableSet (s i)) (h_mono : Monotone s)
    (hfi : IntegrableOn f (⋃ n, s n) μ) :
    Tendsto (fun i => ∫ x in s i, f x ∂μ) atTop (𝓝 (∫ x in ⋃ n, s n, f x ∂μ))

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, ↑‖f x‖₊ ∂μ < ⊤
hSm : MeasurableSet S
hsub : ∀ {i : ι}, s i ⊆ S
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Tactic:
rw [← withDensity_apply _ hSm] at hfi'

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : (μ.withDensity fun x => ↑‖f x‖₊) S < ⊤
hSm : MeasurableSet S
hsub : ∀ {i : ι}, s i ⊆ S
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : (μ.withDensity fun x => ↑‖f x‖₊) S < ⊤
hSm : MeasurableSet S
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun x => ‖f x‖ₑ
hν : ν = μ.withDensity fun x => ‖f x‖ₑ
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ε

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

Result:
case intro
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : (μ.withDensity fun x => ↑‖f x‖₊) S < ⊤
hSm : MeasurableSet S
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun x => ‖f x‖ₑ
hν : ν = μ.withDensity fun x => ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < ↑ε
⊢ ∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hfi : IntegrableOn f (⋃ n, s n) μ
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))

Tactic:
have hfi' : ∫⁻ x in ⋃ n, s n, ‖f x‖₊ ∂μ < ∞ := hfi.2

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hfi : IntegrableOn f (⋃ n, s n) μ
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
hfi' : ∫⁻ (x : X) in ⋃ n, s n, ↑‖f x‖₊ ∂μ < ⊤
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, ↑‖f x‖₊ ∂μ < ⊤
hSm : MeasurableSet S
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Tactic:
have hsub {i} : s i ⊆ S := subset_iUnion s i

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, ↑‖f x‖₊ ∂μ < ⊤
hSm : MeasurableSet S
hsub : ∀ {i : ι}, s i ⊆ S
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hfi : IntegrableOn f (⋃ n, s n) μ
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
hfi' : ∫⁻ (x : X) in ⋃ n, s n, ↑‖f x‖₊ ∂μ < ⊤
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))

Tactic:
set S := ⋃ i, s i

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, ↑‖f x‖₊ ∂μ < ⊤
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Proof state:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hne : atTop.NeBot
this✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : (μ.withDensity fun x => ↑‖f x‖₊) S < ⊤
hSm : MeasurableSet S
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun x => ‖f x‖ₑ
hν : ν = μ.withDensity fun x => ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < ↑ε
this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
i : ι
hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
⊢ ∫ (x : X) in s i, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε

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

Result:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_mono : Monotone s
hne : atTop.NeBot
this✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : (μ.withDensity fun x => ↑‖f x‖₊) S < ⊤
hSm : MeasurableSet S
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun x => ‖f x‖ₑ
hν : ν = μ.withDensity fun x => ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < ↑ε
this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
i : ι
hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
⊢ ↑‖∫ (x : X) in S \ s i, f x ∂μ‖₊ ≤ ↑ε