-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem restrict_of_measure_ne_top [R1Space α] [BorelSpace α] [Regular μ]
    {A : Set α} (h'A : μ A ≠ ∞) : Regular (μ.restrict A)

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ (μ.restrict A) V ≠ ⊤

Tactic:
rw [restrict_apply hV.measurableSet]

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ μ (V ∩ A) ≠ ⊤

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ μ (V ∩ A) ≠ ⊤

Tactic:
exact ((measure_mono inter_subset_right).trans_lt h'A.lt_top).ne

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
⊢ (μ.restrict A).Regular

Tactic:
have : WeaklyRegular (μ.restrict A) := WeaklyRegular.restrict_of_measure_ne_top h'A

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
⊢ (μ.restrict A).Regular

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
⊢ (μ.restrict A).Regular

Tactic:
constructor

Result:
case innerRegular
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
⊢ (μ.restrict A).InnerRegularWRT IsCompact IsOpen

Proof state:
case innerRegular
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K

Tactic:
have R : restrict μ A V ≠ ∞ := by
  rw [restrict_apply hV.measurableSet]
  exact ((measure_mono inter_subset_right).trans_lt h'A.lt_top).ne

Result:
case innerRegular
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
R : (μ.restrict A) V ≠ ⊤
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K

Proof state:
case innerRegular
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
R : (μ.restrict A) V ≠ ⊤
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K

Tactic:
exact MeasurableSet.exists_lt_isCompact_of_ne_top hV.measurableSet R hr

Result:
no goals

Proof state:
case innerRegular
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
⊢ (μ.restrict A).InnerRegularWRT IsCompact IsOpen

Tactic:
intro V hV r hr

Result:
case innerRegular
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ⊤
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K