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 : 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
⊢ (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
have linarith : (|a| + y n + ε') * μ.real (E n) < (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n) →
  (|a| + y n + ε') * μ.real (E n) - ((|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E 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 : 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
linarith :
  (|a| + y n + ε') * μ.real (E n) < (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n) →
    (|a| + y n + ε') * μ.real (E n) - ((|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)) = 0
⊢ (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
have linarith₁ : (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n) < (|a| + y n + ε') * μ.real (E n) →
  (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n) - (|a| + y n + ε') * μ.real (E n) = 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
Λ : (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, (|a| + y n + ε') * (μ.real (E n) + ε' / (↑N : ℝ)) - |a| * μ.real K =
    ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε')
have this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
Tactic: have (n : Fin N) : (|a| + y n + ε') * μ.real (E n) =
        (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n) := by 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 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) → ℝ)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ n : Fin N, (|a| + y n + ε') * (μ.real (E n) + ε' / (↑N : ℝ)) - |a| * μ.real K =
    ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε')
have calc_5 : ∑ x : Fin N, ((|a| + 2 * ε') * μ.real (E x) + (y x - ε') * μ.real (E x) + (|a| + y x + ε') * (ε' / (↑N : ℝ))) -
    |a| * μ.real K =
  ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε')
Tactic: simp_rw [mul_add, this]
-- 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 + ε') ≤ ε
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) → ℝ)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∑ i : Fin N, (μ : (a : Set X) → ℝ≥0∞) (E i) : ℝ≥0∞)
⊢ ∑ i : Fin N, μ.real (E i) = μ.real K
have simp : ∑ x : Fin N, ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (E x)) =
  ENNReal.toReal (∑ i : Fin N, (μ : (a : Set X) → ℝ≥0∞) (E i))
Tactic: simp only [measureReal_def, 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 + ε') ≤ ε
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) → ℝ)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ i : Fin N, μ.real (E i) = μ.real K
have suffices : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∑ i : Fin N, (μ : (a : Set X) → ℝ≥0∞) (E i) : ℝ≥0∞)
Tactic: suffices h : μ K = ∑ i, (μ (E i)) by
        simp only [measureReal_def, h]
        exact Eq.symm <| ENNReal.toReal_sum <| fun n _ ↦ hE' n
-- 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 + ε') ≤ ε
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) → ℝ)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) : ℝ≥0∞)
    (∑ i : Fin N, (μ : (a : Set X) → ℝ≥0∞) (E i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (j : Fin N), E j) : ℝ≥0∞)
  (∑ i : Fin N, (μ : (a : Set X) → ℝ≥0∞) (E i) : ℝ≥0∞)
Tactic: rw [hE.1]
-- 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 + ε') ≤ ε
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) → ℝ)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (j : Fin N), E j) : ℝ≥0∞)
    (∑ i : Fin N, (μ : (a : Set X) → ℝ≥0∞) (E i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑' (i : Fin N), (μ : (a : Set X) → ℝ≥0∞) (E i)) (∑ i : Fin N, (μ : (a : Set X) → ℝ≥0∞) (E i))
Tactic: rw [measure_iUnion (fun m n hmn ↦ hE.2.1 trivial trivial hmn) hE.2.2.2]
-- 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
ε' : ℝ := (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) → ℝ)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ x : Fin N, ((|a| + 2 * ε') * μ.real (E x) + (y x - ε') * μ.real (E x) + (|a| + y x + ε') * (ε' / (↑N : ℝ))) -
      |a| * μ.real K =
    ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε')
have this₁ : ∑ i : Fin N, μ.real (E i) = μ.real K
Tactic: have : ∑ i, μ.real (E i) = μ.real K := by
      suffices h : μ K = ∑ i, (μ (E i)) by
        simp only [measureReal_def, h]
        exact Eq.symm <| ENNReal.toReal_sum <| fun n _ ↦ hE' n
      dsimp [K]; rw [hE.1]
      rw [measure_iUnion (fun m n hmn ↦ hE.2.1 trivial trivial hmn) hE.2.2.2]
      exact tsum_fintype fun b ↦ μ (E b)
-- 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 + ε') ≤ ε
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) → ℝ)
this_1 : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
this : ∑ i : Fin N, μ.real (E i) = μ.real K
⊢ ∑ x : Fin N, ((|a| + 2 * ε') * μ.real (E x) + (y x - ε') * μ.real (E x) + (|a| + y x + ε') * (ε' / (↑N : ℝ))) -
      |a| * μ.real K =
    ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε')
have calc_5 : (|a| + 2 * ε') * μ.real K + ∑ x : Fin N, (y x - ε') * μ.real (E x) + (∑ i : Fin N, (|a| + y i + ε')) * (ε' / (↑N : ℝ)) -
    |a| * μ.real K =
  ∑ n : Fin N, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / (↑N : ℝ) * ∑ n : Fin N, (|a| + y n + ε')
Tactic: rw [Finset.sum_add_distrib, Finset.sum_add_distrib, ← Finset.mul_sum, this, ← Finset.sum_mul]