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
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' := ⋯ }
⊢ Eq (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) : ℝ≥0∞)

Tactic:
Content.measure_apply μ (V₁.2.measurableSet)

Premises used: IsOpen.measurableSet, TopologicalSpace.Opens.is_open', MeasureTheory.Content.measure_apply
-- 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
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' := ⋯ }
⊢ (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)

Tactic:
hV₁.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
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 ε)
rw₁ 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 ε)
⊢ 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:
rw [Content.measure_apply μ hμ', ENNReal.ofNNReal_toNNReal]

Premises used: ENNReal.ofNNReal_toNNReal, MeasureTheory.Content.measure_apply
-- 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
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∞)
_₁ :
  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 ε)
⊢ ((μ.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:
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]

Premises used: IsOpen.measurableSet, MeasureTheory.Content.outerMeasure, SetLike.coe, And.right, MeasureTheory.Content.measure, TopologicalSpace.Opens.is_open', DFunLike.coe, MeasureTheory.Content.measure_apply, Real.toNNReal
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
a' b' ε : ℝ
hε : 0 < ε
hf : Tendsto (α := ℝ) (HDiv.hDiv a') atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ b' + a' / x) atTop (𝓝 (b' + 0))
⊢ Tendsto (fun (N : ℝ) ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))

Tactic:
apply Tendsto.mul

Premises used: Filter.Tendsto.mul
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
a' b' ε : ℝ
hε : 0 < ε
⊢ Tendsto (α := ℝ) (HDiv.hDiv a') atTop (𝓝 0)

Tactic:
Tendsto.div_atTop tendsto_const_nhds tendsto_id

Premises used: Filter.Tendsto.div_atTop, Filter.tendsto_id, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
a' b' ε : ℝ
hε : 0 < ε
⊢ Tendsto (α := ℝ) (HDiv.hDiv a') atTop (𝓝 0)

Tactic:
exact Tendsto.div_atTop tendsto_const_nhds tendsto_id

Premises used: Filter.Tendsto.div_atTop, Filter.tendsto_id, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
a' b' ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun (x : ℝ) ↦ b' + a' / x) atTop (𝓝 (b' + 0))

Tactic:
Tendsto.add tendsto_const_nhds (Tendsto.div_atTop tendsto_const_nhds tendsto_id)

Premises used: Filter.Tendsto.div_atTop, Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
a' b' ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun (x : ℝ) ↦ b' + a' / x) atTop (𝓝 (b' + 0))

Tactic:
exact Tendsto.add tendsto_const_nhds (Tendsto.div_atTop tendsto_const_nhds tendsto_id)

Premises used: Filter.Tendsto.div_atTop, Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
a' b' ε : ℝ
hε : 0 < ε
⊢ 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)
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
a' b' ε : ℝ
hε : 0 < ε
A : Tendsto (fun (N : ℝ) ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
⊢ Tendsto ((fun (N : ℝ) ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) atTop (𝓝 (0 * (b' + 0)))

Tactic:
have B := A.comp tendsto_natCast_atTop_atTop
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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)))
⊢ Tendsto (β := ℝ) ((fun (N : ℝ) ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) atTop (𝓝 0)

Tactic:
simp only [add_zero, zero_mul] at B

Premises used: MulZeroClass.zero_mul, add_zero
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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)
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 : ℝ)) ≤ ε
⊢ ∃ (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

Premises used: tendsto_order, Filter.Eventually.and, Filter.Eventually.exists, Filter.Ici_mem_atTop, And.right, Iff.mp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 : ℕ
hN : ((fun (N : ℝ) ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) N < ε
h'N : 1 ≤ N
⊢ ∃ (N : ℕ), 0 < N ∧ a' / (↑N : ℝ) * (b' + a' / (↑N : ℝ)) ≤ ε

Tactic:
⟨N, h'N, hN.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 : ℕ
hN : ((fun (N : ℝ) ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) N < ε
h'N : 1 ≤ N
⊢ ∃ (N : ℕ), 0 < N ∧ a' / (↑N : ℝ) * (b' + a' / (↑N : ℝ)) ≤ ε

Tactic:
exact ⟨N, h'N, hN.le⟩
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
apply :
  ∀ (ε : ℝ),
    0 < ε →
      (Λ : (a : X →C_c ℝ) → ℝ) f ≤ (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (f : (a : X) → ℝ) x) + ε
⊢ LE.le (α := ℝ) ((Λ : (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

Premises used: Iff.mpr, le_iff_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
obtain :
  ∀ (r : ℝ) (hr : 0 < r ∧ range f.toFun ⊆ Metric.ball 0 r),
    ∃ (a : ℝ) (b : ℝ), a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b
⊢ ∃ (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

Premises used: Metric.isCompact_iff_isClosed_bounded, Bornology.IsBounded.subset_ball_lt, CompactlySupportedContinuousMap.toContinuousMap, And.right, ContinuousMap.continuous_toFun, HasCompactSupport.isCompact_range, Iff.mp, CompactlySupportedContinuousMap.hasCompactSupport', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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
linarith₁ : r ≤ -r → GT.gt (α := ℝ) 2 0
⊢ -r < r

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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
⊢ Metric.ball 0 r = Ioo (-r) r

Tactic:
simp [Real.ball_eq_Ioo]

Premises used: Real.ball_eq_Ioo
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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
⊢ ∃ (a : ℝ) (b : ℝ), a < b ∧ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a b

Tactic:
exact ⟨-r, r, by linarith, hr.2.trans_eq (by simp [Real.ball_eq_Ioo])⟩
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
ε : ℝ
hε : 0 < ε
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) + ε
⊢ (Λ : (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])⟩

Premises used: Set.range, 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
Λ : (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
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) + ε
⊢ (Λ : (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ε

Premises used: HMul.hMul, abs, MeasureTheory.Measure.real, HSub.hSub, HAdd.hAdd, OfNat.ofNat, _private.0.RealRMK.exists_nat_large
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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 : ℝ)
⊢ 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ε'⟩
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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 + ε') ≤ ε
dsimp : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ((b - a) / (↑N : ℝ)))
⊢ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε')

Tactic:
dsimp [ε']
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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 + ε') ≤ ε
field_simp : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (b - a))
⊢ range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ((b - a) / (↑N : ℝ)))

Tactic:
field_simp
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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 + (b - a))

Tactic:
simp [hab.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
Λ : (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 + ε') ≤ ε
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) + ε
⊢ (Λ : (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]

Premises used: And.left, RealRMK.range_cut_partition
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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 + ε') ≤ ε
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)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
n : Fin N
rw : E n ⊆ ⋃ (j : Fin N), E j
⊢ E n ⊆ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)

Tactic:
rw [hE.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
Λ : (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 + ε') ≤ ε
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)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
n : Fin N
⊢ E n ⊆ ⋃ (j : Fin N), E j

Tactic:
subset_iUnion _ _

Premises used: Set.subset_iUnion
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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 + ε') ≤ ε
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)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
n : Fin N
⊢ E n ⊆ ⋃ (j : Fin N), E j

Tactic:
exact subset_iUnion _ _

Premises used: Set.subset_iUnion
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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 + ε') ≤ ε
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)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
n : Fin N
⊢ E n ⊆ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)

Tactic:
have h : E n ⊆ tsupport f := by rw [hE.1]; exact subset_iUnion _ _
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
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 + ε') ≤ ε
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)
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
n : Fin N
h : E n ⊆ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_top_iff_ne_top.mp ?_

Premises used: lt_top_iff_ne_top, Iff.mp