-- 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‖₊ ∂μ < ⊤
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Tactic:
have hSm : MeasurableSet S := MeasurableSet.iUnion_of_monotone h_mono hsm

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
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Proof state:
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 < ↑ε
this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
⊢ ∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε

Tactic:
filter_upwards [this] with i hi

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 i, 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
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‖ₑ
⊢ Tendsto (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 => ?_

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
ν : 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 ∂μ) ε

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 + ↑ε)
⊢ ν S - ν (s i) ≤ ↑ε

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 + ↑ε)
⊢ ν (s i) ≠ ⊤

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]

Result:
no goals