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
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 : f ≤ g
⊢ LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) g : ℝ≥0)

Tactic:
apply monotone_of_nnreal Λ

Premises used: CompactlySupportedContinuousMap.monotone_of_nnreal
-- 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 } + ε
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)
neg :
  ∀ (hx : x ∉ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)),
    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)

Tactic:
by_cases hx : x ∈ tsupport f

Premises used: tsupport, DFunLike.coe
-- 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 } + ε
x : X
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:
le_trans (hf x) (hg.1 x (Set.mem_of_subset_of_mem h hx))

Premises used: Set.mem_of_subset_of_mem, And.left, 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
ε : ℝ≥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 : 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:
exact le_trans (hf x) (hg.1 x (Set.mem_of_subset_of_mem h hx))

Premises used: Set.mem_of_subset_of_mem, And.left, 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
ε : ℝ≥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)
neg : LE.le (α := ℝ≥0) (0 : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ LE.le (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
rw [image_eq_zero_of_notMem_tsupport hx]

Premises used: image_eq_zero_of_notMem_tsupport
-- 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 } + ε
x : X
hx : x ∉ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
⊢ LE.le (α := ℝ≥0) (0 : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
zero_le

Premises used: zero_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
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) (0 : ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
exact zero_le

Premises used: zero_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
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
apply :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤ ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) V

Tactic:
apply le_trans _ (measure_mono h)

Premises used: MeasureTheory.measure_mono, 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)
V : Set X
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ V
apply : Subset (α := Set X) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))
⊢ (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ≥0∞) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))

Tactic:
apply le_rieszMeasure_of_isCompact_tsupport_subset Λ hf f.hasCompactSupport

Premises used: CompactlySupportedContinuousMap.hasCompactSupport, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset
-- 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)
V : Set X
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ V
⊢ Subset (α := Set X) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))

Tactic:
subset_rfl

Premises used: subset_rfl
-- 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)
V : Set X
h : tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0) ⊆ V
⊢ Subset (α := Set X) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))

Tactic:
exact subset_rfl

Premises used: subset_rfl
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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)
hfi : @Integrable ℝ _ _ _ inst_3 (fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)) (rieszMeasure Λ)
⊢ ∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ENNReal) ∂rieszMeasure Λ = (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ENNReal)

Tactic:
rw [lintegral_coe_eq_integral, ← ENNReal.ofNNReal_toNNReal]

Premises used: ENNReal.ofNNReal_toNNReal, MeasureTheory.lintegral_coe_eq_integral
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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
a : X
⊢ LE.le (α := (fun (a : X) ↦ ℝ) a) (0 a) ((fun (a : X) ↦ (↑((f : (a : X) → ℝ≥0) a) : ℝ)) a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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 :
  (@integral _ _ _ _ inst_3 (rieszMeasure Λ) fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)) =
    (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ)
⊢ (↑(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 [ENNReal.coe_inj, Real.toNNReal_of_nonneg (MeasureTheory.integral_nonneg (by intro a; simp)),
       NNReal.eq_iff, NNReal.coe_mk]

Premises used: MeasureTheory.integral_nonneg, ENNReal.coe_inj, NNReal.coe_mk, NNReal.eq_iff, Real.toNNReal_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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
⊢ (@integral _ _ _ _ inst_3 (rieszMeasure Λ) fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)) =
    (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ)

Tactic:
integral_rieszMeasure Λ f

Premises used: NNRealRMK.integral_rieszMeasure
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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
⊢ (@integral _ _ _ _ inst_3 (rieszMeasure Λ) fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)) =
    (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ)

Tactic:
exact integral_rieszMeasure Λ f

Premises used: NNRealRMK.integral_rieszMeasure
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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
⊢ Continuous (Y := ℝ) fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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
⊢ @Integrable ℝ _ _ _ inst_3 (fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)) (rieszContent Λ).measure

Tactic:
exact Continuous.integrable_of_hasCompactSupport (by fun_prop)
    (HasCompactSupport.comp_left f.hasCompactSupport rfl)

Premises used: CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integrable_of_hasCompactSupport, HasCompactSupport.comp_left
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
Λ_1 Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
⊢ Measure.Regular (rieszMeasure Λ)

Tactic:
(rieszContent Λ).regular

Premises used: MeasureTheory.Content.regular, NNRealRMK.rieszMeasure, rieszContent
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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) : ℝ) ∂ν)
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

Premises used: MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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 ℝ
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 ∂ν
⊢ Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)

Tactic:
rw [integral_eq_integral_pos_part_sub_integral_neg_part f.integrable]

Premises used: MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part, CompactlySupportedContinuousMap.integrable
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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 ℝ
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)) : ℝ) ∂ν)
⊢ 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]

Premises used: MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part, CompactlySupportedContinuousMap.integrable
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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 ℝ
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)) : ℝ) ∂ν)
⊢ Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)

Tactic:
repeat rw [integral_eq_integral_pos_part_sub_integral_neg_part f.integrable]

Premises used: MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part, CompactlySupportedContinuousMap.integrable
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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 ℝ
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)) : ℝ) ∂ν)
⊢ 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:
erw [hμν f.nnrealPart, hμν (-f).nnrealPart]

Premises used: CompactlySupportedContinuousMap.nnrealPart, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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 (α := ℝ) (∫ (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:
rfl
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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μν : Eq (α := (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) (integralLinearMap μ) (integralLinearMap ν)
f : X →C_c ℝ≥0
⊢ Eq (α := ℝ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ) (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂ν)

Tactic:
simpa using congr(($hμν f).toReal)
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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 : μ = ν
⊢ Eq (α := (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) (integralLinearMap μ) (integralLinearMap ν)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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
⊢ ∀ (f : X →C_c ℝ≥0),
    Eq (α := ℝ)
      (@integral _ _ _ _ inst_3 (rieszMeasure (integralLinearMap μ)) fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ))
      (∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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
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) : ℝ)
⊢ integralLinearMap (rieszMeasure Λ) = Λ

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
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
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:
simp
-- 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
apply :
  ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) ≤
    ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ))
⊢ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) f) ≤ ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) V

Tactic:
apply le_trans _ (measure_mono hV)

Premises used: MeasureTheory.measure_mono, 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
⊢ 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∞)

Tactic:
have := Content.measure_eq_content_of_regular (rieszContent (toNNRealLinear Λ))
    (contentRegular_rieszContent (toNNRealLinear Λ)) (⟨tsupport f, f.hasCompactSupport⟩)