-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
lemma contentRegular_rieszContent : (rieszContent Λ).ContentRegular

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ⊤
ε : ℝ
hε : 0 < ε
⊢ ↑b.toNNReal ≤ ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})) + ε

Tactic:
lift ε to ℝ≥0 using hε.le

Result:
case intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ⊤
ε : ℝ≥0
hε : 0 < ↑ε
⊢ ↑b.toNNReal ≤ ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})) + ↑ε

Proof state:
case 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ⊤
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + ⟨↑ε, ⋯⟩)
α : ℝ≥0
hα : 1 < α
K' : Set X := ⇑f ⁻¹' Ici α⁻¹
hKK' : ↑K ⊆ interior K'
hK'cp : IsCompact K'
hb' : ↑K ⊆ interior K' → b ≤ ↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp })
⊢ b.toNNReal ≤ Λ (α • f)

Tactic:
exact (ENNReal.toNNReal_mono (by simp) <| hb' hKK').trans <| csInf_le'
  ⟨α • f, fun x ↦ (inv_le_iff_one_le_mul₀' (zero_lt_one.trans hα)).mp, by simp⟩

Result:
no goals

Proof state:
case 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ⊤
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + ⟨↑ε, ⋯⟩)
α : ℝ≥0
hα : 1 < α
K' : Set X := ⇑f ⁻¹' Ici α⁻¹
hKK' : ↑K ⊆ interior K'
hK'cp : IsCompact K'
⊢ b.toNNReal ≤ Λ (α • f)

Tactic:
set hb' := hb ⟨K', hK'cp⟩

Result:
case 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ⊤
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + ⟨↑ε, ⋯⟩)
α : ℝ≥0
hα : 1 < α
K' : Set X := ⇑f ⁻¹' Ici α⁻¹
hKK' : ↑K ⊆ interior K'
hK'cp : IsCompact K'
hb' : b ≤
  ⨅ (_ : ↑K ⊆ interior ↑{ carrier := K', isCompact' := hK'cp }),
    ↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp }) :=
  hb { carrier := K', isCompact' := hK'cp }
⊢ b.toNNReal ≤ Λ (α • f)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
⊢ (rieszContent Λ) K = ⨅ K', ⨅ (_ : ↑K ⊆ interior ↑K'), (rieszContent Λ) K'

Tactic:
simp only [rieszContent, le_antisymm_iff, le_iInf_iff, ENNReal.coe_le_coe, Content.mk_apply]

Result:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
⊢ (∀ (i : Compacts X), ↑K ⊆ interior ↑i → rieszContentAux Λ K ≤ rieszContentAux Λ i) ∧
    ⨅ K', ⨅ (_ : ↑K ⊆ interior ↑K'), ↑(rieszContentAux Λ K') ≤ ↑(rieszContentAux Λ K)

Proof state:
case 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ⊤
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + ⟨↑ε, ⋯⟩)
α : ℝ≥0
hα : 1 < α
K' : Set X := ⇑f ⁻¹' Ici α⁻¹
hKK' : ↑K ⊆ interior K'
hK'cp : IsCompact K'
hb' : b ≤
  ⨅ (_ : ↑K ⊆ interior ↑{ carrier := K', isCompact' := hK'cp }),
    ↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp }) :=
  hb { carrier := K', isCompact' := hK'cp }
⊢ b.toNNReal ≤ Λ (α • f)

Tactic:
simp only [Compacts.coe_mk, le_iInf_iff] at hb'

Result:
case 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ⊤
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + ⟨↑ε, ⋯⟩)
α : ℝ≥0
hα : 1 < α
K' : Set X := ⇑f ⁻¹' Ici α⁻¹
hKK' : ↑K ⊆ interior K'
hK'cp : IsCompact K'
hb' : ↑K ⊆ interior K' → b ≤ ↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp })
⊢ b.toNNReal ≤ Λ (α • f)