awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ s i,
        ∃ U ⊇ s i,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U ∧
              (μ : (a : Set α) → ℝ≥0∞) (s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : (n : ℕ) → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : (n : ℕ) → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst_1] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hF : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F n) : ℝ≥0∞) (δ n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n)
this :
  Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2)))
t : Finset ℕ
ht : (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) < ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2
⊢ ∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞)
have rw : ∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n) =
  HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i)) (∑' (n : ℕ), δ n)
Tactic: rw [measure_iUnion hsd hsm, ENNReal.tsum_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ s i,
        ∃ U ⊇ s i,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U ∧
              (μ : (a : Set α) → ℝ≥0∞) (s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : (n : ℕ) → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : (n : ℕ) → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst_1] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hF : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F n) : ℝ≥0∞) (δ n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n)
this :
  Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2)))
t : Finset ℕ
ht : (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) < ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2
rw :
  ∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i)) (∑' (n : ℕ), δ n)
⊢ ∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞)
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), δ a) =
  HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i)) (∑' (n : ℕ), δ n)
Tactic: rw [measure_iUnion hsd hsm, ENNReal.tsum_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ s i,
        ∃ U ⊇ s i,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U ∧
              (μ : (a : Set α) → ℝ≥0∞) (s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : (n : ℕ) → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : (n : ℕ) → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst_1] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hF : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F n) : ℝ≥0∞) (δ n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n)
this :
  Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2)))
t : Finset ℕ
ht : (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) < ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) ε
have grw : HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2) ≤
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) ε
Tactic: grw [hδε, ENNReal.half_le_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ s i,
        ∃ U ⊇ s i,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U ∧
              (μ : (a : Set α) → ℝ≥0∞) (s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : (n : ℕ) → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : (n : ℕ) → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst_1] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hF : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F n) : ℝ≥0∞) (δ n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n)
this :
  Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2)))
t : Finset ℕ
ht : (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) < ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2
grw :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) ε
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) ε
have grw₁ : HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) ε ≤
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) ε
Tactic: grw [hδε, ENNReal.half_le_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ s i,
        ∃ U ⊇ s i,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U ∧
              (μ : (a : Set α) → ℝ≥0∞) (s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : (n : ℕ) → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : (n : ℕ) → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst_1] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hF : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F n) : ℝ≥0∞) (δ n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n)
this :
  Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2)))
t : Finset ℕ
ht : (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) < ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2
⊢ (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε
have μ₁ : ∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞)
Tactic: calc
        μ (⋃ n, U n) ≤ ∑' n, μ (U n) := measure_iUnion_le _
        _ ≤ ∑' n, (μ (s n) + δ n) := ENNReal.tsum_le_tsum hU
        _ = μ (⋃ n, s n) + ∑' n, δ n := by rw [measure_iUnion hsd hsm, ENNReal.tsum_add]
        _ ≤ μ (⋃ n, s n) + ε := by grw [hδε, ENNReal.half_le_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : ℕ → Set α
hsd : Pairwise (Function.onFun Disjoint s)
hsm : ∀ (i : ℕ), MeasurableSet (s i)
H :
  ∀ (i : ℕ) (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ s i,
        ∃ U ⊇ s i,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U ∧
              (μ : (a : Set α) → ℝ≥0∞) (s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
ε0' : ε / 2 ≠ 0
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < ε / 2
F : (n : ℕ) → Set α
hFs : ∀ (n : ℕ), F n ⊆ s n
U : (n : ℕ) → Set α
hsU : ∀ (n : ℕ), U n ⊇ s n
hFc : ∀ (n : ℕ), IsClosed[inst_1] (F n)
hUo : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hF : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F n) : ℝ≥0∞) (δ n)
hU : ∀ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n)
this :
  Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2)))
t : Finset ℕ
ht : (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) < ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2
μ₁ :
  ∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε
have μ₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) ε
Tactic: calc
        μ (⋃ n, U n) ≤ ∑' n, μ (U n) := measure_iUnion_le _
        _ ≤ ∑' n, (μ (s n) + δ n) := ENNReal.tsum_le_tsum hU
        _ = μ (⋃ n, s n) + ∑' n, δ n := by rw [measure_iUnion hsd hsm, ENNReal.tsum_add]
        _ ≤ μ (⋃ n, s n) + ε := by grw [hδε, ENNReal.half_le_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
inst_2 : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
U : Set X
hU : IsOpen[inst] U
r : ℝ≥0∞
hr : r < (μ : (a : Set X) → ℝ≥0∞) U
⊢ ∃ K ⊆ U, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
have rcases : ∀ (F : ℕ → Set X) (F_closed : ∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n))
  (F_mono : Monotone F) (hU : IsOpen[inst] (⋃ (n : ℕ), F n)) (hr : r < (μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), F n)),
  ∃ K ⊆ ⋃ (n : ℕ), F n, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
Tactic: rcases hU.exists_iUnion_isClosed with ⟨F, F_closed, -, rfl, F_mono⟩
Cleared hypotheses: U, hU, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
inst_2 : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)
F_mono : Monotone F
hU : IsOpen[inst] (⋃ (n : ℕ), F n)
hr : r < (μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), F n)
⊢ ∃ K ⊆ ⋃ (n : ℕ), F n, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
have hr₁ : r < ⨆ (i : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F i)
Tactic: rw [F_mono.measure_iUnion] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
inst_2 : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
r : ℝ≥0∞
F : ℕ → Set X
F_closed : ∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)
F_mono : Monotone F
hU : IsOpen[inst] (⋃ (n : ℕ), F n)
hr : r < ⨆ (i : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F i)
⊢ ∃ K ⊆ ⋃ (n : ℕ), F n, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
have rcases : ∀ (n : ℕ) (hn : r < (μ : (a : Set X) → ℝ≥0∞) (F n)),
  ∃ K ⊆ ⋃ (n : ℕ), F n, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
Tactic: rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
inst_2 : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst] F
r : ℝ≥0∞
hr : r < (μ : (a : Set X) → ℝ≥0∞) F
B : ℕ → Set X := compactCovering X
⊢ ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
have hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
Tactic: have hBc : ∀ n, IsCompact (F ∩ B n) := fun n => (isCompact_compactCovering X n).inter_left hF
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
inst_2 : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst] F
r : ℝ≥0∞
hr : r < (μ : (a : Set X) → ℝ≥0∞) F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ⋃ (n : ℕ), F ∩ B n = F
have rw : F ∩ ⋃ (i : ℕ), B i = F
Tactic: rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
inst_2 : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst] F
r : ℝ≥0∞
hr : r < (μ : (a : Set X) → ℝ≥0∞) F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
rw : F ∩ ⋃ (i : ℕ), B i = F
⊢ ⋃ (n : ℕ), F ∩ B n = F
have rw₁ : F ∩ univ = F
Tactic: rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
inst_2 : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst] F
r : ℝ≥0∞
hr : r < (μ : (a : Set X) → ℝ≥0∞) F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
rw : F ∩ ⋃ (i : ℕ), B i = F
rw₁ : F ∩ univ = F
⊢ ⋃ (n : ℕ), F ∩ B n = F
have rw₂ : F = F
Tactic: rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
inst_2 : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst] F
r : ℝ≥0∞
hr : r < (μ : (a : Set X) → ℝ≥0∞) F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
have hBU : ⋃ (n : ℕ), F ∩ B n = F
Tactic: have hBU : ⋃ n, F ∩ B n = F := by rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
inst_2 : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst] F
r : ℝ≥0∞
hr : r < (μ : (a : Set X) → ℝ≥0∞) F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ (n : ℕ), F ∩ B n = F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n) : ℝ≥0∞)
have rw : Monotone.{0, u_3} (β := Set X) fun (n : ℕ) ↦ F ∩ B n
Tactic: rw [← Monotone.measure_iUnion, hBU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
inst_2 : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst] F
r : ℝ≥0∞
hr : r < (μ : (a : Set X) → ℝ≥0∞) F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ (n : ℕ), F ∩ B n = F
⊢ ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
have this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n) : ℝ≥0∞)
Tactic: have : μ F = ⨆ n, μ (F ∩ B n) := by
    rw [← Monotone.measure_iUnion, hBU]
    exact monotone_const.inter monotone_accumulate
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
inst_2 : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst] F
r : ℝ≥0∞
hr : r < (μ : (a : Set X) → ℝ≥0∞) F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ (n : ℕ), F ∩ B n = F
this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n) : ℝ≥0∞)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
have hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)
Tactic: rw [this] at hr
Cleared hypotheses: hr, hBc, hBU, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : SigmaCompactSpace X
inst_2 : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst] F
r : ℝ≥0∞
B : ℕ → Set X := compactCovering X
hr : r < ⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ (n : ℕ), F ∩ B n = F
this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n) : ℝ≥0∞)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
have rcases : ∀ (n : ℕ) (hn : r < (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)), ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
Tactic: rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
inst_3 : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
hU : IsOpen[inst_1] U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) U
⊢ ∃ K ⊆ U, IsClosed[inst_1] K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have rcases : ∀ (K : Set α) (KU : K ⊆ U) (K_comp : IsCompact K) (hK : r < (μ : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ U, IsClosed[inst_1] K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases h.innerRegular hU.measurableSet r hr with ⟨K, KU, K_comp, hK⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, MeasurableSet.univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have simp_rw₁ : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, MeasurableSet.univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
simp_rw₁ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have simp_rw₂ : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ¬Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), (μ : (a : Set α) → ℝ≥0∞) K) 0
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, MeasurableSet.univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
simp_rw₁ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), (μ : (a : Set α) → ℝ≥0∞) K) 0
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have simp_rw₃ : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ¬∀ (i : Set α) (i_1 : i ⊆ univ) (i_2 : IsCompact i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, MeasurableSet.univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]