-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
theorem rieszContentAux_image_nonempty (K : Compacts X) :
    (Λ '' { f : C_c(X, ℝ≥0) | ∀ x ∈ K, (1 : ℝ≥0) ≤ f x }).Nonempty

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
⊢ {f | ∀ x ∈ K, 1 ≤ f x}.Nonempty

Tactic:
have hfHasCompactSupport : HasCompactSupport f :=
  IsCompact.of_isClosed_subset hVcp (isClosed_tsupport f)
    (Set.Subset.trans hsuppfsubV interior_subset)

Result:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
⊢ {f | ∀ x ∈ K, 1 ≤ f x}.Nonempty

Proof state:
case h
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
⊢ { toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport }.nnrealPart ∈ {f | ∀ x ∈ K, 1 ≤ f x}

Tactic:
intro x hx

Result:
case h
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
x : X
hx : x ∈ K
⊢ 1 ≤ { toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport }.nnrealPart x

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ closure (interior V) ⊆ closure V

Tactic:
exact closure_mono interior_subset

Result:
no goals

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ IsCompact (closure (interior V))

Tactic:
apply IsCompact.of_isClosed_subset hVcp isClosed_closure

Result:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ closure (interior V) ⊆ V

Proof state:
case h.hab
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
x : X
hx : x ∈ K
⊢ 1 = (f x).toNNReal

Tactic:
rw [← Real.toNNReal_one, Real.toNNReal_eq_toNNReal_iff (zero_le_one' ℝ) (hfinicc x).1]

Result:
case h.hab
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
x : X
hx : x ∈ K
⊢ 1 = f x

Proof state:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ {f | ∀ x ∈ K, 1 ≤ f x}.Nonempty

Tactic:
have hIsCompact_closure_interior : IsCompact (closure (interior V)) := by
  apply IsCompact.of_isClosed_subset hVcp isClosed_closure
  nth_rw 2 [← closure_eq_iff_isClosed.mpr (IsCompact.isClosed hVcp)]
  exact closure_mono interior_subset

Result:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
⊢ {f | ∀ x ∈ K, 1 ≤ f x}.Nonempty

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ closure (interior V) ⊆ V

Tactic:
nth_rw 2 [← closure_eq_iff_isClosed.mpr (IsCompact.isClosed hVcp)]

Result:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ closure (interior V) ⊆ closure V

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
⊢ {f | ∀ x ∈ K, 1 ≤ f x}.Nonempty

Tactic:
use nnrealPart ⟨f, hfHasCompactSupport⟩

Result:
case h
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
⊢ { toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport }.nnrealPart ∈ {f | ∀ x ∈ K, 1 ≤ f x}

Proof state:
case h.hab
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
x : X
hx : x ∈ K
⊢ 1 = { toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport }.nnrealPart x

Tactic:
simp only [nnrealPart_apply, CompactlySupportedContinuousMap.coe_mk]

Result:
case h.hab
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
x : X
hx : x ∈ K
⊢ 1 = (f x).toNNReal