-- Mathlib/MeasureTheory/Measure/Regular.lean
/-- If `μ` is inner regular for finite measure sets with respect to compact sets
and is locally finite in an R₁ space,
then any compact set can be approximated from outside by open sets. -/
protected lemma _root_.IsCompact.measure_eq_iInf_isOpen [InnerRegularCompactLTTop μ]
    [IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) :
    μ K = ⨅ (U : Set α) (_ : K ⊆ U) (_ : IsOpen U), μ U

Proof state:
case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ μ K ≤ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U

Tactic:
simp only [le_iInf_iff]

Result:
case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ∀ (i : Set α), K ⊆ i → IsOpen i → μ K ≤ μ i

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ μ K = ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ μ K ≤ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U

case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U ≤ μ K

Proof state:
case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U ≤ μ K

Tactic:
apply le_of_forall_lt'

Result:
case a.H
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ∀ (c : ℝ≥0∞), μ K < c → ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U < c

Proof state:
case a.H
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ∀ (c : ℝ≥0∞), μ K < c → ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U < c

Tactic:
simpa only [iInf_lt_iff, exists_prop, exists_and_left] using hK.exists_isOpen_lt_of_lt

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ∀ (i : Set α), K ⊆ i → IsOpen i → μ K ≤ μ i

Tactic:
exact fun U KU _ ↦ measure_mono KU

Result:
no goals