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

Proof state:
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)
F : Set X
hF : IsCompact F ∧ K.carrier ⊆ interior F
⊢ b < ⊤

Tactic:
exact (le_iInf_iff.mp (hb ⟨F, hF.1⟩) hF.2).trans_lt ENNReal.coe_lt_top

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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
⊢ b ≤ ↑(rieszContentAux Λ K)

Tactic:
rw [rieszContentAux, ENNReal.le_coe_iff]

Result:
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)
⊢ ∃ p, b = ↑p ∧ p ≤ sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
⊢ (rieszContent Λ).ContentRegular

Tactic:
intro K

Result:
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'

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 < ⊤
ε : ℝ≥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 })
⊢ Λ (α • f) = Λ (α • f)

Tactic:
simp

Result:
no goals

Proof state:
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})) + ↑ε

Tactic:
obtain ⟨f, hfleoneonK, hfle⟩ := exists_lt_rieszContentAux_add_pos Λ K (Real.toNNReal_pos.mpr hε)

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 < rieszContentAux Λ K + (↑ε).toNNReal
⊢ ↑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 < rieszContentAux Λ K + (↑ε).toNNReal
⊢ ↑b.toNNReal ≤ ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})) + ↑ε

Tactic:
rw [rieszContentAux, Real.toNNReal_of_nonneg hε.le, ← NNReal.coe_lt_coe] at hfle

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}) + ⟨↑ε, ⋯⟩)
⊢ ↑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 < α
⊢ b.toNNReal ≤ Λ f * α

Tactic:
rw [mul_comm, ← smul_eq_mul, ← map_smul]

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 < α
⊢ b.toNNReal ≤ Λ (α • f)

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 α⁻¹
⊢ b.toNNReal ≤ Λ (α • f)

Tactic:
have hKK' : ↑K ⊆ interior K' :=
  subset_interior_iff.2 ⟨f ⁻¹' Ioi α⁻¹, isOpen_Ioi.preimage f.1.2,
    fun x hx ↦ (inv_lt_one_of_one_lt₀ hα).trans_le (hfleoneonK x hx),
    preimage_mono Ioi_subset_Ici_self⟩

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'
⊢ b.toNNReal ≤ Λ (α • f)

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}) + ⟨↑ε, ⋯⟩)
⊢ ↑b.toNNReal ≤ ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})) + ↑ε

Tactic:
refine ((le_iff_forall_one_lt_le_mul₀ (zero_le (Λ f))).mpr fun α hα ↦ ?_).trans hfle.le

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 < α
⊢ 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
⊢ ⨅ K', ⨅ (_ : ↑K ⊆ interior ↑K'), ↑(rieszContentAux Λ K') ≤ ↑(rieszContentAux Λ K)

Tactic:
rw [iInf_le_iff]

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