awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
obtain : ∀ (F : Set X) (hF : IsCompact F ∧ K.carrier ⊆ interior F), b < ∞
⊢ b < ∞

Tactic:
obtain ⟨F, hF⟩ := exists_compact_superset K.2

Premises used: TopologicalSpace.Compacts.isCompact', exists_compact_superset
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
F : Set X
hF : IsCompact F ∧ K.carrier ⊆ interior F
⊢ b < ∞

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

Premises used: le_iInf_iff, TopologicalSpace.Compacts.mk, And.right, And.left, Iff.mp, LE.le.trans_lt, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
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

Premises used: le_iInf_iff, TopologicalSpace.Compacts.mk, And.right, And.left, Iff.mp, LE.le.trans_lt, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
⊢ b < ∞

Tactic:
have : b < ⊤ := by
    obtain ⟨F, hF⟩ := exists_compact_superset K.2
    exact (le_iInf_iff.mp (hb ⟨F, hF.1⟩) hF.2).trans_lt ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
⊢ ∃ (p : ℝ≥0),
    b = (↑p : ℝ≥0∞) ∧
      p ≤
        sInf
          (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
            {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})

Tactic:
⟨b.toNNReal, (ENNReal.coe_toNNReal this.ne).symm, NNReal.coe_le_coe.mp ?_⟩

Premises used: ENNReal.coe_toNNReal, ENNReal.toNNReal, And.intro, Exists.intro, Iff.mp, Eq.symm, NNReal.coe_le_coe, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
refine :
  (↑b.toNNReal : ℝ) ≤
    (↑(sInf
          (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
            {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})) :
      ℝ)
⊢ ∃ (p : ℝ≥0),
    b = (↑p : ℝ≥0∞) ∧
      p ≤
        sInf
          (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
            {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})

Tactic:
refine ⟨b.toNNReal, (ENNReal.coe_toNNReal this.ne).symm, NNReal.coe_le_coe.mp ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
apply :
  ∀ (ε : ℝ),
    0 < ε →
      (↑b.toNNReal : ℝ) ≤
        (↑(sInf
                (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
                  {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})) :
            ℝ) +
          ε
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(sInf
          (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
            {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})) :
      ℝ)

Tactic:
apply le_iff_forall_pos_le_add.mpr

Premises used: Iff.mpr, le_iff_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ
hε : 0 < ε
⊢ 0 ≤ ε

Tactic:
hε.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ
hε : 0 < ε
lift :
  ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ)),
    (↑b.toNNReal : ℝ) ≤
      (↑(sInf
              (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
                {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})) :
          ℝ) +
        (↑ε : ℝ)
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})) :
        ℝ) +
      ε

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

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
obtain :
  ∀ (f : X →C_c ℝ≥0) (hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0))
    (hfle : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + (↑ε : ℝ).toNNReal),
    (↑b.toNNReal : ℝ) ≤
      (↑(sInf
              (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
                {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})) :
          ℝ) +
        (↑ε : ℝ)
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})) :
        ℝ) +
      (↑ε : ℝ)

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

Premises used: Iff.mpr, Real.toNNReal_pos, exists_lt_rieszContentAux_add_pos
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + (↑ε : ℝ).toNNReal
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)

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

Premises used: LT.lt.le, rieszContentAux, NNReal.coe_lt_coe, Real.toNNReal_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})) :
        ℝ) +
      (↑ε : ℝ)

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

Premises used: Iff.mpr, zero_le, le_iff_forall_one_lt_le_mul₀, LT.lt.le, NNReal, LE.le.trans, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
refine : ∀ (α : ℝ≥0) (hα : 1 < α), b.toNNReal ≤ HMul.hMul (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f : ℝ≥0) α
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})) :
        ℝ) +
      (↑ε : ℝ)

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

Premises used: Iff.mpr, zero_le, le_iff_forall_one_lt_le_mul₀, LT.lt.le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
α : ℝ≥0
hα : 1 < α
rw : b.toNNReal ≤ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (α • f)
⊢ b.toNNReal ≤ HMul.hMul (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f : ℝ≥0) α

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

Premises used: mul_comm, smul_eq_mul, map_smul
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
α : ℝ≥0
hα : 1 < α
K' : Set X := (⇑f : (a : X) → ℝ≥0) ⁻¹' Ici α⁻¹
⊢ (↑K : Set X) ⊆ interior K'

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⟩
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
α : ℝ≥0
hα : 1 < α
K' : Set X := (⇑f : (a : X) → ℝ≥0) ⁻¹' Ici α⁻¹
hKK' : (↑K : Set X) ⊆ interior K'
⊢ IsCompact K'

Tactic:
have hK'cp : IsCompact K' := .of_isClosed_subset f.2 (isClosed_Ici.preimage f.1.2) fun x hx ↦
    subset_closure ((inv_pos_of_pos <| zero_lt_one.trans hα).trans_le hx).ne'
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
α : ℝ≥0
hα : 1 < α
K' : Set X := (⇑f : (a : X) → ℝ≥0) ⁻¹' Ici α⁻¹
hKK' : (↑K : Set X) ⊆ interior K'
hK'cp : IsCompact K'
hb' : b ≤
  ⨅ (_ : (↑K : Set X) ⊆ interior (↑{ carrier := K', isCompact' := hK'cp : Compacts X } : Set X)),
    (↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp }) : ℝ≥0∞) :=
  ⋯
⊢ ∀ (i : (↑K : Set X) ⊆ interior K'), b ≤ (↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp }) : ℝ≥0∞)

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

Premises used: le_iInf_iff, TopologicalSpace.Compacts.coe_mk
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
α : ℝ≥0
hα : 1 < α
K' : Set X := (⇑f : (a : X) → ℝ≥0) ⁻¹' Ici α⁻¹
hKK' : (↑K : Set X) ⊆ interior K'
hK'cp : IsCompact K'
hb' : ∀ (i : (↑K : Set X) ⊆ interior K'), b ≤ (↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp }) : ℝ≥0∞)
⊢ (↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp : Compacts X }) : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
α : ℝ≥0
hα : 1 < α
K' : Set X := (⇑f : (a : X) → ℝ≥0) ⁻¹' Ici α⁻¹
hKK' : (↑K : Set X) ⊆ interior K'
hK'cp : IsCompact K'
hb' : ∀ (i : (↑K : Set X) ⊆ interior K'), b ≤ (↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp }) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (α • f) : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (α • f) : ℝ≥0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(sInf
            (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
              {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
α : ℝ≥0
hα : 1 < α
K' : Set X := (⇑f : (a : X) → ℝ≥0) ⁻¹' Ici α⁻¹
hKK' : (↑K : Set X) ⊆ interior K'
hK'cp : IsCompact K'
hb' : ∀ (i : (↑K : Set X) ⊆ interior K'), b ≤ (↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp }) : ℝ≥0∞)
⊢ b.toNNReal ≤ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (α • 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⟩

Premises used: ENNReal.toNNReal_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
K : Set X
hK : IsCompact K
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ K
rw :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (↑{ carrier := K, isCompact' := hK : Compacts X } : Set X)
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤ ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) K

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

Premises used: TopologicalSpace.Compacts.coe_mk
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
K : Set X
hK : IsCompact K
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ K
simp :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
    (rieszContent Λ : (a : Compacts X) → ℝ≥0∞) { carrier := K, isCompact' := hK }
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (↑{ carrier := K, isCompact' := hK : Compacts X } : Set X)

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

Premises used: MeasureTheory.Content.measure_eq_content_of_regular, NNRealRMK.rieszMeasure, rieszContent, contentRegular_rieszContent
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
K : Set X
hK : IsCompact K
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ K
simp : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X }
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
    (rieszContent Λ : (a : Compacts X) → ℝ≥0∞) { carrier := K, isCompact' := hK }

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

Premises used: ENNReal.coe_le_coe, rieszContent, MeasureTheory.Content.mk_apply
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
K : Set X
hK : IsCompact K
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ K
apply :
  ∀ (ε : ℝ≥0),
    0 < ε → (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X } + ε
⊢ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X }

Tactic:
apply le_iff_forall_pos_le_add.mpr

Premises used: Iff.mpr, le_iff_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
K : Set X
hK : IsCompact K
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ K
ε : ℝ≥0
hε : 0 < ε
obtain :
  ∀ (g : X →C_c ℝ≥0)
    (hg :
      (∀ x ∈ { carrier := K, isCompact' := hK : Compacts X },
          LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
        (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) g < rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X } + ε),
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X } + ε
⊢ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X } + ε

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

Premises used: TopologicalSpace.Compacts.mk, exists_lt_rieszContentAux_add_pos
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
K : Set X
hK : IsCompact K
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK : Compacts X }, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) g < rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X } + ε
apply : LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) g : ℝ≥0)
⊢ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X } + ε

Tactic:
apply le_trans _ hg.2.le

Premises used: LT.lt.le, And.right, le_trans