case intro.intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
inst✝ : LocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ ↑(Content.outerMeasure μ) K < ⊤
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
inst✝ : LocallyCompactSpace G
K : Set G
hK : IsCompact K
⊢ ↑(Content.outerMeasure μ) K < ⊤
rcases exists_compact_superset hK with ⟨F, h1F, h2F⟩
no goals
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
inst✝ : LocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ ↑(Content.outerMeasure μ) K < ⊤
calc
  μ.outerMeasure K ≤ μ.outerMeasure (interior F) := OuterMeasure.mono' _ h2F
  _ ≤ μ ⟨F, h1F⟩ := by
    apply μ.outerMeasure_le ⟨interior F, isOpen_interior⟩ ⟨F, h1F⟩ interior_subset
  _ < ⊤ := μ.lt_top _
no goals
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : T2Space G
inst✝ : LocallyCompactSpace G
K : Set G
hK : IsCompact K
F : Set G
h1F : IsCompact F
h2F : K ⊆ interior F
⊢ ↑(Content.outerMeasure μ) (interior F) ≤ (fun s => ↑(toFun μ s)) { carrier := F, isCompact' := h1F }
apply μ.outerMeasure_le ⟨interior F, isOpen_interior⟩ ⟨F, h1F⟩ interior_subset