awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
r : ENNReal
hr : (μ : (a : Set X) → ENNReal) k < r
U : Set X
kU : k ⊆ U
U_open : IsOpen U
mu_U : (μ : (a : Set X) → ENNReal) U < r
f : X → ℝ
f_cont : Continuous f
fk : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 k
fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ
f_comp : HasCompactSupport (α := X) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ)
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 ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r
have refine : ENNReal.ofReal (∫ (x : X), f x ∂μ) < r
Tactic: refine ⟨f, f_cont, f_comp, fk, fun x ↦ (f_range x).1, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal)
    (⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
have a : LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal)
  (⨆ (f : X → ℝ),
      ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
    ENNReal)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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 :
  LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal)
    (⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal)
    (⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
have a₁ : 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: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal)
    (⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
have apply : ∀ (r : ENNReal) (hr : r < (μ : (a : Set X) → ENNReal) U),
  r <
    ⨆ (f : X → ℝ),
      ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)
Tactic: apply le_of_forall_lt (fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ r <
    ⨆ (f : X → ℝ),
      ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)
have simp : ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)
Tactic: simp only [lt_iSup_iff, exists_prop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)
have 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 ∂μ)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)
have 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 ∂μ)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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 ∂μ)
have refine : r < ENNReal.ofReal (∫ (x : X), f x ∂μ)
Tactic: refine ⟨f, f_cont, fU, fun x ↦ (f_range x).1, fun x ↦ (f_range x).2, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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 : ℝ)
⊢ r < ENNReal.ofReal (∫ (x : X), f x ∂μ)
have apply : (μ : (a : Set X) → ENNReal) K ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
Tactic: apply hK.trans_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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 : ℝ)
⊢ (μ : (a : Set X) → ENNReal) K ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
have f_int : Integrable f μ
Tactic: apply Integrable.measure_le_integral
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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 μ
⊢ (μ : (a : Set X) → ENNReal) K ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
have f_nonneg : 0 ≤ᶠ[ae μ] f
Tactic: apply Integrable.measure_le_integral
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ (μ : (a : Set X) → ENNReal) K ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
have hs : ∀ x ∈ K, 1 ≤ f x
Tactic: apply Integrable.measure_le_integral
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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 : ℝ)
⊢ Integrable f μ
have f_int : ∀ᵐ (ω : X) ∂μ, Membership.mem (γ := Set ℝ) (Icc 0 1) (f ω)
Tactic: apply Integrable.of_mem_Icc 0 1 f_cont.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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) ∂μ, Membership.mem (γ := Set ℝ) (Icc 0 1) (f ω)
have f_int : ∀ (a : X), Membership.mem (γ := Set X) {x : X | (fun (ω : X) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) (f ω)) x} a
Tactic: filter_upwards [] with x using f_range x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ ∀ᵐ (ω : X) ∂μ, Membership.mem (γ := Set ℝ) (Icc 0 1) (f ω)
have f_int₁ : ∀ (a : X), Membership.mem (γ := Set ℝ) (Icc 0 1) (f a)
Tactic: filter_upwards [] with x using f_range x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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 : ℝ)
⊢ 0 ≤ᶠ[ae μ] f
have f_nonneg : ∀ (a : X), Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ 0 x ≤ f x) x} a
Tactic: filter_upwards [] with x using (f_range x).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ 0 ≤ᶠ[ae μ] f
have f_nonneg₁ : ∀ (a : X), 0 a ≤ f a
Tactic: filter_upwards [] with x using (f_range x).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ 1 ≤ f x
have hs : f x = 1
Tactic: apply Eq.ge
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
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
⊢ 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)
have 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
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₁ : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₂ : ℝ≥0)
have 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)
Tactic: obtain ⟨g, hg⟩ := CompactlySupportedContinuousMap.exists_add_of_le h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
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₂ : ℝ≥0)
have rw : LE.le (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f₁ : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (f₁ + g) : ℝ≥0)
Tactic: rw [← hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
⊢ 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)})
have 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)}
Tactic: rw [image_nonempty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
⊢ 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)}
have 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)}
Tactic: obtain ⟨V, hVcp, hKsubintV⟩ := exists_compact_superset K.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ IsCompact (closure (interior V))
have apply : closure (interior V) ⊆ V
Tactic: apply IsCompact.of_isClosed_subset hVcp isClosed_closure
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
⊢ closure (interior V) ⊆ V
have nth_rw : closure (interior V) ⊆ closure V
Tactic: nth_rw 2 [← closure_eq_iff_isClosed.mpr (IsCompact.isClosed hVcp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
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)}
have hIsCompact_closure_interior : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (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)}
have 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)}
Tactic: obtain ⟨f, hsuppfsubV, hfeq1onK, hfinicc⟩ :=
    exists_tsupport_one_of_isOpen_isClosed isOpen_interior hIsCompact_closure_interior
      (IsCompact.isClosed K.2) hKsubintV
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
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 : ℝ)
⊢ 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)}
have hfHasCompactSupport : HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ)
Tactic: have hfHasCompactSupport : HasCompactSupport f :=
    IsCompact.of_isClosed_subset hVcp (isClosed_tsupport f)
      (Set.Subset.trans hsuppfsubV interior_subset)