awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
δ : ℝ
δ_pos : 0 < δ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ (↑(((thickenedIndicator δ_pos F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
δ : ℝ
δ_pos : 0 < δ
refine : ∀ (x : Ω), ‖(↑(((thickenedIndicator δ_pos F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ)‖ ≤ 1
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ (↑(((thickenedIndicator δ_pos F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)) μ

Tactic:
refine .of_bound (by fun_prop) 1 (ae_of_all _ fun x ↦ ?_)
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
δ : ℝ
δ_pos : 0 < δ
x : Ω
⊢ ‖(↑(((thickenedIndicator δ_pos F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ)‖ ≤ 1

Tactic:
simpa using thickenedIndicator_le_one δ_pos F x

Premises used: thickenedIndicator_le_one
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)

Tactic:
have h := tendsto_lintegral_thickenedIndicator_of_isClosed μ F_closed δs_pos δs_lim
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
n : ℕ
hfi : Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ)) μ
⊢ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
    ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)

Tactic:
rw [lintegral_coe_eq_integral]

Premises used: MeasureTheory.lintegral_coe_eq_integral
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
n : ℕ
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ)) μ

Tactic:
integrable_thickenedIndicator F (δs_pos _)

Premises used: MeasureTheory.integrable_thickenedIndicator
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
n : ℕ
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ)) μ

Tactic:
exact integrable_thickenedIndicator F (δs_pos _)

Premises used: MeasureTheory.integrable_thickenedIndicator
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
⊢ ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)

Tactic:
have h_eq (n : ℕ) : ∫⁻ ω, thickenedIndicator (δs_pos n) F ω ∂μ
      = ENNReal.ofReal (∫ ω, fs n ω ∂μ) := by
    rw [lintegral_coe_eq_integral]
    exact integrable_thickenedIndicator F (δs_pos _)
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)

Tactic:
simp_rw [h_eq] at h
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
h₁ : ∀ (n : ℕ), ∫ (ω : Ω), fs n ω ∂μ = (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂μ) fun (n : ℕ) ↦
    (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal

Tactic:
ext n
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
n : ℕ
h₁ : LE.le (α := ℝ) 0 (∫ (ω : Ω), fs n ω ∂μ)
⊢ ∫ (ω : Ω), fs n ω ∂μ = (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal

Tactic:
rw [ENNReal.toReal_ofReal]

Premises used: ENNReal.toReal_ofReal
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
n : ℕ
x : Ω
⊢ 0 x ≤ fs n x

Tactic:
simp [fs]
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
n : ℕ
⊢ LE.le (α := ℝ) 0 (∫ (ω : Ω), fs n ω ∂μ)

Tactic:
exact integral_nonneg fun x ↦ by simp [fs]

Premises used: MeasureTheory.integral_nonneg
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂μ) fun (n : ℕ) ↦
    (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal

Tactic:
have h_eq' : (fun n ↦ ∫ ω, fs n ω ∂μ) = fun n ↦ (ENNReal.ofReal (∫ ω, fs n ω ∂μ)).toReal := by
    ext n
    rw [ENNReal.toReal_ofReal]
    exact integral_nonneg fun x ↦ by simp [fs]
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
h_eq' :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂μ) fun (n : ℕ) ↦
    (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
⊢ ∀ (i : ℕ), ENNReal.ofReal (∫ (ω : Ω), fs i ω ∂μ) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
h_eq' :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂μ) fun (n : ℕ) ↦
    (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
h_eq' :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂μ) fun (n : ℕ) ↦
    (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
rwa :
  Tendsto (fun (n : ℕ) ↦ (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal) atTop
    (𝓝 (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) F)))
rwa₁ rwa₂ rwa₃ rwa₄ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ) ∂μ) atTop
    (𝓝 (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) F)))

Tactic:
rwa [h_eq', ENNReal.tendsto_toReal_iff (by simp) (by finiteness)]

Premises used: ENNReal.tendsto_toReal_iff
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
n : ℕ
x : X
⊢ LE.le (α := ℝ≥0) ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)

Tactic:
(Exists.choose_spec (HasOuterApproxClosed.exAppr F hF)).1 n x

Premises used: Exists.choose_spec, And.left, HasOuterApproxClosed.exAppr
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
n : ℕ
x : X
hxF : x ∈ F
⊢ Eq (α := ℝ≥0) ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)

Tactic:
le_antisymm (apprSeq_apply_le_one _ _ _)
    ((Exists.choose_spec (HasOuterApproxClosed.exAppr F hF)).2.1 n x hxF)

Premises used: Exists.choose_spec, le_antisymm, And.right, And.left, HasOuterApproxClosed.apprSeq_apply_le_one, HasOuterApproxClosed.exAppr
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
⊢ Tendsto (β := (x : X) → ℝ≥0) (fun (n : ℕ) (x : X) ↦ (hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x) atTop
    (𝓝 (F.indicator fun (x : X) ↦ 1))

Tactic:
(Exists.choose_spec (HasOuterApproxClosed.exAppr F hF)).2.2

Premises used: Exists.choose_spec, And.right, HasOuterApproxClosed.exAppr
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
n : ℕ
x : X
pos :
  ∀ (hxF : x ∈ F),
    LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
      ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)
neg :
  ∀ (hxF : x ∉ F),
    LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
      ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
    ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
by_cases hxF : x ∈ F
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
n : ℕ
x : X
hxF : x ∈ F
⊢ LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
    ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
simp only [hxF, indicator_of_mem, apprSeq_apply_eq_one hF n, le_refl]

Premises used: le_refl, HasOuterApproxClosed.apprSeq_apply_eq_one, Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
n : ℕ
x : X
hxF : x ∉ F
⊢ LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
    ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
simp only [hxF, not_false_eq_true, indicator_of_notMem, zero_le]

Premises used: zero_le, Set.indicator_of_notMem, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
h : (μ : (a : Set X) → ℝ≥0∞) F = ∫⁻ (x : X), F.indicator (fun (x : X) ↦ 1) x ∂μ
convert_to :
  ∫⁻ (x : X), F.indicator (fun (x : X) ↦ 1) x ∂μ ≤ ∫⁻ (x : X), (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ
⊢ (μ : (a : Set X) → ℝ≥0∞) F ≤ ∫⁻ (x : X), (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
convert_to ∫⁻ x, (F.indicator (fun _ ↦ (1 : ℝ≥0∞))) x ∂μ ≤ ∫⁻ x, hF.apprSeq n x ∂μ
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
h : (μ : (a : Set X) → ℝ≥0∞) F = ∫⁻ (a : X) in F, 1 ∂μ
⊢ (μ : (a : Set X) → ℝ≥0∞) F = ∫⁻ (x : X), F.indicator (fun (x : X) ↦ 1) x ∂μ

Tactic:
rw [lintegral_indicator hF.measurableSet]

Premises used: IsClosed.measurableSet, MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ (μ : (a : Set X) → ℝ≥0∞) F = ∫⁻ (a : X) in F, 1 ∂μ

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

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ, MeasureTheory.lintegral_one
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
hfg :
  LE.le (α := X → ℝ≥0∞) (F.indicator fun (x : X) ↦ 1) fun (a : X) ↦
    (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)
⊢ ∫⁻ (x : X), F.indicator (fun (x : X) ↦ 1) x ∂μ ≤ ∫⁻ (x : X), (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
apply lintegral_mono

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
pos :
  ∀ (hxF : x ∈ F),
    LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
      ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)
neg :
  ∀ (hxF : x ∉ F),
    LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
      ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)
⊢ LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
    ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)

Tactic:
by_cases hxF : x ∈ F
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
hxF : x ∈ F
⊢ LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
    ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)

Tactic:
simp only [hxF, indicator_of_mem, apprSeq_apply_eq_one hF n hxF, ENNReal.coe_one, le_refl]

Premises used: le_refl, ENNReal.coe_one, HasOuterApproxClosed.apprSeq_apply_eq_one, Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
hxF : x ∉ F
⊢ LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
    ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)

Tactic:
simp only [hxF, not_false_eq_true, indicator_of_notMem, zero_le]

Premises used: zero_le, Set.indicator_of_notMem, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : X), (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ) atTop
    (𝓝 ((μ : (a : Set X) → ℝ≥0∞) F) : Filter ℝ≥0∞)

Tactic:
measure_of_cont_bdd_of_tendsto_indicator μ hF.measurableSet hF.apprSeq
    (apprSeq_apply_le_one hF) (tendsto_apprSeq hF)

Premises used: MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator, HasOuterApproxClosed.tendsto_apprSeq, IsClosed.measurableSet, IsClosed.apprSeq, HasOuterApproxClosed.apprSeq_apply_le_one
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
⊢ HasOuterApproxClosed X

Tactic:
⟨fun F hF ↦ ?_⟩

Premises used: HasOuterApproxClosed.mk
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
refine :
  ∀ (F : Set X) (hF : IsClosed[inst] F),
    ∃ (fseq : ℕ → X →ᵇ ℝ≥0),
      (∀ (n : ℕ) (x : X), LE.le (α := ℝ≥0) ((fseq n : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)) ∧
        (∀ (n : ℕ), ∀ x ∈ F, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((fseq n : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
          Tendsto (β := (x : X) → ℝ≥0) (fun (n : ℕ) (x : X) ↦ (fseq n : (a : X) → ℝ≥0) x) atTop
            (𝓝 (F.indicator fun (x : X) ↦ 1))
⊢ HasOuterApproxClosed X

Tactic:
refine ⟨fun F hF ↦ ?_⟩