-- Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean
theorem measure_le_lintegral [MeasurableSpace X] [OpensMeasurableSpace X] (μ : Measure X) (n : ℕ) :
    μ F ≤ ∫⁻ x, (hF.apprSeq n x : ℝ≥0∞) ∂μ

Proof state:
case h.e'_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F = ∫⁻ (x : X), F.indicator (fun x => 1) x ∂μ

Tactic:
rw [lintegral_indicator hF.measurableSet]

Result:
case h.e'_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F = ∫⁻ (a : X) in F, 1 ∂μ

Proof state:
case hfg
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ (F.indicator fun x => 1) ≤ fun a => ↑((hF.apprSeq n) a)

Tactic:
intro x

Result:
case hfg
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
⊢ F.indicator (fun x => 1) x ≤ (fun a => ↑((hF.apprSeq n) a)) x

Proof state:
case hfg
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
⊢ F.indicator (fun x => 1) x ≤ (fun a => ↑((hF.apprSeq n) a)) x

Tactic:
by_cases hxF : x ∈ F

Result:
case pos
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
hxF : x ∈ F
⊢ F.indicator (fun x => 1) x ≤ (fun a => ↑((hF.apprSeq n) a)) x

case neg
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
hxF : x ∉ F
⊢ F.indicator (fun x => 1) x ≤ (fun a => ↑((hF.apprSeq n) a)) x

Proof state:
case pos
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
hxF : x ∈ F
⊢ F.indicator (fun x => 1) x ≤ (fun a => ↑((hF.apprSeq n) a)) x

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

Result:
no goals

Proof state:
case h.e'_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F = ∫⁻ (a : X) in F, 1 ∂μ

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

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ ∫⁻ (x : X), F.indicator (fun x => 1) x ∂μ ≤ ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ

Tactic:
apply lintegral_mono

Result:
case hfg
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ (F.indicator fun x => 1) ≤ fun a => ↑((hF.apprSeq n) a)

Proof state:
case neg
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
x : X
hxF : x ∉ F
⊢ F.indicator (fun x => 1) x ≤ (fun a => ↑((hF.apprSeq n) a)) x

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

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F ≤ ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ

Tactic:
convert_to ∫⁻ x, (F.indicator (fun _ ↦ (1 : ℝ≥0∞))) x ∂μ ≤ ∫⁻ x, hF.apprSeq n x ∂μ

Result:
case h.e'_3
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F = ∫⁻ (x : X), F.indicator (fun x => 1) x ∂μ

X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ ∫⁻ (x : X), F.indicator (fun x => 1) x ∂μ ≤ ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ