-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem _root_.Antitone.tendsto_setIntegral (hsm : ∀ i, MeasurableSet (s i)) (h_anti : Antitone s)
    (hfi : IntegrableOn f (s 0) μ) :
    Tendsto (fun i => ∫ a in s i, f a ∂μ) atTop (𝓝 (∫ a in ⋂ n, s n, f a ∂μ))

Proof state:
case refine_3
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖(s n).indicator f a‖ ≤ bound a

Tactic:
simp_rw [norm_indicator_eq_indicator_norm]

Result:
case refine_3
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, (s n).indicator (fun a => ‖f a‖) a ≤ bound a

Proof state:
case refine_1
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
⊢ AEStronglyMeasurable f (μ.restrict (s n))

Tactic:
exact (IntegrableOn.mono_set hfi (h_anti (zero_le n))).1

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
⊢ Tendsto (fun i => ∫ (a : α), (s i).indicator f a ∂μ) atTop (𝓝 (∫ (x : α), (⋂ b, s b).indicator f x ∂μ))

Tactic:
refine tendsto_integral_of_dominated_convergence bound ?_ ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ (n : ℕ), AEStronglyMeasurable ((s n).indicator f) μ

case refine_2
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
⊢ Integrable bound μ

case refine_3
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖(s n).indicator f a‖ ≤ bound a

case refine_4
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => (s n).indicator f a) atTop (𝓝 ((⋂ b, s b).indicator f a))

Proof state:
case refine_3
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
x : α
⊢ (s n).indicator (fun a => ‖f a‖) x ≤ bound x

Tactic:
exact indicator_le_indicator_of_subset (h_anti (zero_le n)) (fun a => norm_nonneg _) _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
⊢ Tendsto (fun i => ∫ (a : α), (s i).indicator f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ n, s n, f a ∂μ))

Tactic:
rw [← integral_indicator (MeasurableSet.iInter hsm)]

Result:
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a => ‖f a‖
h_int_eq : (fun i => ∫ (a : α) in s i, f a ∂μ) = fun i => ∫ (a : α), (s i).indicator f a ∂μ
⊢ Tendsto (fun i => ∫ (a : α), (s i).indicator f a ∂μ) atTop (𝓝 (∫ (x : α), (⋂ b, s b).indicator f x ∂μ))