-- Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean
theorem measure_of_cont_bdd_of_tendsto_filter_indicator {ι : Type*} {L : Filter ι}
    [L.IsCountablyGenerated] (μ : Measure Ω)
    [IsFiniteMeasure μ] {c : ℝ≥0} {E : Set Ω} (E_mble : MeasurableSet E) (fs : ι → Ω →ᵇ ℝ≥0)
    (fs_bdd : ∀ᶠ i in L, ∀ᵐ ω : Ω ∂μ, fs i ω ≤ c)
    (fs_lim : ∀ᵐ ω ∂μ, Tendsto (fun i ↦ fs i ω) L (𝓝 (indicator E (fun _ ↦ (1 : ℝ≥0)) ω))) :
    Tendsto (fun n ↦ lintegral μ fun ω ↦ fs n ω) L (𝓝 (μ E))

Proof state:
case h.e'_5.h.e'_3
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))
aux : ∀ (ω : Ω), E.indicator (fun x => 1) ω = ↑(E.indicator (fun x => 1) ω)
⊢ μ E = ∫⁻ (ω : Ω), ↑(E.indicator (fun x => 1) ω) ∂μ

Tactic:
simp_rw [← aux, lintegral_indicator E_mble]

Result:
case h.e'_5.h.e'_3
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))
aux : ∀ (ω : Ω), E.indicator (fun x => 1) ω = ↑(E.indicator (fun x => 1) ω)
⊢ μ E = ∫⁻ (x : Ω) in E, 1 ∂μ

Proof state:
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))
ω : Ω
⊢ E.indicator (fun x => 1) ω = ↑(E.indicator (fun x => 1) ω)

Tactic:
simp only [ENNReal.coe_indicator, ENNReal.coe_one]

Result:
no goals

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

Tactic:
convert tendsto_lintegral_nn_filter_of_le_const μ fs_bdd fs_lim

Result:
case h.e'_5.h.e'_3
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))
⊢ μ E = ∫⁻ (ω : Ω), ↑(E.indicator (fun x => 1) ω) ∂μ

Proof state:
case h.e'_5.h.e'_3
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))
aux : ∀ (ω : Ω), E.indicator (fun x => 1) ω = ↑(E.indicator (fun x => 1) ω)
⊢ μ E = ∫⁻ (x : Ω) in E, 1 ∂μ

Tactic:
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]

Result:
no goals

Proof state:
case h.e'_5.h.e'_3
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))
⊢ μ E = ∫⁻ (ω : Ω), ↑(E.indicator (fun x => 1) ω) ∂μ

Tactic:
have aux : ∀ ω, indicator E (fun _ ↦ (1 : ℝ≥0∞)) ω = ↑(indicator E (fun _ ↦ (1 : ℝ≥0)) ω) :=
  fun ω ↦ by simp only [ENNReal.coe_indicator, ENNReal.coe_one]

Result:
case h.e'_5.h.e'_3
Ω : Type u_1
inst✝⁴ : TopologicalSpace Ω
inst✝³ : MeasurableSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (E.indicator (fun x => 1) ω))
aux : ∀ (ω : Ω), E.indicator (fun x => 1) ω = ↑(E.indicator (fun x => 1) ω)
⊢ μ E = ∫⁻ (ω : Ω), ↑(E.indicator (fun x => 1) ω) ∂μ