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 : ℝ)
x : X
pos :
  ∀ (hx : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x),
    LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
neg : ∀ (hx : x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)

Tactic:
by_cases hx : x ∈ tsupport f

Premises used: tsupport, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : 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 : ℝ)
x : X
hx : Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
⊢ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)

Tactic:
simp [(pf2 hx), (pf3 x).2]

Premises used: And.right
-- 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 : ℝ)
x : X
hx : x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
⊢ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)

Tactic:
simp [image_eq_zero_of_notMem_tsupport hx, Set.indicator_nonneg]

Premises used: image_eq_zero_of_notMem_tsupport, Set.indicator_nonneg
-- 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 : ℝ)
⊢ ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)

Tactic:
have hfV (x : X) : f x ≤ V.indicator 1 x := by
    by_cases hx : x ∈ tsupport f
    · simp [(pf2 hx), (pf3 x).2]
    · simp [image_eq_zero_of_notMem_tsupport hx, Set.indicator_nonneg]
-- 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 : ℝ)
x : X
pos : ∀ (hx : x ∈ K), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
neg : ∀ (hx : x ∉ K), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
by_cases hx : x ∈ K
-- 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 : ℝ)
x : X
hx : x ∈ K
⊢ LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
simp [hx, pf1 hx]
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : 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 : ℝ)
x : X
hx : x ∉ K
⊢ LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
simp [hx, (pf3 x).1]

Premises used: And.left
-- 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 : ℝ)
⊢ ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
have hfK (x : X) : K.indicator 1 x ≤ f x := by
    by_cases hx : x ∈ K
    · simp [hx, pf1 hx]
    · simp [hx, (pf3 x).1]
-- 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 : ℝ)
⊢ μ.real K = ∫ (x : X), K.indicator 1 x ∂μ

Tactic:
integral_indicator_one hK.measurableSet |>.symm

Premises used: MeasureTheory.integral_indicator_one, Eq.symm, 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 : ν.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 : ℝ)
⊢ LE.le (α := ℝ) (∫ (x : X), K.indicator 1 x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)

Tactic:
integral_mono ?_ f.integrable hfK

Premises used: MeasureTheory.integral_mono, CompactlySupportedContinuousMap.integrable
-- 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 : ℝ)
refine : Integrable (ε := ℝ) (K.indicator 1) μ
⊢ LE.le (α := ℝ) (∫ (x : X), K.indicator 1 x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)

Tactic:
refine integral_mono ?_ f.integrable hfK

Premises used: MeasureTheory.integral_mono, CompactlySupportedContinuousMap.integrable
-- 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 (ε := ℝ) (K.indicator 1) μ

Tactic:
(continuousOn_const.integrableOn_compact hK).integrable_indicator hK.measurableSet

Premises used: MeasureTheory.IntegrableOn.integrable_indicator, 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 : ν.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 (ε := ℝ) (K.indicator 1) μ

Tactic:
exact (continuousOn_const.integrableOn_compact hK).integrable_indicator hK.measurableSet

Premises used: MeasureTheory.IntegrableOn.integrable_indicator, 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 : ν.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 : ℝ)
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)

Tactic:
hμν f
-- 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 : ℝ)
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν) (∫ (x : X), V.indicator 1 x ∂ν)

Tactic:
integral_mono f.integrable ?_ hfV

Premises used: MeasureTheory.integral_mono, CompactlySupportedContinuousMap.integrable
-- 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 : ℝ)
refine : Integrable (ε := ℝ) (V.indicator 1) ν
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν) (∫ (x : X), V.indicator 1 x ∂ν)

Tactic:
refine integral_mono f.integrable ?_ hfV

Premises used: MeasureTheory.integral_mono, CompactlySupportedContinuousMap.integrable
-- 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:
IntegrableOn.integrable_indicator integrableOn_const pV2.measurableSet

Premises used: MeasureTheory.IntegrableOn.integrable_indicator, IsOpen.measurableSet, MeasureTheory.integrableOn_const