-- Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean
theorem measure_of_cont_bdd_of_tendsto_indicator
    (μ : Measure Ω) [IsFiniteMeasure μ] {c : ℝ≥0} {E : Set Ω} (E_mble : MeasurableSet E)
    (fs : ℕ → Ω →ᵇ ℝ≥0) (fs_bdd : ∀ n ω, fs n ω ≤ c)
    (fs_lim : Tendsto (fun n ω ↦ fs n ω) atTop (𝓝 (indicator E fun _ ↦ (1 : ℝ≥0)))) :
    Tendsto (fun n ↦ lintegral μ fun ω ↦ fs n ω) atTop (𝓝 (μ E))

Proof state:
Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : Tendsto (fun n ω => (fs n) ω) atTop (𝓝 (E.indicator fun x => 1))
⊢ ∀ (ω : Ω), Tendsto (fun n => (fs n) ω) atTop (𝓝 (E.indicator (fun x => 1) ω))

Tactic:
rw [tendsto_pi_nhds] at fs_lim

Result:
Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : ∀ (x : Ω), Tendsto (fun i => (fs i) x) atTop (𝓝 (E.indicator (fun x => 1) x))
⊢ ∀ (ω : Ω), Tendsto (fun n => (fs n) ω) atTop (𝓝 (E.indicator (fun x => 1) ω))

Proof state:
Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : ∀ (x : Ω), Tendsto (fun i => (fs i) x) atTop (𝓝 (E.indicator (fun x => 1) x))
⊢ ∀ (ω : Ω), Tendsto (fun n => (fs n) ω) atTop (𝓝 (E.indicator (fun x => 1) ω))

Tactic:
exact fun ω ↦ fs_lim ω

Result:
no goals

Proof state:
Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : Tendsto (fun n ω => (fs n) ω) atTop (𝓝 (E.indicator fun x => 1))
fs_lim' : ∀ (ω : Ω), Tendsto (fun n => (fs n) ω) atTop (𝓝 (E.indicator (fun x => 1) ω))
⊢ Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) atTop (𝓝 (μ E))

Tactic:
apply measure_of_cont_bdd_of_tendsto_filter_indicator μ E_mble fs
  (Eventually.of_forall fun n ↦ Eventually.of_forall (fs_bdd n)) (Eventually.of_forall fs_lim')

Result:
no goals

Proof state:
Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : Tendsto (fun n ω => (fs n) ω) atTop (𝓝 (E.indicator fun x => 1))
⊢ Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) atTop (𝓝 (μ E))

Tactic:
have fs_lim' :
  ∀ ω, Tendsto (fun n : ℕ ↦ (fs n ω : ℝ≥0)) atTop (𝓝 (indicator E (fun _ ↦ (1 : ℝ≥0)) ω)) := by
  rw [tendsto_pi_nhds] at fs_lim
  exact fun ω ↦ fs_lim ω

Result:
Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : Tendsto (fun n ω => (fs n) ω) atTop (𝓝 (E.indicator fun x => 1))
fs_lim' : ∀ (ω : Ω), Tendsto (fun n => (fs n) ω) atTop (𝓝 (E.indicator (fun x => 1) ω))
⊢ Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) atTop (𝓝 (μ E))