-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
lemma le_rieszMeasure_of_isCompact_tsupport_subset {f : C_c(X, ℝ≥0)} (hf : ∀ x, f x ≤ 1)
    {K : Set X} (hK : IsCompact K) (h : tsupport f ⊆ K) : .ofNNReal (Λ f) ≤ rieszMeasure Λ K

Proof state:
case a
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
⊢ f ≤ g

Tactic:
intro x

Result:
case a
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
x : X
⊢ f x ≤ g x

Proof state:
case pos
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
x : X
hx : x ∈ tsupport ⇑f
⊢ f x ≤ g x

Tactic:
exact le_trans (hf x) (hg.1 x (Set.mem_of_subset_of_mem h hx))

Result:
no goals

Proof state:
case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
x : X
hx : x ∉ tsupport ⇑f
⊢ f x ≤ g x

Tactic:
rw [image_eq_zero_of_nmem_tsupport hx]

Result:
case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
x : X
hx : x ∉ tsupport ⇑f
⊢ 0 ≤ g x

Proof state:
case a
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
x : X
⊢ f x ≤ g x

Tactic:
by_cases hx : x ∈ tsupport f

Result:
case pos
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
x : X
hx : x ∈ tsupport ⇑f
⊢ f x ≤ g x

case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
x : X
hx : x ∉ tsupport ⇑f
⊢ f x ≤ g x

Proof state:
case intro
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
⊢ Λ f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK } + ε

Tactic:
apply le_trans _ hg.2.le

Result:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
⊢ Λ f ≤ Λ g

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
⊢ ↑(Λ f) ≤ (rieszMeasure Λ) K

Tactic:
rw [← TopologicalSpace.Compacts.coe_mk K hK]

Result:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
⊢ ↑(Λ f) ≤ (rieszMeasure Λ) ↑{ carrier := K, isCompact' := hK }

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
⊢ ↑(Λ f) ≤ (rieszMeasure Λ) ↑{ carrier := K, isCompact' := hK }

Tactic:
simp only [rieszMeasure, Content.measure_eq_content_of_regular (rieszContent Λ)
  (contentRegular_rieszContent Λ)]

Result:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
⊢ ↑(Λ f) ≤ (rieszContent Λ) { carrier := K, isCompact' := hK }

Proof state:
case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
x : X
hx : x ∉ tsupport ⇑f
⊢ 0 ≤ g x

Tactic:
exact zero_le (g x)

Result:
no goals

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
⊢ Λ f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK } + ε

Tactic:
obtain ⟨g, hg⟩ := exists_lt_rieszContentAux_add_pos Λ ⟨K, hK⟩ hε

Result:
case intro
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
⊢ Λ f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK } + ε