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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ Integrable (ε := ℝ) (V.indicator 1) ν

Tactic:
exact IntegrableOn.integrable_indicator integrableOn_const pV2.measurableSet

Premises used: MeasureTheory.IntegrableOn.integrable_indicator, IsOpen.measurableSet, MeasureTheory.integrableOn_const
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
ha : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
hb : HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≠ ∞
ha₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hb₁ : (↑ε : ℝ≥0∞) ≠ ∞
⊢ ∫ (x : X), V.indicator 1 x ∂ν ≤ ENNReal.toReal ((ν : (a : Set X) → ℝ≥0∞) K) + (↑ε : ℝ)

Tactic:
rwa [integral_indicator_one pV2.measurableSet, measureReal_def,
        ← ENNReal.coe_toReal, ← ENNReal.toReal_add, ENNReal.toReal_le_toReal]

Premises used: ENNReal.toReal_add, ENNReal.coe_toReal, MeasureTheory.integral_indicator_one, IsOpen.measurableSet, MeasureTheory.measureReal_def, ENNReal.toReal_le_toReal
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞) ≠ ∞

Tactic:
finiteness
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ (↑ε : ℝ≥0∞) ≠ ∞

Tactic:
finiteness
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K₁ : LE.le (α := ℝ) (∫ (x : X), K.indicator 1 x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
K₂ : LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν) (∫ (x : X), V.indicator 1 x ∂ν)
K₃ : ∫ (x : X), V.indicator 1 x ∂ν ≤ ENNReal.toReal ((ν : (a : Set X) → ℝ≥0∞) K) + (↑ε : ℝ)
⊢ μ.real K ≤ ν.real K + (↑ε : ℝ)

Tactic:
calc
    μ.real K = ∫ x, K.indicator 1 x ∂μ := integral_indicator_one hK.measurableSet |>.symm
    _ ≤ ∫ x, f x ∂μ := by
      refine integral_mono ?_ f.integrable hfK
      exact (continuousOn_const.integrableOn_compact hK).integrable_indicator hK.measurableSet
    _ ≤ ∫ x, f x ∂ν := hμν f
    _ ≤ ∫ x, V.indicator 1 x ∂ν := by
      refine integral_mono f.integrable ?_ hfV
      exact IntegrableOn.integrable_indicator integrableOn_const pV2.measurableSet
    _ ≤ (ν K).toReal + ↑ε := by
      rwa [integral_indicator_one pV2.measurableSet, measureReal_def,
        ← ENNReal.coe_toReal, ← ENNReal.toReal_add, ENNReal.toReal_le_toReal]
      all_goals finiteness

Premises used: MeasureTheory.Measure.real, MeasureTheory.integral_indicator_one, ENNReal.toReal, Eq.symm, DFunLike.coe, IsCompact.measurableSet
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
hμν₁ :
  ∀ (U : Set X), IsOpen[inst] U → Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞)
⊢ μ = ν

Tactic:
apply Measure.OuterRegular.ext_isOpen

Premises used: MeasureTheory.Measure.OuterRegular.ext_isOpen
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
hμν₁ :
  ∀ (U : Set X), IsCompact U → Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞)
⊢ ∀ (U : Set X), IsOpen[inst] U → Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
apply Measure.InnerRegularWRT.eq_of_innerRegularWRT_of_forall_eq Measure.Regular.innerRegular
    Measure.Regular.innerRegular

Premises used: MeasureTheory.Measure.Regular.innerRegular, MeasureTheory.Measure.InnerRegularWRT.eq_of_innerRegularWRT_of_forall_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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
hμν₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)
hμν₂ : LE.le (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
measure_le_of_isCompact_of_integral (fun f ↦ (hμν f).le) hK

Premises used: RealRMK.measure_le_of_isCompact_of_integral, Eq.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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
exact measure_le_of_isCompact_of_integral (fun f ↦ (hμν f).le) hK

Premises used: RealRMK.measure_le_of_isCompact_of_integral, Eq.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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
measure_le_of_isCompact_of_integral (fun f ↦ (hμν f).ge) hK

Premises used: Eq.ge, RealRMK.measure_le_of_isCompact_of_integral
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
exact measure_le_of_isCompact_of_integral (fun f ↦ (hμν f).ge) hK

Premises used: Eq.ge, RealRMK.measure_le_of_isCompact_of_integral
-- 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
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
h : μ = ν
⊢ Eq (α := (X →C_c ℝ) →ₚ[ℝ] ℝ) (integralPositiveLinearMap μ) (integralPositiveLinearMap ν)

Tactic:
congr
-- 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
μ : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
⊢ ∀ (f : X →C_c ℝ),
    Eq (α := ℝ)
      (@integral _ _ _ _ inst_2 (rieszMeasure (integralPositiveLinearMap μ)) fun (x : X) ↦ (f : (a : X) → ℝ) x)
      (∫ (x : X), (f : (a : X) → ℝ) 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
h :
  ∀ (x : X →C_c ℝ),
    Eq (α := ℝ) ((integralPositiveLinearMap (rieszMeasure Λ) : (a : X →C_c ℝ) → ℝ) x : ℝ)
      ((Λ : (a : X →C_c ℝ) → ℝ) x : ℝ)
⊢ integralPositiveLinearMap (rieszMeasure Λ) = Λ

Tactic:
ext
-- 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
x : X →C_c ℝ
⊢ Eq (α := ℝ) ((integralPositiveLinearMap (rieszMeasure Λ) : (a : X →C_c ℝ) → ℝ) x : ℝ) ((Λ : (a : X →C_c ℝ) → ℝ) 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
Λ_1 : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : CompactSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
measure_univ_lt_top : LT.lt (α := ℝ≥0∞) (((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure (m0 := inst_2) (rieszMeasure Λ)

Tactic:
constructor
-- 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
Λ_1 : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : CompactSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
o : X →C_c ℝ := { toContinuousMap := 1, hasCompactSupport' := ⋯ }
⊢ ((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) univ ≤ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) o)

Tactic:
rieszMeasure_le_of_eq_one _ (fun x ↦ zero_le_one) isCompact_univ (fun x hx ↦ rfl)

Premises used: RealRMK.rieszMeasure_le_of_eq_one, isCompact_univ, rfl
-- 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
Λ_1 : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : CompactSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
o : X →C_c ℝ := { toContinuousMap := 1, hasCompactSupport' := ⋯ }
⊢ ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) o) < ∞

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
Λ_1 : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : CompactSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
o : X →C_c ℝ := { toContinuousMap := 1, hasCompactSupport' := ⋯ }
calc : ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) o) < ∞
⊢ LT.lt (α := ℝ≥0∞) (((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
calc rieszMeasure Λ univ
  _ ≤ ENNReal.ofReal (Λ o) :=
    rieszMeasure_le_of_eq_one _ (fun x ↦ zero_le_one) isCompact_univ (fun x hx ↦ rfl)
  _ < ⊤ := by simp

Premises used: RealRMK.rieszMeasure, ENNReal.ofReal, Set.univ, RealRMK.rieszMeasure_le_of_eq_one, isCompact_univ, 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
inst_4 : CompactSpace X
μ : Measure X
inst_5 : IsFiniteMeasure μ
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ :=
  { toFun := fun (g : X →C_c ℝ) ↦ ∫ (x : X), (g : (a : X) → ℝ) x ∂μ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
⊢ Measure.Regular (rieszMeasure Λ)

Tactic:
infer_instance
-- 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
inst_4 : CompactSpace X
μ : Measure X
inst_5 : IsFiniteMeasure μ
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ :=
  { toFun := fun (g : X →C_c ℝ) ↦ ∫ (x : X), (g : (a : X) → ℝ) x ∂μ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
⊢ IsFiniteMeasure (m0 := inst_2) (rieszMeasure Λ)

Tactic:
infer_instance
-- 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
inst_4 : CompactSpace X
μ : Measure X
inst_5 : IsFiniteMeasure μ
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ :=
  { toFun := fun (g : X →C_c ℝ) ↦ ∫ (x : X), (g : (a : X) → ℝ) x ∂μ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
refine :
  ∀ (g : X →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (g : (a : X) → ℝ) x)
⊢ ∃ (ν : Measure X),
    ν.Regular ∧
      IsFiniteMeasure ν ∧
        ∀ (g : X →ᵇ ℝ), Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ) (∫ (x : X), (g : (a : X) → ℝ) x ∂ν)

Tactic:
refine ⟨RealRMK.rieszMeasure Λ, by infer_instance, by infer_instance, fun g ↦ ?_⟩
-- 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
inst_4 : CompactSpace X
μ : Measure X
inst_5 : IsFiniteMeasure μ
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ :=
  { toFun := fun (g : X →C_c ℝ) ↦ ∫ (x : X), (g : (a : X) → ℝ) x ∂μ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
g : X →ᵇ ℝ
g' : X →C_c ℝ := { toFun := (⇑g : (a : X) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
    (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (g : (a : X) → ℝ) x)

Tactic:
(integral_rieszMeasure Λ g').symm

Premises used: RealRMK.integral_rieszMeasure, Eq.symm
-- 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
inst_4 : CompactSpace X
μ : Measure X
inst_5 : IsFiniteMeasure μ
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ :=
  { toFun := fun (g : X →C_c ℝ) ↦ ∫ (x : X), (g : (a : X) → ℝ) x ∂μ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
g : X →ᵇ ℝ
g' : X →C_c ℝ := { toFun := (⇑g : (a : X) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
    (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (g : (a : X) → ℝ) x)

Tactic:
exact (integral_rieszMeasure Λ g').symm

Premises used: RealRMK.integral_rieszMeasure, Eq.symm
-- 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
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
⊢ CompactSpace.{u_1} (↑K : Type u_1)

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- 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
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
this : CompactSpace.{u_1} (↑K : Type u_1)
⊢ ∃ (ν : Measure (↑K : Type u_1)),
    ν.Regular ∧
      IsFiniteMeasure ν ∧
        ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
          Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
            (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν)

Tactic:
Measure.exists_regular_eq_of_compactSpace μ'

Premises used: MeasureTheory.Measure.exists_regular_eq_of_compactSpace