awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
V : Set X
hV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
this :
  Eq (α := ℝ≥0∞)
    ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
        (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } : Set X) :
      ℝ≥0∞)
    ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ } :
      ℝ≥0∞)
rw :
  NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
    rieszContentAux (toNNRealLinear Λ) { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ }
⊢ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ))

Tactic:
rw [← Compacts.coe_mk (tsupport f) f.hasCompactSupport, rieszMeasure, this, rieszContent,
    ENNReal.ofReal_eq_coe_nnreal (Λ.map_nonneg fun x ↦ (hf x).1), Content.mk_apply,
    ENNReal.coe_le_coe]

Premises used: CompactlySupportedContinuousMap.hasCompactSupport, RealRMK.rieszMeasure, PositiveLinearMap.map_nonneg, ENNReal.coe_le_coe, tsupport, TopologicalSpace.Compacts.coe_mk, rieszContent, MeasureTheory.Content.mk_apply, And.left, ENNReal.ofReal_eq_coe_nnreal, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
V : Set X
hV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
this :
  Eq (α := ℝ≥0∞)
    ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
        (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } : Set X) :
      ℝ≥0∞)
    ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ } :
      ℝ≥0∞)
apply :
  ∀ (ε : NNReal),
    0 < ε →
      NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
        rieszContentAux (toNNRealLinear Λ)
            { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
          ε
⊢ NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
    rieszContentAux (toNNRealLinear Λ) { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ }

Tactic:
apply le_iff_forall_pos_le_add.mpr

Premises used: Iff.mpr, le_iff_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
V : Set X
hV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
this :
  Eq (α := ℝ≥0∞)
    ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
        (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } : Set X) :
      ℝ≥0∞)
    ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ } :
      ℝ≥0∞)
ε : NNReal
hε : 0 < ε
obtain :
  ∀ (g : X →C_c NNReal)
    (hg :
      (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X },
          LE.le (α := NNReal) (1 : NNReal) ((g : (a : X) → NNReal) x : NNReal)) ∧
        (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) g <
          rieszContentAux (toNNRealLinear Λ)
              { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
            (↑ε : ℝ).toNNReal),
    NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
      rieszContentAux (toNNRealLinear Λ)
          { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
        ε
⊢ NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
    rieszContentAux (toNNRealLinear Λ)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
      ε

Tactic:
obtain ⟨g, hg⟩ := exists_lt_rieszContentAux_add_pos (toNNRealLinear Λ)
    ⟨tsupport f, f.hasCompactSupport⟩ (Real.toNNReal_pos.mpr hε)

Premises used: Iff.mpr, CompactlySupportedContinuousMap.hasCompactSupport, tsupport, CompactlySupportedContinuousMap.toNNRealLinear, Real.toNNReal_pos, TopologicalSpace.Compacts.mk, exists_lt_rieszContentAux_add_pos, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
V : Set X
hV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
this :
  Eq (α := ℝ≥0∞)
    ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
        (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } : Set X) :
      ℝ≥0∞)
    ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ } :
      ℝ≥0∞)
ε : NNReal
hε : 0 < ε
g : X →C_c NNReal
hg :
  (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X },
      LE.le (α := NNReal) (1 : NNReal) ((g : (a : X) → NNReal) x : NNReal)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) g <
      rieszContentAux (toNNRealLinear Λ)
          { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
        (↑ε : ℝ).toNNReal
⊢ (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X },
      LE.le (α := NNReal) (1 : NNReal) ((g : (a : X) → NNReal) x : NNReal)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) g <
      rieszContentAux (toNNRealLinear Λ)
          { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
        ε

Tactic:
simp_rw [NNReal.val_eq_coe, Real.toNNReal_coe] at hg

Premises used: NNReal.val_eq_coe, Real.toNNReal_coe
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
V : Set X
hV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
this :
  Eq (α := ℝ≥0∞)
    ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
        (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } : Set X) :
      ℝ≥0∞)
    ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ } :
      ℝ≥0∞)
ε : NNReal
hε : 0 < ε
g : X →C_c NNReal
hg :
  (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X },
      LE.le (α := NNReal) (1 : NNReal) ((g : (a : X) → NNReal) x : NNReal)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) g <
      rieszContentAux (toNNRealLinear Λ)
          { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
        ε
⊢ NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
    rieszContentAux (toNNRealLinear Λ)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
      ε

Tactic:
(Λ.mono ?_).trans hg.2.le

Premises used: LT.lt.le, OrderHom.mono, And.right, PositiveLinearMap.toOrderHom, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
V : Set X
hV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
this :
  Eq (α := ℝ≥0∞)
    ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
        (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } : Set X) :
      ℝ≥0∞)
    ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ } :
      ℝ≥0∞)
ε : NNReal
hε : 0 < ε
g : X →C_c NNReal
hg :
  (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X },
      LE.le (α := NNReal) (1 : NNReal) ((g : (a : X) → NNReal) x : NNReal)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) g <
      rieszContentAux (toNNRealLinear Λ)
          { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
        ε
refine : f ≤ (toRealLinearMap : (a : X →C_c NNReal) → X →C_c ℝ) g
⊢ NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
    rieszContentAux (toNNRealLinear Λ)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
      ε

Tactic:
refine (Λ.mono ?_).trans hg.2.le

Premises used: LT.lt.le, OrderHom.mono, And.right, PositiveLinearMap.toOrderHom, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
V : Set X
hV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
this :
  Eq (α := ℝ≥0∞)
    ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
        (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } : Set X) :
      ℝ≥0∞)
    ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ } :
      ℝ≥0∞)
ε : NNReal
hε : 0 < ε
g : X →C_c NNReal
hg :
  (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X },
      LE.le (α := NNReal) (1 : NNReal) ((g : (a : X) → NNReal) x : NNReal)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) g <
      rieszContentAux (toNNRealLinear Λ)
          { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
        ε
x : X
pos :
  ∀ (hx : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x),
    LE.le (α := (fun (a : X) ↦ ℝ) x) ((f : (a : X) → ℝ) x : ℝ)
      ((((toRealLinearMap : (a : X →C_c NNReal) → X →C_c ℝ) g : X →C_c ℝ) : (a : X) → ℝ) x : ℝ)
neg :
  ∀ (hx : x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)),
    LE.le (α := (fun (a : X) ↦ ℝ) x) ((f : (a : X) → ℝ) x : ℝ)
      ((((toRealLinearMap : (a : X →C_c NNReal) → X →C_c ℝ) g : X →C_c ℝ) : (a : X) → ℝ) x : ℝ)
⊢ LE.le (α := (fun (a : X) ↦ ℝ) x) ((f : (a : X) → ℝ) x : ℝ)
    ((((toRealLinearMap : (a : X →C_c NNReal) → X →C_c ℝ) g : X →C_c ℝ) : (a : X) → ℝ) x : ℝ)

Tactic:
by_cases hx : x ∈ tsupport f

Premises used: tsupport, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
V : Set X
hV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
this :
  Eq (α := ℝ≥0∞)
    ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
        (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } : Set X) :
      ℝ≥0∞)
    ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ } :
      ℝ≥0∞)
ε : NNReal
hε : 0 < ε
g : X →C_c NNReal
hg :
  (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X },
      LE.le (α := NNReal) (1 : NNReal) ((g : (a : X) → NNReal) x : NNReal)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) g <
      rieszContentAux (toNNRealLinear Λ)
          { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
        ε
x : X
hx : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
⊢ LE.le (α := (fun (a : X) ↦ ℝ) x) ((f : (a : X) → ℝ) x : ℝ)
    ((((toRealLinearMap : (a : X →C_c NNReal) → X →C_c ℝ) g : X →C_c ℝ) : (a : X) → ℝ) x : ℝ)

Tactic:
simpa using le_trans (hf x).2 (hg.1 x hx)

Premises used: And.right, And.left, le_trans
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ) ∧ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
V : Set X
hV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
this :
  Eq (α := ℝ≥0∞)
    ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
        (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } : Set X) :
      ℝ≥0∞)
    ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ } :
      ℝ≥0∞)
ε : NNReal
hε : 0 < ε
g : X →C_c NNReal
hg :
  (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X },
      LE.le (α := NNReal) (1 : NNReal) ((g : (a : X) → NNReal) x : NNReal)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) g <
      rieszContentAux (toNNRealLinear Λ)
          { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
        ε
x : X
hx : x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
⊢ LE.le (α := (fun (a : X) ↦ ℝ) x) ((f : (a : X) → ℝ) x : ℝ)
    ((((toRealLinearMap : (a : X →C_c NNReal) → X →C_c ℝ) g : X →C_c ℝ) : (a : X) → ℝ) x : ℝ)

Tactic:
simp [image_eq_zero_of_notMem_tsupport hx]

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
rw :
  (rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞) { carrier := K, isCompact' := hK } ≤
    ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f)
⊢ ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) K ≤ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f)

Tactic:
rw [← Compacts.coe_mk K hK, rieszMeasure,
    Content.measure_eq_content_of_regular _ (contentRegular_rieszContent (toNNRealLinear Λ))]

Premises used: RealRMK.rieszMeasure, MeasureTheory.Content.measure_eq_content_of_regular, CompactlySupportedContinuousMap.toNNRealLinear, TopologicalSpace.Compacts.coe_mk, contentRegular_rieszContent
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
apply :
  ∀ (p : NNReal),
    ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) = (↑p : ℝ≥0∞) →
      (rieszContent (toNNRealLinear Λ)).toFun { carrier := K, isCompact' := hK : Compacts X } ≤ p
⊢ (rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞) { carrier := K, isCompact' := hK } ≤
    ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f)

Tactic:
apply ENNReal.coe_le_iff.mpr

Premises used: Iff.mpr, ENNReal.coe_le_iff
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) = (↑p : ℝ≥0∞)
⊢ (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)

Tactic:
rw [← ENNReal.ofReal_coe_nnreal,
    ENNReal.ofReal_eq_ofReal_iff (Λ.map_nonneg hf) NNReal.zero_le_coe] at hp

Premises used: PositiveLinearMap.map_nonneg, ENNReal.ofReal_eq_ofReal_iff, ENNReal.ofReal_coe_nnreal, NNReal.zero_le_coe
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
h :
  Membership.mem (γ := Set NNReal)
    (image (α := X →C_c NNReal) (⇑(toNNRealLinear Λ) : (a : X →C_c NNReal) → NNReal)
      {f : X →C_c NNReal |
        ∀ x ∈ { carrier := K, isCompact' := hK : Compacts X },
          LE.le (α := NNReal) (1 : NNReal) ((f : (a : X) → NNReal) x : NNReal)})
    p
⊢ (rieszContent (toNNRealLinear Λ)).toFun { carrier := K, isCompact' := hK : Compacts X } ≤ p

Tactic:
apply csInf_le'

Premises used: csInf_le'
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
h :
  Membership.mem (γ := Set (X →C_c NNReal))
      {f : X →C_c NNReal |
        ∀ x ∈ { carrier := K, isCompact' := hK : Compacts X },
          LE.le (α := NNReal) (1 : NNReal) ((f : (a : X) → NNReal) x : NNReal)}
      f.nnrealPart ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart = p
⊢ ∃ (x : X →C_c NNReal),
    Membership.mem (γ := Set (X →C_c NNReal))
        {f : X →C_c NNReal |
          ∀ x ∈ { carrier := K, isCompact' := hK : Compacts X },
            LE.le (α := NNReal) (1 : NNReal) ((f : (a : X) → NNReal) x : NNReal)}
        x ∧
      (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) x = p

Tactic:
use f.nnrealPart

Premises used: CompactlySupportedContinuousMap.nnrealPart
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
h :
  (∀ x ∈ { carrier := K, isCompact' := hK : Compacts X }, LE.le (α := ℝ) (1 : ℝ) ((f : (a : X) → ℝ) x : ℝ)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart = p
⊢ Membership.mem (γ := Set (X →C_c NNReal))
      {f : X →C_c NNReal |
        ∀ x ∈ { carrier := K, isCompact' := hK : Compacts X },
          LE.le (α := NNReal) (1 : NNReal) ((f : (a : X) → NNReal) x : NNReal)}
      f.nnrealPart ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart = p

Tactic:
simp_rw [Set.mem_setOf_eq, nnrealPart_apply, Real.one_le_toNNReal]

Premises used: Set.mem_setOf_eq, Real.one_le_toNNReal, CompactlySupportedContinuousMap.nnrealPart_apply
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
⊢ (∀ x ∈ { carrier := K, isCompact' := hK : Compacts X }, LE.le (α := ℝ) (1 : ℝ) ((f : (a : X) → ℝ) x : ℝ)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart = p

Tactic:
⟨(fun x hx ↦ Eq.ge (hfK x hx)), ?_⟩

Premises used: Eq.ge, And.intro
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
h : (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart = p
⊢ (∀ x ∈ { carrier := K, isCompact' := hK : Compacts X }, LE.le (α := ℝ) (1 : ℝ) ((f : (a : X) → ℝ) x : ℝ)) ∧
    (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart = p

Tactic:
refine ⟨(fun x hx ↦ Eq.ge (hfK x hx)), ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
h : (↑((toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart) : ℝ) = (↑p : ℝ)
⊢ (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart = p

Tactic:
apply NNReal.eq

Premises used: NNReal.eq
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
h : ∀ (z : X), Eq (α := ℝ) ((f.nnrealPart.toReal : (a : X) → ℝ) z : ℝ) ((f : (a : X) → ℝ) z : ℝ)
⊢ f.nnrealPart.toReal = f

Tactic:
ext z
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
z : X
⊢ Eq (α := ℝ) ((f.nnrealPart.toReal : (a : X) → ℝ) z : ℝ) ((f : (a : X) → ℝ) z : ℝ)

Tactic:
simp [hf z]