-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem isCompact_isClosed {X : Type*} [TopologicalSpace X] [SigmaCompactSpace X]
    [MeasurableSpace X] (μ : Measure X) : InnerRegularWRT μ IsCompact IsClosed

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
this : μ F = ⨆ n, μ (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
rw [this] at hr

Result:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ n, μ (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
this : μ F = ⨆ n, μ (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ Monotone fun n => F ∩ B n

Tactic:
exact monotone_const.inter monotone_accumulate

Result:
no goals

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ μ.InnerRegularWRT IsCompact IsClosed

Tactic:
intro F hF r hr

Result:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ μ F = ⨆ n, μ (F ∩ B n)

Tactic:
rw [← Monotone.measure_iUnion, hBU]

Result:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ Monotone fun n => F ∩ B n

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
have : μ F = ⨆ n, μ (F ∩ B n) := by
  rw [← Monotone.measure_iUnion, hBU]
  exact monotone_const.inter monotone_accumulate

Result:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
this : μ F = ⨆ n, μ (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
set B : ℕ → Set X := compactCovering X

Result:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ⋃ n, F ∩ B n = F

Tactic:
rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]

Result:
no goals

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ n, μ (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
this : μ F = ⨆ n, μ (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

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

Result:
case intro
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ n, μ (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
this : μ F = ⨆ n, μ (F ∩ B n)
n : ℕ
hn : r < μ (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Proof state:
case intro
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ n, μ (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
this : μ F = ⨆ n, μ (F ∩ B n)
n : ℕ
hn : r < μ (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
exact ⟨_, inter_subset_left, hBc n, hn⟩

Result:
no goals

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
have hBc : ∀ n, IsCompact (F ∩ B n) := fun n => (isCompact_compactCovering X n).inter_left hF

Result:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
have hBU : ⋃ n, F ∩ B n = F := by rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]

Result:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K