awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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 < α
⊢ b.toNNReal ≤ HMul.hMul (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f : ℝ≥0) α
have rw : b.toNNReal ≤ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (α • f)
Tactic: rw [mul_comm, ← smul_eq_mul, ← map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
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 α⁻¹
⊢ b.toNNReal ≤ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (α • f)
have hKK' : (↑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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
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'
⊢ b.toNNReal ≤ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (α • f)
have hK'cp : 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'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
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∞) :=
  ⋯
⊢ b.toNNReal ≤ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (α • f)
have hb'₁ : ∀ (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'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤ ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) K
have rw : (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
  ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (↑{ carrier := K, isCompact' := hK : Compacts X } : Set X)
Tactic: rw [← TopologicalSpace.Compacts.coe_mk K hK]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (↑{ carrier := K, isCompact' := hK : Compacts X } : Set X)
have simp : (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
  (rieszContent Λ : (a : Compacts X) → ℝ≥0∞) { carrier := K, isCompact' := hK }
Tactic: simp only [rieszMeasure, Content.measure_eq_content_of_regular (rieszContent Λ)
    (contentRegular_rieszContent Λ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
    (rieszContent Λ : (a : Compacts X) → ℝ≥0∞) { carrier := K, isCompact' := hK }
have simp : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X }
Tactic: simp only [rieszContent, ENNReal.coe_le_coe, Content.mk_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
⊢ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X }
have apply : ∀ (ε : ℝ≥0),
  0 < ε → (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X } + ε
Tactic: apply le_iff_forall_pos_le_add.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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 < ε
⊢ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X } + ε
have 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 } + ε
Tactic: obtain ⟨g, hg⟩ := exists_lt_rieszContentAux_add_pos Λ ⟨K, hK⟩ hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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 } + ε
⊢ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f ≤ rieszContentAux Λ { carrier := K, isCompact' := hK : Compacts X } + ε
have apply : LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) g : ℝ≥0)
Tactic: apply le_trans _ hg.2.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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 } + ε
⊢ LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) g : ℝ≥0)
have a : f ≤ g
Tactic: apply monotone_of_nnreal Λ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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 } + ε
x : X
⊢ LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
have pos : ∀ (hx : Membership.mem (γ := Set X) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x),
  LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: by_cases hx : x ∈ tsupport f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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 } + ε
x : X
pos :
  ∀ (hx : Membership.mem (γ := Set X) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x),
    LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
have neg : ∀ (hx : x ∉ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)),
  LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: by_cases hx : x ∈ tsupport f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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 } + ε
x : X
hx : x ∉ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
⊢ LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
have neg : LE.le (α := ℝ≥0) (0 : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: rw [image_eq_zero_of_notMem_tsupport hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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)
V : Set X
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ V
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤ ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) V
have apply : (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
  ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))
Tactic: apply le_trans _ (measure_mono h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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)
V : Set X
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ V
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))
have apply : Subset (α := Set X) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))
Tactic: apply le_rieszMeasure_of_isCompact_tsupport_subset Λ hf f.hasCompactSupport
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ ∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ENNReal) ∂rieszMeasure Λ = (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ENNReal)
have rw : (↑(Real.toNNReal (@integral _ _ _ _ inst_3 (rieszMeasure Λ) fun (a : X) ↦ (↑((f : (a : X) → ℝ≥0) a) : ℝ))) : ENNReal) =
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ENNReal)
Tactic: rw [lintegral_coe_eq_integral, ← ENNReal.ofNNReal_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
rw :
  (↑(Real.toNNReal (@integral _ _ _ _ inst_3 (rieszMeasure Λ) fun (a : X) ↦ (↑((f : (a : X) → ℝ≥0) a) : ℝ))) :
      ENNReal) =
    (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ENNReal)
⊢ ∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ENNReal) ∂rieszMeasure Λ = (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ENNReal)
have hfi : @Integrable ℝ _ _ _ inst_3 (fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)) (rieszMeasure Λ)
Tactic: rw [lintegral_coe_eq_integral, ← ENNReal.ofNNReal_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ (↑(Real.toNNReal (@integral _ _ _ _ inst_3 (rieszMeasure Λ) fun (a : X) ↦ (↑((f : (a : X) → ℝ≥0) a) : ℝ))) :
      ENNReal) =
    (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ENNReal)
have rw : (@integral _ _ _ _ inst_3 (rieszMeasure Λ) fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)) =
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ)
Tactic: rw [ENNReal.coe_inj, Real.toNNReal_of_nonneg (MeasureTheory.integral_nonneg (by intro a; simp)),
       NNReal.eq_iff, NNReal.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
μ ν : Measure X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν :
  ∀ (f : X →C_c ℝ≥0),
    Eq (α := ℝ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂ν)
⊢ μ = ν
have hμν₁ : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
Tactic: apply Measure.ext_of_integral_eq_on_compactlySupported
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
μ ν : Measure X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν :
  ∀ (f : X →C_c ℝ≥0),
    Eq (α := ℝ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂ν)
f : X →C_c ℝ
⊢ Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
have hμν₁ : HSub.hSub (α := ℝ) (∫ (a : X), (↑(Real.toNNReal ((f : (a : X) → ℝ) a)) : ℝ) ∂μ)
    (∫ (a : X), (↑(Real.toNNReal (-(f : (a : X) → ℝ) a)) : ℝ) ∂μ) =
  ∫ (x : X), (f : (a : X) → ℝ) x ∂ν
Tactic: rw [integral_eq_integral_pos_part_sub_integral_neg_part f.integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
μ ν : Measure X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν :
  ∀ (f : X →C_c ℝ≥0),
    Eq (α := ℝ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂ν)
f : X →C_c ℝ
⊢ HSub.hSub (α := ℝ) (∫ (a : X), (↑(Real.toNNReal ((f : (a : X) → ℝ) a)) : ℝ) ∂μ)
      (∫ (a : X), (↑(Real.toNNReal (-(f : (a : X) → ℝ) a)) : ℝ) ∂μ) =
    ∫ (x : X), (f : (a : X) → ℝ) x ∂ν
have hμν₁ : HSub.hSub (α := ℝ) (∫ (a : X), (↑(Real.toNNReal ((f : (a : X) → ℝ) a)) : ℝ) ∂μ)
    (∫ (a : X), (↑(Real.toNNReal (-(f : (a : X) → ℝ) a)) : ℝ) ∂μ) =
  HSub.hSub (α := ℝ) (∫ (a : X), (↑(Real.toNNReal ((f : (a : X) → ℝ) a)) : ℝ) ∂ν)
    (∫ (a : X), (↑(Real.toNNReal (-(f : (a : X) → ℝ) a)) : ℝ) ∂ν)
Tactic: rw [integral_eq_integral_pos_part_sub_integral_neg_part f.integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
μ ν : Measure X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν :
  ∀ (f : X →C_c ℝ≥0),
    Eq (α := ℝ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂ν)
f : X →C_c ℝ
⊢ Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
have hμν₁ : HSub.hSub (α := ℝ) (∫ (a : X), (↑(Real.toNNReal ((f : (a : X) → ℝ) a)) : ℝ) ∂μ)
    (∫ (a : X), (↑(Real.toNNReal (-(f : (a : X) → ℝ) a)) : ℝ) ∂μ) =
  HSub.hSub (α := ℝ) (∫ (a : X), (↑(Real.toNNReal ((f : (a : X) → ℝ) a)) : ℝ) ∂ν)
    (∫ (a : X), (↑(Real.toNNReal (-(f : (a : X) → ℝ) a)) : ℝ) ∂ν)
Tactic: repeat rw [integral_eq_integral_pos_part_sub_integral_neg_part f.integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
μ ν : Measure X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν :
  ∀ (f : X →C_c ℝ≥0),
    Eq (α := ℝ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂ν)
f : X →C_c ℝ
⊢ HSub.hSub (α := ℝ) (∫ (a : X), (↑(Real.toNNReal ((f : (a : X) → ℝ) a)) : ℝ) ∂μ)
      (∫ (a : X), (↑(Real.toNNReal (-(f : (a : X) → ℝ) a)) : ℝ) ∂μ) =
    HSub.hSub (α := ℝ) (∫ (a : X), (↑(Real.toNNReal ((f : (a : X) → ℝ) a)) : ℝ) ∂ν)
      (∫ (a : X), (↑(Real.toNNReal (-(f : (a : X) → ℝ) a)) : ℝ) ∂ν)
have hμν₁ : HSub.hSub (α := ℝ) (∫ (x : X), (↑((f.nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂ν)
    (∫ (x : X), (↑(((-f).nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂ν) =
  HSub.hSub (α := ℝ) (∫ (a : X), (↑(Real.toNNReal ((f : (a : X) → ℝ) a)) : ℝ) ∂ν)
    (∫ (a : X), (↑(Real.toNNReal (-(f : (a : X) → ℝ) a)) : ℝ) ∂ν)
Tactic: erw [hμν f.nnrealPart, hμν (-f).nnrealPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
⊢ integralLinearMap (rieszMeasure Λ) = Λ
have h : ∀ (x : X →C_c ℝ≥0),
  (↑(((integralLinearMap (rieszMeasure Λ) : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) : (a : X →C_c ℝ≥0) → ℝ≥0) x) : ℝ) =
    (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) x) : ℝ)
Tactic: ext
-- 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
⊢ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) ≤ ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) V
have apply : ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) ≤
  ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ))
Tactic: apply le_trans _ (measure_mono hV)
-- 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
⊢ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ))
have this : Eq (α := ℝ≥0∞)
  ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞)
      (↑{ carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := sorry : Compacts X } : Set X) :
    ℝ≥0∞)
  ((rieszContent (toNNRealLinear Λ) : (a : Compacts X) → ℝ≥0∞)
      { carrier := tsupport (α := ℝ) (⇑f : (a : X) → ℝ), isCompact' := sorry } :
    ℝ≥0∞)
Tactic: have := Content.measure_eq_content_of_regular (rieszContent (toNNRealLinear Λ))
    (contentRegular_rieszContent (toNNRealLinear Λ)) (⟨tsupport f, f.hasCompactSupport⟩)