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
Λ : (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) → ℝ)
refine : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine lt_top_iff_ne_top.mp ?_

Premises used: lt_top_iff_ne_top, Iff.mp
-- 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) → ℝ)
apply : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply lt_of_le_of_lt <| measure_mono h

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono
-- 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) → ℝ)
dsimp :
  LT.lt (α := ℝ≥0∞) (((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞)

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 + ε') ≤ ε
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) → ℝ)
rw :
  LT.lt (α := ℝ≥0∞) (((rieszContent (toNNRealLinear Λ)).outerMeasure : (a : Set X) → ℝ≥0∞) (tsupport f.toFun) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [rieszMeasure, ← coe_toContinuousMap, ← ContinuousMap.toFun_eq_coe,
      Content.measure_apply _ f.2.measurableSet]

Premises used: RealRMK.rieszMeasure, CompactlySupportedContinuousMap.coe_toContinuousMap, CompactlySupportedContinuousMap.hasCompactSupport', ContinuousMap.toFun_eq_coe, IsCompact.measurableSet, 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
Λ : (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) → ℝ)
⊢ LT.lt (α := ℝ≥0∞) (((rieszContent (toNNRealLinear Λ)).outerMeasure : (a : Set X) → ℝ≥0∞) (tsupport f.toFun) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
Content.outerMeasure_lt_top_of_isCompact _ f.2

Premises used: CompactlySupportedContinuousMap.hasCompactSupport', MeasureTheory.Content.outerMeasure_lt_top_of_isCompact
-- 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) → ℝ)
⊢ LT.lt (α := ℝ≥0∞) (((rieszContent (toNNRealLinear Λ)).outerMeasure : (a : Set X) → ℝ≥0∞) (tsupport f.toFun) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact Content.outerMeasure_lt_top_of_isCompact _ f.2

Premises used: CompactlySupportedContinuousMap.hasCompactSupport', MeasureTheory.Content.outerMeasure_lt_top_of_isCompact
-- 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), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hE' (n : Fin N) : μ (E n) ≠ ∞ := by
    have h : E n ⊆ tsupport f := by rw [hE.1]; exact subset_iUnion _ _
    refine lt_top_iff_ne_top.mp ?_
    apply lt_of_le_of_lt <| measure_mono h
    dsimp [μ]
    rw [rieszMeasure, ← coe_toContinuousMap, ← ContinuousMap.toFun_eq_coe,
      Content.measure_apply _ f.2.measurableSet]
    exact Content.outerMeasure_lt_top_of_isCompact _ f.2
-- 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
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 < ε' / (↑N : ℝ)

Tactic:
have h_ε' := (div_pos hε'.1 (Nat.cast_pos'.mpr hN))
-- 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
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ε' : 0 < ε' / (↑N : ℝ)
⊢ ∀ (n : Fin N) (x : X) (hx : x ∈ E n), (f : (a : X) → ℝ) x < a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 + ε'

Tactic:
have h n x (hx : x ∈ E n) := lt_add_of_le_of_pos ((hE.2.2.1 n x hx).right) hε'.1
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (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
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ε' : 0 < ε' / (↑N : ℝ)
h : ∀ (n : Fin N) (x : X) (hx : x ∈ E n), (f : (a : X) → ℝ) x < a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 + ε'
⊢ ∀ (n : Fin N),
    Ne (α := ℝ≥0∞) (((rieszContent (toNNRealLinear Λ)).outerMeasure : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h' n := Eq.trans_ne
      (Content.measure_apply (rieszContent (toNNRealLinear Λ)) (hE.2.2.2 n)).symm (hE' n)
-- 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
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ε' : 0 < ε' / (↑N : ℝ)
h : ∀ (n : Fin N) (x : X) (hx : x ∈ E n), (f : (a : X) → ℝ) x < a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 + ε'
h' :
  ∀ (n : Fin N),
    Ne (α := ℝ≥0∞) (((rieszContent (toNNRealLinear Λ)).outerMeasure : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
choose :
  ∀ (V : (n : Fin N) → Opens X)
    (hV :
      ∀ (n : Fin N),
        E n ⊆ (↑(V n) : Set X) ∧
          (∀ x ∈ V n, (f : (a : X) → ℝ) x < a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 + ε') ∧
            (((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
              HAdd.hAdd (α := ℝ≥0∞)
                ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞)
                (ENNReal.ofReal (ε' / (↑N : ℝ)))),
    ∃ (V : Fin N → Opens X),
      ∀ (n : Fin N),
        E n ⊆ (↑(V n) : Set X) ∧
          (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
            (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
⊢ ∃ (V : Fin N → Opens X),
    ∀ (n : Fin N),
      E n ⊆ (↑(V n) : Set X) ∧
        (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
          (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
            HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))

Tactic:
choose V hV using fun n ↦ exists_open_approx f h_ε' (E n) (h' n) (hE.2.2.2 n) (h n)

Premises used: And.right, RealRMK.exists_open_approx
-- 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
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ε' : 0 < ε' / (↑N : ℝ)
h : ∀ (n : Fin N) (x : X) (hx : x ∈ E n), (f : (a : X) → ℝ) x < a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 + ε'
h' :
  ∀ (n : Fin N),
    Ne (α := ℝ≥0∞) (((rieszContent (toNNRealLinear Λ)).outerMeasure : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : (n : Fin N) → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 + ε') ∧
        (((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞)
            ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞)
            (ENNReal.ofReal (ε' / (↑N : ℝ)))
⊢ ∃ (V : Fin N → Opens X),
    ∀ (n : Fin N),
      E n ⊆ (↑(V n) : Set X) ∧
        (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
          (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
            HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))

Tactic:
⟨V, hV⟩

Premises used: Exists.intro
-- 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
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ε' : 0 < ε' / (↑N : ℝ)
h : ∀ (n : Fin N) (x : X) (hx : x ∈ E n), (f : (a : X) → ℝ) x < a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 + ε'
h' :
  ∀ (n : Fin N),
    Ne (α := ℝ≥0∞) (((rieszContent (toNNRealLinear Λ)).outerMeasure : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : (n : Fin N) → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < a + ε' * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 + ε') ∧
        (((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞)
            ((((rieszContent (toNNRealLinear Λ)).measure : Measure X) : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞)
            (ENNReal.ofReal (ε' / (↑N : ℝ)))
⊢ ∃ (V : Fin N → Opens X),
    ∀ (n : Fin N),
      E n ⊆ (↑(V n) : Set X) ∧
        (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
          (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
            HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))

Tactic:
exact ⟨V, hV⟩
-- 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
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
obtain :
  ∀ (V : Fin N → Opens X)
    (hV :
      ∀ (n : Fin N),
        E n ⊆ (↑(V n) : Set X) ∧
          (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
            (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑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 ⟨V, hV⟩ : ∃ V : Fin N → Opens X, ∀ n, E n ⊆ (V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧
      μ (V n) ≤ μ (E n) + ENNReal.ofReal (ε' / N) := by
    have h_ε' := (div_pos hε'.1 (Nat.cast_pos'.mpr hN))
    have h n x (hx : x ∈ E n) := lt_add_of_le_of_pos ((hE.2.2.1 n x hx).right) hε'.1
    have h' n := Eq.trans_ne
      (Content.measure_apply (rieszContent (toNNRealLinear Λ)) (hE.2.2.2 n)).symm (hE' n)
    choose V hV using fun n ↦ exists_open_approx f h_ε' (E n) (h' n) (hE.2.2.2 n) (h n)
    exact ⟨V, hV⟩
-- 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
hE' : ∀ (n : Fin N), Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Fin N → Opens X
hV :
  ∀ (n : Fin N),
    E n ⊆ (↑(V n) : Set X) ∧
      (∀ x ∈ V n, (f : (a : X) → ℝ) x < y n + ε') ∧
        (μ : (a : Set X) → ℝ≥0∞) (↑(V n) : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (E n) : ℝ≥0∞) (ENNReal.ofReal (ε' / (↑N : ℝ)))
h : ∀ (n : Fin N), E n ⊆ (V n).carrier
⊢ Subset.{u_1} (α := Set X) (⋃ (j : Fin N), E j) (⋃ (n : Fin N), (V n).carrier)

Tactic:
gcongr with n