-- Mathlib/MeasureTheory/Measure/Content.lean
theorem measure_eq_content_of_regular (H : MeasureTheory.Content.ContentRegular μ)
    (K : TopologicalSpace.Compacts G) : μ.measure ↑K = μ K

Proof state:
case refine_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ ∀ (ε : ℝ≥0), 0 < ε → μ K < ⊤ → μ.measure ↑K ≤ μ K + ↑ε

Tactic:
intro ε εpos _

Result:
case refine_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : μ K < ⊤
⊢ μ.measure ↑K ≤ μ K + ↑ε

Proof state:
case refine_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ K ≤ μ.measure ↑K

Tactic:
calc
μ K ≤ μ ⟨closure K, K.2.closure⟩ := μ.mono _ _ subset_closure
_ ≤ μ.measure (closure K) := by
  rw [μ.measure_apply (isClosed_closure.measurableSet)]
  exact μ.le_outerMeasure_compacts _
_ = μ.measure K := K.2.measure_closure _

Result:
no goals

Proof state:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : μ K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ μ.outerMeasure (interior ↑K') ≤ μ K'

Tactic:
exact μ.outerMeasure_interior_compacts K'

Result:
no goals

Proof state:
case refine_1.h.intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : μ K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ μ.measure ↑K ≤ μ K + ↑ε

Tactic:
calc
  μ.measure ↑K ≤ μ.measure (interior ↑K') := measure_mono K'_hyp.1
  _ ≤ μ K' := by
    rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]
    exact μ.outerMeasure_interior_compacts K'
  _ ≤ μ K + ε := K'_hyp.right

Result:
no goals

Proof state:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : μ K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ μ.measure (interior ↑K') ≤ μ K'

Tactic:
rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]

Result:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : μ K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ μ.outerMeasure (interior ↑K') ≤ μ K'

Proof state:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ { carrier := closure ↑K, isCompact' := ⋯ } ≤ μ.measure (closure ↑K)

Tactic:
rw [μ.measure_apply (isClosed_closure.measurableSet)]

Result:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ { carrier := closure ↑K, isCompact' := ⋯ } ≤ μ.outerMeasure (closure ↑K)

Proof state:
case refine_1
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ.measure ↑K ≤ μ K

Tactic:
apply ENNReal.le_of_forall_pos_le_add

Result:
case refine_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ ∀ (ε : ℝ≥0), 0 < ε → μ K < ⊤ → μ.measure ↑K ≤ μ K + ↑ε

Proof state:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ { carrier := closure ↑K, isCompact' := ⋯ } ≤ μ.outerMeasure (closure ↑K)

Tactic:
exact μ.le_outerMeasure_compacts _

Result:
no goals

Proof state:
case refine_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : μ K < ⊤
⊢ μ.measure ↑K ≤ μ K + ↑ε

Tactic:
obtain ⟨K', K'_hyp⟩ := contentRegular_exists_compact μ H K (ne_bot_of_gt εpos)

Result:
case refine_1.h.intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : μ K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ μ.measure ↑K ≤ μ K + ↑ε

Proof state:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ.measure ↑K = μ K

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ.measure ↑K ≤ μ K

case refine_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ K ≤ μ.measure ↑K