case refine'_1
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K

case refine'_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑↑(Content.measure μ) ↑K
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ ↑↑(Content.measure μ) ↑K = (fun s => ↑(toFun μ s)) K
refine' le_antisymm _ _
case refine'_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ ∀ (ε : ℝ≥0), 0 < ε → (fun s => ↑(toFun μ s)) K < ⊤ → ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K + ↑ε
case refine'_1
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K
apply ENNReal.le_of_forall_pos_le_add
case refine'_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
⊢ ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K + ↑ε
case refine'_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ ∀ (ε : ℝ≥0), 0 < ε → (fun s => ↑(toFun μ s)) K < ⊤ → ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K + ↑ε
intro ε εpos _
case refine'_1.h.intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K + ↑ε
case refine'_1.h
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
⊢ ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K + ↑ε
obtain ⟨K', K'_hyp⟩ := contentRegular_exists_compact μ H K (ne_bot_of_gt εpos)
no goals
case refine'_1.h.intro
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑↑(Content.measure μ) ↑K ≤ (fun s => ↑(toFun μ s)) K + ↑ε
calc
  μ.measure ↑K ≤ μ.measure (interior ↑K') := by
    rw [μ.measure_apply isOpen_interior.measurableSet,
      μ.measure_apply K.isCompact.measurableSet]
    exact μ.outerMeasure.mono K'_hyp.left
  _ ≤ μ K' := by
    rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]
    exact μ.outerMeasure_interior_compacts K'
  _ ≤ μ K + ε := K'_hyp.right
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑(Content.outerMeasure μ) ↑K ≤ ↑(Content.outerMeasure μ) (interior ↑K')
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑↑(Content.measure μ) ↑K ≤ ↑↑(Content.measure μ) (interior ↑K')
rw [μ.measure_apply isOpen_interior.measurableSet,
  μ.measure_apply K.isCompact.measurableSet]
no goals
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑(Content.outerMeasure μ) ↑K ≤ ↑(Content.outerMeasure μ) (interior ↑K')
exact μ.outerMeasure.mono K'_hyp.left
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑(Content.outerMeasure μ) (interior ↑K') ≤ (fun s => ↑(toFun μ s)) K'
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑↑(Content.measure μ) (interior ↑K') ≤ (fun s => ↑(toFun μ s)) K'
rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]
no goals
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : (fun s => ↑(toFun μ s)) K < ⊤
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ (fun s => ↑(toFun μ s)) K' ≤ (fun s => ↑(toFun μ s)) K + ↑ε
⊢ ↑(Content.outerMeasure μ) (interior ↑K') ≤ (fun s => ↑(toFun μ s)) K'
exact μ.outerMeasure_interior_compacts K'
case refine'_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑(Content.outerMeasure μ) ↑K
case refine'_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑↑(Content.measure μ) ↑K
rw [μ.measure_apply (IsCompact.measurableSet K.isCompact)]
no goals
case refine'_2
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : T2Space G
inst✝ : BorelSpace G
H : ContentRegular μ
K : Compacts G
⊢ (fun s => ↑(toFun μ s)) K ≤ ↑(Content.outerMeasure μ) ↑K
exact μ.le_outerMeasure_compacts K