awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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∞)
⊢ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ))
have rw : NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) sorry ≤
  rieszContentAux (toNNRealLinear Λ) { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := sorry }
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
    rieszContentAux (toNNRealLinear Λ) { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ }
have apply : ∀ (ε : NNReal),
  0 < ε →
    NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) sorry ≤
      rieszContentAux (toNNRealLinear Λ)
          { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := sorry : Compacts X } +
        ε
Tactic: apply le_iff_forall_pos_le_add.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 < ε
⊢ NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
    rieszContentAux (toNNRealLinear Λ)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
      ε
have obtain : ∀ (g : X →C_c NNReal)
  (hg :
    (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := sorry : 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' := sorry : Compacts X } +
          (↑ε : ℝ).toNNReal),
  NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) sorry ≤
    rieszContentAux (toNNRealLinear Λ)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := sorry : Compacts X } +
      ε
Tactic: obtain ⟨g, hg⟩ := exists_lt_rieszContentAux_add_pos (toNNRealLinear Λ)
    ⟨tsupport f, f.hasCompactSupport⟩ (Real.toNNReal_pos.mpr hε)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
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
⊢ NNReal.mk ((Λ : (a : X →C_c ℝ) → ℝ) f) ⋯ ≤
    rieszContentAux (toNNRealLinear Λ)
        { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := ⋯ : Compacts X } +
      ε
have hg₁ : (∀ x ∈ { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := sorry : 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' := sorry : Compacts X } +
      ε
Tactic: simp_rw [NNReal.val_eq_coe, Real.toNNReal_coe] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 } +
      ε
have refine : f ≤ (toRealLinearMap : (a : X →C_c NNReal) → X →C_c ℝ) g
Tactic: refine (Λ.mono ?_).trans hg.2.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ 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 : ℝ)
have 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 : ℝ)
Tactic: by_cases hx : x ∈ tsupport f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : ℝ)
⊢ 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 : ℝ)
have 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 : ℝ)
Tactic: by_cases hx : x ∈ tsupport f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : ℝ)
⊢ ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) K ≤ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f)
have rw : (rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞) { carrier := K, isCompact' := hK } ≤
  ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f)
Tactic: rw [← Compacts.coe_mk K hK, rieszMeasure,
    Content.measure_eq_content_of_regular _ (contentRegular_rieszContent (toNNRealLinear Λ))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : ℝ)
⊢ (rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞) { carrier := K, isCompact' := hK } ≤
    ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f)
have apply : ∀ (p : NNReal),
  ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) = (↑p : ℝ≥0∞) →
    (rieszContent (toNNRealLinear Λ)).toFun { carrier := K, isCompact' := hK : Compacts X } ≤ p
Tactic: apply ENNReal.coe_le_iff.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
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∞)
⊢ (rieszContent (toNNRealLinear Λ)).toFun { carrier := K, isCompact' := hK : Compacts X } ≤ p
have hp₁ : (Λ : (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
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : ℝ)
⊢ (rieszContent (toNNRealLinear Λ)).toFun { carrier := K, isCompact' := hK : Compacts X } ≤ p
have 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
Tactic: apply csInf_le'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : 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
have 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
Tactic: use f.nnrealPart
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : ℝ)
⊢ 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
have 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
Tactic: simp_rw [Set.mem_setOf_eq, nnrealPart_apply, Real.one_le_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
have h : (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart = p
Tactic: refine ⟨(fun x hx ↦ Eq.ge (hfK x hx)), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : ℝ)
⊢ (toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart = p
have h : (↑((toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart) : ℝ) = (↑p : ℝ)
Tactic: apply NNReal.eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : ℝ)
⊢ f.nnrealPart.toReal = f
have h : ∀ (z : X), Eq (α := ℝ) ((f.nnrealPart.toReal : (a : X) → ℝ) z : ℝ) ((f : (a : X) → ℝ) z : ℝ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : ℝ)
⊢ (↑((toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart) : ℝ) = (↑p : ℝ)
have h : (Λ : (a : X →C_c ℝ) → ℝ) f.nnrealPart.toReal = (↑p : ℝ)
Tactic: rw [toNNRealLinear_apply, show f.nnrealPart.toReal = f by ext z; simp [hf z], hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : (Λ : (a : X →C_c ℝ) → ℝ) f.nnrealPart.toReal = (↑p : ℝ)
h₁ : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
⊢ (↑((toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart) : ℝ) = (↑p : ℝ)
have h₂ : (↑p : ℝ) = (↑p : ℝ)
Tactic: rw [toNNRealLinear_apply, show f.nnrealPart.toReal = f by ext z; simp [hf z], hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
n m : Fin N
h : n < m
⊢ HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 ≤ (↑(↑m : ℕ) : ℝ)
have norm_cast : (↑n : ℕ) + 1 ≤ (↑m : ℕ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
n m : Fin N
h : n < m
⊢ a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + ε * HAdd.hAdd (α := ℝ) (↑(↑m : ℕ) : ℝ) 1
have rw : a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + (ε * (↑(↑m : ℕ) : ℝ) + ε * 1)
Tactic: rw [mul_add, mul_one, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
n m : Fin N
h : n < m
rw : a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + (ε * (↑(↑m : ℕ) : ℝ) + ε * 1)
⊢ a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + ε * HAdd.hAdd (α := ℝ) (↑(↑m : ℕ) : ℝ) 1
have rw₁ : a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + (ε * (↑(↑m : ℕ) : ℝ) + ε)
Tactic: rw [mul_add, mul_one, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
n m : Fin N
h : n < m
rw : a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + (ε * (↑(↑m : ℕ) : ℝ) + ε * 1)
rw₁ : a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + (ε * (↑(↑m : ℕ) : ℝ) + ε)
⊢ a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + ε * HAdd.hAdd (α := ℝ) (↑(↑m : ℕ) : ℝ) 1
have rw₂ : a + (ε * (↑(↑m : ℕ) : ℝ) + ε) = a + (ε * (↑(↑m : ℕ) : ℝ) + ε)
Tactic: rw [mul_add, mul_one, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
⊢ ∃ (E : Fin N → Set X),
    Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
      PairwiseDisjoint univ E ∧
        (∀ (n : Fin N),
            ∀ x ∈ E n,
              a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
                (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
          ∀ (n : Fin N), MeasurableSet (E n)
have hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
Tactic: have hy {n m : Fin N} (h : n < m) : y n + ε ≤ y m := calc
    _ ≤ a + ε * m + ε := by
      exact add_le_add_three (by rfl) ((mul_le_mul_iff_of_pos_left hε).mpr (by norm_cast)) (by rfl)
    _ = _ := by dsimp [y]; rw [mul_add, mul_one, add_assoc]