awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
obtain :
  ∀ (K : Set X) (KU : K ⊆ U) (K_comp : IsCompact K) (hK : r < (μ : (a : Set X) → ENNReal) K),
    ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)
⊢ ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)

Tactic:
obtain ⟨K, KU, K_comp, hK⟩ : ∃ K ⊆ U, IsCompact K ∧ r < μ K :=
      MeasurableSet.exists_lt_isCompact_of_ne_top hU.measurableSet (by simp) hr

Premises used: IsOpen.measurableSet, MeasurableSet.exists_lt_isCompact_of_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 Uᶜ ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K ∧
        ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
exists_continuous_zero_one_of_isClosed
      hU.isClosed_compl K_comp.isClosed (disjoint_compl_left_iff_subset.mpr KU)

Premises used: Iff.mpr, Set.disjoint_compl_left_iff_subset, exists_continuous_zero_one_of_isClosed, IsOpen.isClosed_compl, IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
obtain :
  ∀ (f : X → ℝ) (f_cont : Continuous f)
    (fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ)
    (fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K)
    (f_range :
      ∀ (x : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
          (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)),
    ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)
⊢ ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)

Tactic:
obtain ⟨⟨f, f_cont⟩, fU, fK, f_range⟩ : ∃ (f : C(X, ℝ)), EqOn f 0 Uᶜ ∧ EqOn f 1 K
        ∧ ∀ (x : X), f x ∈ Icc 0 1 := exists_continuous_zero_one_of_isClosed
      hU.isClosed_compl K_comp.isClosed (disjoint_compl_left_iff_subset.mpr KU)

Premises used: Iff.mpr, Set.disjoint_compl_left_iff_subset, exists_continuous_zero_one_of_isClosed, IsOpen.isClosed_compl, IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
⊢ ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)

Tactic:
⟨f, f_cont, fU, fun x ↦ (f_range x).1, fun x ↦ (f_range x).2, ?_⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
refine : r < ENNReal.ofReal (∫ (x : X), f x ∂μ)
⊢ ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)

Tactic:
refine ⟨f, f_cont, fU, fun x ↦ (f_range x).1, fun x ↦ (f_range x).2, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
apply : (μ : (a : Set X) → ENNReal) K ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
⊢ r < ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
apply hK.trans_le

Premises used: LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
hs : ∀ x ∈ K, 1 ≤ f x
⊢ (μ : (a : Set X) → ENNReal) K ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
apply Integrable.measure_le_integral

Premises used: MeasureTheory.Integrable.measure_le_integral
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
f_int : ∀ᵐ (ω : X) ∂μ, Membership.mem (γ := Set ℝ) (Icc 0 1) (f ω)
⊢ Integrable f μ

Tactic:
apply Integrable.of_mem_Icc 0 1 f_cont.aemeasurable

Premises used: Continuous.aemeasurable, MeasureTheory.Integrable.of_mem_Icc, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
x : X
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)

Tactic:
f_range x

Premises used: Set.Mem
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
f_int : ∀ (a : X), Membership.mem (γ := Set X) {x : X | (fun (ω : X) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) (f ω)) x} a
f_int₁ f_int₂ : ∀ (x : X), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
⊢ ∀ᵐ (ω : X) ∂μ, Membership.mem (γ := Set ℝ) (Icc 0 1) (f ω)

Tactic:
filter_upwards [] with x using f_range x
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
x : X
⊢ 0 x ≤ f x

Tactic:
(f_range x).1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
f_nonneg : ∀ (a : X), Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ 0 x ≤ f x) x} a
f_nonneg₁ f_nonneg₂ : ∀ (x : X), 0 x ≤ f x
⊢ 0 ≤ᶠ[ae μ] f

Tactic:
filter_upwards [] with x using (f_range x).1
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
x : X
hx : x ∈ K
hs : f x = 1
⊢ 1 ≤ f x

Tactic:
apply Eq.ge

Premises used: Eq.ge
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
x : X
hx : x ∈ K
⊢ f x = 1

Tactic:
fK hx
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < (μ : (a : Set X) → ENNReal) K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
fK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 K
f_range :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
x : X
hx : x ∈ K
⊢ f x = 1

Tactic:
exact fK hx
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
a :
  ∀ (i : X → ℝ) (i_1 : Continuous i) (i_2 : EqOn i 0 Uᶜ) (i_3 : 0 ≤ i) (i_4 : i ≤ 1),
    ENNReal.ofReal (∫ (x : X), i x ∂μ) ≤ (μ : (a : Set X) → ENNReal) U
⊢ LE.le (α := ENNReal)
    (⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
    ((μ : (a : Set X) → ENNReal) U : ENNReal)

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
f : X → ℝ
f_cont : Continuous f
fU : EqOn f 0 Uᶜ
f_nonneg : 0 ≤ f
f_le : f ≤ 1
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ENNReal) U

Tactic:
integral_le_measure (fun x hx ↦ f_le x) (fun x hx ↦ le_of_eq (fU hx))

Premises used: MeasureTheory.integral_le_measure, le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
f : X → ℝ
f_cont : Continuous f
fU : EqOn f 0 Uᶜ
f_nonneg : 0 ≤ f
f_le : f ≤ 1
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ENNReal) U

Tactic:
exact integral_le_measure (fun x hx ↦ f_le x) (fun x hx ↦ le_of_eq (fU hx))

Premises used: MeasureTheory.integral_le_measure, le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
obtain :
  ∀ (g : X →C_c ℝ≥0) (hg : f₁ + g = f₂),
    LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₁ : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₂ : ℝ≥0)
⊢ LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₁ : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₂ : ℝ≥0)

Tactic:
obtain ⟨g, hg⟩ := CompactlySupportedContinuousMap.exists_add_of_le h

Premises used: CompactlySupportedContinuousMap.exists_add_of_le
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
g : X →C_c ℝ≥0
hg : f₁ + g = f₂
rw : LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₁ : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (f₁ + g) : ℝ≥0)
⊢ LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₁ : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₂ : ℝ≥0)

Tactic:
rw [← hg]
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
g : X →C_c ℝ≥0
hg : f₁ + g = f₂
⊢ LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₁ : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (f₁ + g) : ℝ≥0)

Tactic:
simp
-- 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
K : Compacts X
rw :
  Set.Nonempty.{u_1} (α := X →C_c ℝ≥0)
    {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}
⊢ Set.Nonempty (α := ℝ≥0)
    (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)})

Tactic:
rw [image_nonempty]

Premises used: Set.image_nonempty
-- 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
K : Compacts X
obtain :
  ∀ (V : Set X) (hVcp : IsCompact V) (hKsubintV : K.carrier ⊆ interior V),
    Set.Nonempty.{u_1} (α := X →C_c ℝ≥0)
      {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}
⊢ Set.Nonempty.{u_1} (α := X →C_c ℝ≥0)
    {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}

Tactic:
obtain ⟨V, hVcp, hKsubintV⟩ := exists_compact_superset K.2

Premises used: TopologicalSpace.Compacts.isCompact', exists_compact_superset
-- 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
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
apply : closure (interior V) ⊆ V
⊢ IsCompact (closure (interior V))

Tactic:
apply IsCompact.of_isClosed_subset hVcp isClosed_closure

Premises used: IsCompact.of_isClosed_subset, isClosed_closure
-- 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
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
nth_rw : closure (interior V) ⊆ closure V
⊢ closure (interior V) ⊆ V

Tactic:
nth_rw 2 [← closure_eq_iff_isClosed.mpr (IsCompact.isClosed hVcp)]

Premises used: Iff.mpr, closure_eq_iff_isClosed, IsCompact.isClosed
-- 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
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ closure (interior V) ⊆ closure V

Tactic:
closure_mono interior_subset

Premises used: interior_subset, closure_mono
-- 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
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ closure (interior V) ⊆ closure V

Tactic:
exact closure_mono interior_subset

Premises used: interior_subset, closure_mono
-- 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
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ IsCompact (closure (interior V))

Tactic:
have hIsCompact_closure_interior : IsCompact (closure (interior V)) := by
    apply IsCompact.of_isClosed_subset hVcp isClosed_closure
    nth_rw 2 [← closure_eq_iff_isClosed.mpr (IsCompact.isClosed hVcp)]
    exact closure_mono interior_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
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
obtain :
  ∀ (f : C(X, ℝ)) (hsuppfsubV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ interior V)
    (hfeq1onK : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K.carrier)
    (hfinicc : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)),
    Set.Nonempty.{u_1} (α := X →C_c ℝ≥0)
      {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}
⊢ Set.Nonempty.{u_1} (α := X →C_c ℝ≥0)
    {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}

Tactic:
obtain ⟨f, hsuppfsubV, hfeq1onK, hfinicc⟩ :=
    exists_tsupport_one_of_isOpen_isClosed isOpen_interior hIsCompact_closure_interior
      (IsCompact.isClosed K.2) hKsubintV

Premises used: isOpen_interior, TopologicalSpace.Compacts.isCompact', exists_tsupport_one_of_isOpen_isClosed, IsCompact.isClosed
-- 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
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ interior V
hfeq1onK : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K.carrier
hfinicc : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
⊢ HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ)

Tactic:
have hfHasCompactSupport : HasCompactSupport f :=
    IsCompact.of_isClosed_subset hVcp (isClosed_tsupport f)
      (Set.Subset.trans hsuppfsubV interior_subset)