-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem weaklyRegular_of_finite [BorelSpace α] (μ : Measure α) [IsFiniteMeasure μ]
    (H : InnerRegularWRT μ IsClosed IsOpen) : WeaklyRegular μ

Proof state:
case iUnion.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H : ∀ (i : ℕ) (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed F ∧ IsOpen U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed (F n)
hUo : ∀ (n : ℕ), IsOpen (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t => ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
⊢ ∃ F ⊆ ⋃ i, s i, ∃ U ⊇ ⋃ i, s i, IsClosed F ∧ IsOpen U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε

Tactic:
rcases (this.eventually <| lt_mem_nhds <| ENNReal.lt_add_right hfin ε0').exists with ⟨t, ht⟩

Result:
case iUnion.intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H : ∀ (i : ℕ) (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed F ∧ IsOpen U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : ℕ → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : ℕ → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed (F n)
hUo : ∀ (n : ℕ), IsOpen (U n)
hF : ∀ (n : ℕ), μ (s n) ≤ μ (F n) + δ n
hU : ∀ (n : ℕ), μ (U n) ≤ μ (s n) + δ n
this : Tendsto (fun t => ∑ k ∈ t, μ (s k) + ε / 2) atTop (𝓝 (μ (⋃ n, s n) + ε / 2))
t : Finset ℕ
ht : μ (⋃ n, s n) < ∑ k ∈ t, μ (s k) + ε / 2
⊢ ∃ F ⊆ ⋃ i, s i, ∃ U ⊇ ⋃ i, s i, IsClosed F ∧ IsOpen U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
this :
  ∀ (s : Set α),
    MeasurableSet s → ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
⊢ ∃ U ⊇ s, IsOpen U ∧ μ U < r

Tactic:
rcases exists_between hr with ⟨r', hsr', hr'r⟩

Result:
case intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
this :
  ∀ (s : Set α),
    MeasurableSet s → ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
r' : ℝ≥0∞
hsr' : μ s < r'
hr'r : r' < r
⊢ ∃ U ⊇ s, IsOpen U ∧ μ U < r

Proof state:
case intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
this :
  ∀ (s : Set α),
    MeasurableSet s → ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
r' : ℝ≥0∞
hsr' : μ s < r'
hr'r : r' < r
⊢ ∃ U ⊇ s, IsOpen U ∧ μ U < r

Tactic:
rcases this s hs _ (tsub_pos_iff_lt.2 hsr').ne' with ⟨-, -, U, hsU, -, hUo, -, H⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
this :
  ∀ (s : Set α),
    MeasurableSet s → ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
r' : ℝ≥0∞
hsr' : μ s < r'
hr'r : r' < r
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
H : μ U ≤ μ s + (r' - μ s)
⊢ ∃ U ⊇ s, IsOpen U ∧ μ U < r

Proof state:
case iUnion
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H : ∀ (i : ℕ) (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed F ∧ IsOpen U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
⊢ ∃ F ⊆ ⋃ i, s i, ∃ U ⊇ ⋃ i, s i, IsClosed F ∧ IsOpen U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε

Tactic:
rcases ENNReal.exists_pos_sum_of_countable' ε0' ℕ with ⟨δ, δ0, hδε⟩

Result:
case iUnion.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H : ∀ (i : ℕ) (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s i, ∃ U ⊇ s i, IsClosed F ∧ IsOpen U ∧ μ (s i) ≤ μ F + ε ∧ μ U ≤ μ (s i) + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
⊢ ∃ F ⊆ ⋃ i, s i, ∃ U ⊇ ⋃ i, s i, IsClosed F ∧ IsOpen U ∧ μ (⋃ i, s i) ≤ μ F + ε ∧ μ U ≤ μ (⋃ i, s i) + ε

Proof state:
case compl
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
⊢ ∀ (t : Set α),
    MeasurableSet t →
      (∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ t, ∃ U ⊇ t, IsClosed F ∧ IsOpen U ∧ μ t ≤ μ F + ε ∧ μ U ≤ μ t + ε) →
        ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ tᶜ, ∃ U ⊇ tᶜ, IsClosed F ∧ IsOpen U ∧ μ tᶜ ≤ μ F + ε ∧ μ U ≤ μ tᶜ + ε

Tactic:
rintro s hs H ε hε

Result:
case compl
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
s : Set α
hs : MeasurableSet s
H : ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ F ⊆ sᶜ, ∃ U ⊇ sᶜ, IsClosed F ∧ IsOpen U ∧ μ sᶜ ≤ μ F + ε ∧ μ U ≤ μ sᶜ + ε

Proof state:
case isOpen
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
U : Set α
hU : IsOpen U
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ F ⊆ U, ∃ U_1 ⊇ U, IsClosed F ∧ IsOpen U_1 ∧ μ U ≤ μ F + ε ∧ μ U_1 ≤ μ U + ε

Tactic:
rcases H.exists_subset_lt_add isClosed_empty hU hfin hε with ⟨F, hsF, hFc, hF⟩

Result:
case isOpen.intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed IsOpen
hfin : ∀ {s : Set α}, μ s ≠ ⊤
U : Set α
hU : IsOpen U
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hsF : F ⊆ U
hFc : IsClosed F
hF : μ U < μ F + ε
⊢ ∃ F ⊆ U, ∃ U_1 ⊇ U, IsClosed F ∧ IsOpen U_1 ∧ μ U ≤ μ F + ε ∧ μ U_1 ≤ μ U + ε