awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 :
  ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2 ≤
    ∑ x ∈ t, HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F x) : ℝ≥0∞) (δ x) + ε / 2
⊢ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2 ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (F k)) (∑ k ∈ t, δ k) + ε / 2

Tactic:
rw [← sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
bc : ∀ i ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F i) : ℝ≥0∞) (δ i)
⊢ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2 ≤
    ∑ x ∈ t, HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F x) : ℝ≥0∞) (δ x) + ε / 2

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
i : ℕ
h : i ∈ t
⊢ (μ : (a : Set α) → ℝ≥0∞) (s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (F i) : ℝ≥0∞) (δ i)

Tactic:
apply hF
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
bc : ∑ k ∈ t, δ k ≤ ε / 2
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (F k)) (∑ k ∈ t, δ k) + ε / 2 ≤
    ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (F k) + ε / 2 + ε / 2

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ ∑ k ∈ t, δ k ≤ ε / 2

Tactic:
(ENNReal.sum_le_tsum _).trans hδε.le

Premises used: LT.lt.le, ENNReal.sum_le_tsum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ ∑ k ∈ t, δ k ≤ ε / 2

Tactic:
exact (ENNReal.sum_le_tsum _).trans hδε.le

Premises used: LT.lt.le, ENNReal.sum_le_tsum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
hd : (↑t : Set ℕ).PairwiseDisjoint F
hm : ∀ b ∈ t, MeasurableSet (F b)
⊢ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (F k) + ε / 2 + ε / 2 =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ k ∈ t, F k) : ℝ≥0∞) ε

Tactic:
rw [measure_biUnion_finset, add_assoc, ENNReal.add_halves]

Premises used: add_assoc, ENNReal.add_halves, MeasureTheory.measure_biUnion_finset
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ (↑t : Set ℕ).PairwiseDisjoint F

Tactic:
fun k _ n _ hkn => (hsd hkn).mono (hFs k) (hFs n)

Premises used: Set.PairwiseDisjoint, Set.Pairwise, Disjoint.mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ ∀ b ∈ t, MeasurableSet (F b)

Tactic:
fun k _ => (hFc k).measurableSet

Premises used: IsClosed.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ (↑t : Set ℕ).PairwiseDisjoint F

Tactic:
exacts [fun k _ n _ hkn => (hsd hkn).mono (hFs k) (hFs n),
            fun k _ => (hFc k).measurableSet]

Premises used: IsClosed.measurableSet, Disjoint.mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
k :
  ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2 ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (F k)) (∑ k ∈ t, δ k) + ε / 2
k₁ :
  HAdd.hAdd (α := ℝ≥0∞) (∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (F k)) (∑ k ∈ t, δ k) + ε / 2 ≤
    ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (F k) + ε / 2 + ε / 2
k₂ :
  ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (F k) + ε / 2 + ε / 2 =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ k ∈ t, F k) : ℝ≥0∞) ε
⊢ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2 ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ k ∈ t, F k) : ℝ≥0∞) ε

Tactic:
calc
        (∑ k ∈ t, μ (s k)) + ε / 2 ≤ ((∑ k ∈ t, μ (F k)) + ∑ k ∈ t, δ k) + ε / 2 := by
          rw [← sum_add_distrib]
          gcongr
          apply hF
        _ ≤ (∑ k ∈ t, μ (F k)) + ε / 2 + ε / 2 := by
          gcongr
          exact (ENNReal.sum_le_tsum _).trans hδε.le
        _ = μ (⋃ k ∈ t, F k) + ε := by
          rw [measure_biUnion_finset, add_assoc, ENNReal.add_halves]
          exacts [fun k _ n _ hkn => (hsd hkn).mono (hFs k) (hFs n),
            fun k _ => (hFc k).measurableSet]

Premises used: HAdd.hAdd, DFunLike.coe, Set.iUnion, Finset.sum
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), U n) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n) : ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (U n))
    (∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n))

Tactic:
ENNReal.tsum_le_tsum hU

Premises used: ENNReal.tsum_le_tsum