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
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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
n : Fin N
⊢ @Integrable ℝ _ _ _ inst_2 (fun (x : X) ↦ (f : (a : X) → ℝ) x) (rieszContent (toNNRealLinear Λ)).measure

Tactic:
Continuous.integrable_of_hasCompactSupport f.1.2 f.2

Premises used: Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap, ContinuousMap.continuous_toFun, CompactlySupportedContinuousMap.hasCompactSupport'
-- 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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
n : Fin N
⊢ @Integrable ℝ _ _ _ inst_2 (fun (x : X) ↦ (f : (a : X) → ℝ) x) (rieszContent (toNNRealLinear Λ)).measure

Tactic:
exact Continuous.integrable_of_hasCompactSupport f.1.2 f.2

Premises used: Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap, ContinuousMap.continuous_toFun, CompactlySupportedContinuousMap.hasCompactSupport'
-- 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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
⊢ ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ

Tactic:
have h : ∀ n, (y n - ε') * μ.real (E n) ≤ ∫ x in (E n), f x ∂μ := by
      intro n
      apply setIntegral_ge_of_const_le_real (hE.2.2.2 n) (hE' n)
      · intro x hx
        dsimp [y]; linarith [(hE.2.2.1 n x hx).1]
      · apply Integrable.integrableOn
        dsimp [μ, rieszMeasure]
        exact Continuous.integrable_of_hasCompactSupport f.1.2 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∞)
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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ
⊢ LE.le (α := ℝ) (∑ i : Fin N, (y i - ε') * μ.real (E i)) (∑ n : Fin N, ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ)

Tactic:
Finset.sum_le_sum fun i a ↦ h i

Premises used: Finset.sum_le_sum
-- 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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ
⊢ Eq (α := ℝ) (∑ n : Fin N, ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ)
    (∫ (x : X) in ⋃ (n : Fin N), E n, (f : (a : X) → ℝ) x ∂μ)

Tactic:
Eq.symm <| integral_iUnion_fintype hE.2.2.2 (fun _ _ ↦ hE.2.1 trivial trivial) ?_

Premises used: trivial, And.right, And.left, Eq.symm, MeasureTheory.integral_iUnion_fintype
-- 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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ
refine : ∀ (i : Fin N), IntegrableOn (ε := ℝ) (⇑f : (a : X) → ℝ) (E i) μ
⊢ Eq (α := ℝ) (∑ n : Fin N, ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ)
    (∫ (x : X) in ⋃ (n : Fin N), E n, (f : (a : X) → ℝ) x ∂μ)

Tactic:
refine Eq.symm <| integral_iUnion_fintype hE.2.2.2 (fun _ _ ↦ hE.2.1 trivial trivial) ?_

Premises used: trivial, And.right, And.left, Eq.symm, MeasureTheory.integral_iUnion_fintype
-- 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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ
dsimp :
  ∀ (i : Fin N), IntegrableOn (ε := ℝ) (mα := inst_2) (⇑f : (a : X) → ℝ) (E i) (rieszContent (toNNRealLinear Λ)).measure
⊢ ∀ (i : Fin N), IntegrableOn (ε := ℝ) (⇑f : (a : X) → ℝ) (E i) μ

Tactic:
dsimp [μ, rieszMeasure]

Premises used: RealRMK.rieszMeasure
-- 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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ
⊢ ∀ (i : Fin N), IntegrableOn (ε := ℝ) (mα := inst_2) (⇑f : (a : X) → ℝ) (E i) (rieszContent (toNNRealLinear Λ)).measure

Tactic:
fun _ ↦
          Integrable.integrableOn <| Continuous.integrable_of_hasCompactSupport f.1.2 f.2

Premises used: Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap, ContinuousMap.continuous_toFun, CompactlySupportedContinuousMap.hasCompactSupport', MeasureTheory.Integrable.integrableOn
-- 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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ
⊢ ∀ (i : Fin N), IntegrableOn (ε := ℝ) (mα := inst_2) (⇑f : (a : X) → ℝ) (E i) (rieszContent (toNNRealLinear Λ)).measure

Tactic:
exact fun _ ↦
          Integrable.integrableOn <| Continuous.integrable_of_hasCompactSupport f.1.2 f.2

Premises used: Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap, ContinuousMap.continuous_toFun, CompactlySupportedContinuousMap.hasCompactSupport', MeasureTheory.Integrable.integrableOn
-- 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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ
⊢ Eq (α := ℝ) (∫ (x : X) in ⋃ (n : Fin N), E n, (f : (a : X) → ℝ) x ∂μ)
    (∫ (x : X) in tsupport (α := ℝ) (⇑f : (a : X) → ℝ), (f : (a : X) → ℝ) x ∂μ)

Tactic:
simp_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
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 : ℝ)))
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport (α := ℝ) (⇑(g n) : (a : X) → ℝ) ⊆ (V n).carrier) ∧
    EqOn (β := ℝ) (∑ n : Fin N, (⇑(g n) : (a : X) → ℝ)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((g n : (a : X) → ℝ) x : ℝ)) ∧
        ∀ (n : Fin N), HasCompactSupport (α := X) (β := ℝ) (⇑(g n) : (a : X) → ℝ)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, (f : (a : X) → ℝ) x ∂μ
⊢ Eq (α := ℝ) (∫ (x : X) in tsupport (α := ℝ) (⇑f : (a : X) → ℝ), (f : (a : X) → ℝ) x ∂μ)
    (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)

Tactic:
setIntegral_tsupport

Premises used: MeasureTheory.setIntegral_tsupport