awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
n : Fin N
x : X
hx :
  (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 - ε < (f : (a : X) → ℝ) x ∧
      (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
⊢ a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x
have linarith : (f : (a : X) → ℝ) x ≤ a + ε * (↑(↑n : ℕ) : ℝ) →
  HSub.hSub (β := ℝ) (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 - ε) ((f : (a : X) → ℝ) x : ℝ) +
      HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (a + ε * (↑(↑n : ℕ) : ℝ)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
n : Fin N
x : X
hx :
  (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 - ε < (f : (a : X) → ℝ) x ∧
      (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
⊢ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
have linarith : a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 < (f : (a : X) → ℝ) x →
  HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) +
      HSub.hSub (β := ℝ) (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ((f : (a : X) → ℝ) x : ℝ) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
⊢ ∃ (V : Opens X),
    E ⊆ (↑V : Set X) ∧
      (∀ x ∈ V, (f : (a : X) → ℝ) x < c) ∧
        ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
have hε' : ε.toNNReal ≠ 0
Tactic: have hε' := ne_of_gt <| Real.toNNReal_pos.mpr hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
⊢ ∃ (V : Opens X),
    E ⊆ (↑V : Set X) ∧
      (∀ x ∈ V, (f : (a : X) → ℝ) x < c) ∧
        ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
have obtain : ∀ (V₁ : Opens X)
  (hV₁ :
    E ⊆ (↑V₁ : Set X) ∧
      (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
        HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)),
  ∃ (V : Opens X),
    E ⊆ (↑V : Set X) ∧
      (∀ x ∈ V, (f : (a : X) → ℝ) x < c) ∧
        ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
Tactic: obtain ⟨V₁ : Opens X, hV₁⟩ := Content.outerMeasure_exists_open μ hμ hε'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
⊢ ∃ (V : Opens X),
    E ⊆ (↑V : Set X) ∧
      (∀ x ∈ V, (f : (a : X) → ℝ) x < c) ∧
        ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
have h : E ⊆ (↑(V₁ ⊓ V₂) : Set X) ∧
  (∀ x ∈ V₁ ⊓ V₂, (f : (a : X) → ℝ) x < c) ∧
    ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
Tactic: use V₁ ⊓ V₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
⊢ E ⊆ (↑(V₁ ⊓ V₂) : Set X) ∧
    (∀ x ∈ V₁ ⊓ V₂, (f : (a : X) → ℝ) x < c) ∧
      ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
        HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
have h : ∀ x ∈ V₁ ⊓ V₂, (f : (a : X) → ℝ) x < c
Tactic: refine ⟨subset_inter hV₁.1 hfE, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
h : ∀ x ∈ V₁ ⊓ V₂, (f : (a : X) → ℝ) x < c
⊢ E ⊆ (↑(V₁ ⊓ V₂) : Set X) ∧
    (∀ x ∈ V₁ ⊓ V₂, (f : (a : X) → ℝ) x < c) ∧
      ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
        HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
have h₁ : ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
  HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
Tactic: refine ⟨subset_inter hV₁.1 hfE, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
x : X
hx : x ∈ V₁ ⊓ V₂
⊢ (f : (a : X) → ℝ) x < c
have h : ∀ x ∈ V₂.carrier, (f : (a : X) → ℝ) x < c
Tactic: suffices ∀ x ∈ V₂.carrier, f x < c from this x (mem_of_mem_inter_right hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
have rw : HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
Tactic: rw [Content.measure_apply μ hμ', ENNReal.ofNNReal_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
rw :
  HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε) =
  HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
Tactic: rw [Content.measure_apply μ hμ', ENNReal.ofNNReal_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
⊢ ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
have _ : LE.le (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) : ℝ≥0∞)
  (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) : ℝ≥0∞)
Tactic: calc
      _ ≤ μ.measure V₁ := by simp [measure_mono]
      _ = μ.outerMeasure V₁ := Content.measure_apply μ (V₁.2.measurableSet)
      _ ≤ μ.outerMeasure E + ε.toNNReal := hV₁.2
      _ = _ := by rw [Content.measure_apply μ hμ', ENNReal.ofNNReal_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
_ :
  LE.le (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) : ℝ≥0∞)
    (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) : ℝ≥0∞)
⊢ ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
have _₁ : HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
Tactic: calc
      _ ≤ μ.measure V₁ := by simp [measure_mono]
      _ = μ.outerMeasure V₁ := Content.measure_apply μ (V₁.2.measurableSet)
      _ ≤ μ.outerMeasure E + ε.toNNReal := hV₁.2
      _ = _ := by rw [Content.measure_apply μ hμ', ENNReal.ofNNReal_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
a' b' ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun (N : ℝ) ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
have hf : Tendsto (α := ℝ) (HDiv.hDiv a') atTop (𝓝 0)
Tactic: apply Tendsto.mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
a' b' ε : ℝ
hε : 0 < ε
hf : Tendsto (α := ℝ) (HDiv.hDiv a') atTop (𝓝 0)
⊢ Tendsto (fun (N : ℝ) ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
have hg : Tendsto (fun (x : ℝ) ↦ b' + a' / x) atTop (𝓝 (b' + 0))
Tactic: apply Tendsto.mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
a' b' ε : ℝ
hε : 0 < ε
⊢ ∃ (N : ℕ), 0 < N ∧ a' / (↑N : ℝ) * (b' + a' / (↑N : ℝ)) ≤ ε
have A : Tendsto (fun (N : ℝ) ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
Tactic: have A : Tendsto (fun (N : ℝ) ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0))) := by
    apply Tendsto.mul
    · exact Tendsto.div_atTop tendsto_const_nhds tendsto_id
    · exact Tendsto.add tendsto_const_nhds (Tendsto.div_atTop tendsto_const_nhds tendsto_id)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
a' b' ε : ℝ
hε : 0 < ε
A : Tendsto (fun (N : ℝ) ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
⊢ ∃ (N : ℕ), 0 < N ∧ a' / (↑N : ℝ) * (b' + a' / (↑N : ℝ)) ≤ ε
have B : Tendsto ((fun (N : ℝ) ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) atTop (𝓝 (0 * (b' + 0)))
Tactic: have B := A.comp tendsto_natCast_atTop_atTop
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
a' b' ε : ℝ
hε : 0 < ε
A : Tendsto (fun (N : ℝ) ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
B : Tendsto ((fun (N : ℝ) ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) atTop (𝓝 (0 * (b' + 0)))
⊢ ∃ (N : ℕ), 0 < N ∧ a' / (↑N : ℝ) * (b' + a' / (↑N : ℝ)) ≤ ε
have B₁ : Tendsto (β := ℝ) ((fun (N : ℝ) ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) atTop (𝓝 0)
Tactic: simp only [add_zero, zero_mul] at B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
a' b' ε : ℝ
hε : 0 < ε
A : Tendsto (fun (N : ℝ) ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
B : Tendsto (β := ℝ) ((fun (N : ℝ) ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) atTop (𝓝 0)
⊢ ∃ (N : ℕ), 0 < N ∧ a' / (↑N : ℝ) * (b' + a' / (↑N : ℝ)) ≤ ε
have obtain : ∀ (N : ℕ) (hN : ((fun (N : ℝ) ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) N < ε) (h'N : 1 ≤ N),
  ∃ (N : ℕ), 0 < N ∧ a' / (↑N : ℝ) * (b' + a' / (↑N : ℝ)) ≤ ε
Tactic: obtain ⟨N, hN, h'N⟩ := (((tendsto_order.1 B).2 _ hε).and (Ici_mem_atTop 1)).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
⊢ LE.le (α := ℝ) ((Λ : (a : X →C_c ℝ) → ℝ) f : ℝ)
    (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x : ℝ)
have apply : ∀ (ε : ℝ),
  0 < ε → (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
Tactic: apply le_iff_forall_pos_le_add.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
⊢ ∃ (a : ℝ) (b : ℝ), a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
have obtain : ∀ (r : ℝ) (hr : 0 < r ∧ range f.toFun ⊆ Metric.ball 0 r),
  ∃ (a : ℝ) (b : ℝ), a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
Tactic: obtain ⟨r, hr⟩ := (Metric.isCompact_iff_isClosed_bounded.mp
      (HasCompactSupport.isCompact_range f.2 f.1.2)).2.subset_ball_lt 0 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
r : ℝ
hr : 0 < r ∧ range f.toFun ⊆ Metric.ball 0 r
⊢ -r < r
have linarith : r ≤ -r → 2 * (0 - r) + (r - -r) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
r : ℝ
hr : 0 < r ∧ range f.toFun ⊆ Metric.ball 0 r
linarith : r ≤ -r → 2 * (0 - r) + (r - -r) = 0
⊢ -r < r
have linarith₁ : r ≤ -r → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
⊢ (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
have obtain : ∀ (a b : ℝ) (hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b),
  (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
Tactic: obtain ⟨a, b, hab⟩ : ∃ a b : ℝ, a < b ∧ range f ⊆ Ioo a b := by
    obtain ⟨r, hr⟩ := (Metric.isCompact_iff_isClosed_bounded.mp
      (HasCompactSupport.isCompact_range f.2 f.1.2)).2.subset_ball_lt 0 0
    exact ⟨-r, r, by linarith, hr.2.trans_eq (by simp [Real.ball_eq_Ioo])⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
⊢ (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
have obtain : ∀ (N : ℕ) (hN : 0 < N) (hε' : (b - a) / (↑N : ℝ) * (2 * μ.real K + |a| + b + (b - a) / (↑N : ℝ)) ≤ ε),
  (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
Tactic: obtain ⟨N, hN, hε'⟩ := exists_nat_large (b - a) (2 * μ.real K + |a| + b) hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
hε' : (b - a) / (↑N : ℝ) * (2 * μ.real K + |a| + b + (b - a) / (↑N : ℝ)) ≤ ε
ε' : ℝ := (b - a) / (↑N : ℝ)
⊢ (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
have hε'₁ : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
Tactic: replace hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε :=
    ⟨div_pos (sub_pos.mpr hab.1) (Nat.cast_pos'.mpr hN), hε'⟩
Cleared hypotheses: hε'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
⊢ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ((b - a) / (↑N : ℝ)))
have field_simp : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (b - a))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / (↑N : ℝ)
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
⊢ (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
have obtain : ∀ (E : Fin N → Set X)
  (hE :
    Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
      PairwiseDisjoint univ E ∧
        (∀ (n : Fin N),
            ∀ x ∈ E n,
              a + ε' * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
                (f : (a : X) → ℝ) x ≤ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
          ∀ (n : Fin N), MeasurableSet (E n)),
  (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
Tactic: obtain ⟨E, hE⟩ := range_cut_partition f a hε'.1 N <| by
    dsimp [ε']
    field_simp
    simp [hab.2]