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

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
U : Set X
hU : IsOpen U
r : ℝ≥0∞
hr : r < μ U
⊢ ∃ K ⊆ U, IsClosed K ∧ r < μ K

Tactic:
rcases hU.exists_iUnion_isClosed with ⟨F, F_closed, -, rfl, F_mono⟩

Result:
case intro.intro.intro.intro
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ n, F n)
hr : r < μ (⋃ n, F n)
⊢ ∃ K ⊆ ⋃ n, F n, IsClosed K ∧ r < μ K

Proof state:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ μ.InnerRegularWRT IsClosed IsOpen

Tactic:
intro U hU r hr

Result:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
U : Set X
hU : IsOpen U
r : ℝ≥0∞
hr : r < μ U
⊢ ∃ K ⊆ U, IsClosed K ∧ r < μ K

Proof state:
case intro.intro.intro.intro
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ n, F n)
hr : r < ⨆ i, μ (F i)
⊢ ∃ K ⊆ ⋃ n, F n, IsClosed K ∧ r < μ K

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

Result:
case intro.intro.intro.intro.intro
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ n, F n)
hr : r < ⨆ i, μ (F i)
n : ℕ
hn : r < μ (F n)
⊢ ∃ K ⊆ ⋃ n, F n, IsClosed K ∧ r < μ K

Proof state:
case intro.intro.intro.intro.intro
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ n, F n)
hr : r < ⨆ i, μ (F i)
n : ℕ
hn : r < μ (F n)
⊢ ∃ K ⊆ ⋃ n, F n, IsClosed K ∧ r < μ K

Tactic:
exact ⟨F n, subset_iUnion _ _, F_closed n, hn⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ n, F n)
hr : r < μ (⋃ n, F n)
⊢ ∃ K ⊆ ⋃ n, F n, IsClosed K ∧ r < μ K

Tactic:
rw [F_mono.measure_iUnion] at hr

Result:
case intro.intro.intro.intro
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed (F n)
F_mono : Monotone F
hU : IsOpen (⋃ n, F n)
hr : r < ⨆ i, μ (F i)
⊢ ∃ K ⊆ ⋃ n, F n, IsClosed K ∧ r < μ K

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

Tactic:
let A : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X

Result:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ μ.InnerRegularWRT IsClosed IsOpen