-- Mathlib/MeasureTheory/Measure/Regular.lean
/-- Given a σ-finite measure, any measurable set can be approximated from inside by a measurable
set of finite measure. -/
lemma of_sigmaFinite [SigmaFinite μ] :
    InnerRegularWRT μ (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) (fun s ↦ MeasurableSet s)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ n, μ (s ∩ B n)
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Tactic:
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩

Result:
case intro
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ n, μ (s ∩ B n)
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
n : ℕ
hn : r < μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
⊢ ⋃ n, s ∩ B n = s

Tactic:
rw [← inter_iUnion, iUnion_spanningSets, inter_univ]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Tactic:
rw [this] at hr

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ n, μ (s ∩ B n)
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ n, s ∩ B n = s
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Tactic:
have : μ s = ⨆ n, μ (s ∩ B n) := by
  rw [← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion, hBU]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Tactic:
set B : ℕ → Set α := spanningSets μ

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Proof state:
case intro
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ n, μ (s ∩ B n)
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
n : ℕ
hn : r < μ (s ∩ B n)
⊢ μ (s ∩ B n) ≠ ⊤

Tactic:
exact ((measure_mono inter_subset_right).trans_lt (measure_spanningSets_lt_top μ n)).ne

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ n, s ∩ B n = s
⊢ μ s = ⨆ n, μ (s ∩ B n)

Tactic:
rw [← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion, hBU]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ μ.InnerRegularWRT (fun s => MeasurableSet s ∧ μ s ≠ ⊤) fun s => MeasurableSet s

Tactic:
intro s hs r hr

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Tactic:
have hBU : ⋃ n, s ∩ B n = s := by rw [← inter_iUnion, iUnion_spanningSets, inter_univ]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ n, s ∩ B n = s
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Proof state:
case intro
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ n, μ (s ∩ B n)
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
n : ℕ
hn : r < μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K

Tactic:
refine ⟨s ∩ B n, inter_subset_left, ⟨hs.inter (measurableSet_spanningSets μ n), ?_⟩, hn⟩

Result:
case intro
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ n, μ (s ∩ B n)
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
n : ℕ
hn : r < μ (s ∩ B n)
⊢ μ (s ∩ B n) ≠ ⊤