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 α
hs : MeasurableSet s
H :
  ∀ (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ s,
        ∃ U ⊇ s,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U ∧
              (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFs : F ⊆ s
U : Set α
hsU : U ⊇ s
hFc : IsClosed[inst_1] F
hUo : IsOpen[inst_1] U
hF : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε
hU : (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ ∃ F ⊆ sᶜ,
    ∃ U ⊇ sᶜ,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U ∧
          (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) ε

Tactic:
⟨Uᶜ, compl_subset_compl.2 hsU, Fᶜ, compl_subset_compl.2 hFs, hUo.isClosed_compl,
        hFc.isOpen_compl, ?_⟩

Premises used: Iff.mpr, IsClosed.isOpen_compl, Compl.compl, Set.compl_subset_compl, IsOpen.isClosed_compl, And.intro, Exists.intro
-- 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 α
hs : MeasurableSet s
H :
  ∀ (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ s,
        ∃ U ⊇ s,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U ∧
              (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFs : F ⊆ s
U : Set α
hsU : U ⊇ s
hFc : IsClosed[inst_1] F
hUo : IsOpen[inst_1] U
hF : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε
hU : (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
compl :
  (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Uᶜ : ℝ≥0∞) ε ∧
    (μ : (a : Set α) → ℝ≥0∞) Fᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) ε
⊢ ∃ F ⊆ sᶜ,
    ∃ U ⊇ sᶜ,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U ∧
          (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) ε

Tactic:
refine
      ⟨Uᶜ, compl_subset_compl.2 hsU, Fᶜ, compl_subset_compl.2 hFs, hUo.isClosed_compl,
        hFc.isOpen_compl, ?_⟩
-- 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 α
hs : MeasurableSet s
H :
  ∀ (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ s,
        ∃ U ⊇ s,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U ∧
              (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFs : F ⊆ s
U : Set α
hsU : U ⊇ s
hFc : IsClosed[inst_1] F
hUo : IsOpen[inst_1] U
hF : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε
hU : (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Uᶜ : ℝ≥0∞) ε ∧
    (μ : (a : Set α) → ℝ≥0∞) Fᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) ε

Tactic:
simp only [measure_compl_le_add_iff, *, hUo.measurableSet, hFc.measurableSet, true_and]

Premises used: MeasureTheory.measure_compl_le_add_iff, IsClosed.measurableSet, IsOpen.measurableSet, true_and
-- 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
⊢ ε / 2 ≠ 0

Tactic:
have ε0' : ε / 2 ≠ 0 := (ENNReal.half_pos ε0).ne'
-- 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
iUnion :
  ∀ (δ : ℕ → ℝ≥0∞) (δ0 : ∀ (i : ℕ), 0 < δ i) (hδε : ∑' (i : ℕ), δ i < ε / 2),
    ∃ F ⊆ ⋃ (i : ℕ), s i,
      ∃ U ⊇ ⋃ (i : ℕ), s i,
        IsClosed[inst_1] F ∧
          IsOpen[inst_1] U ∧
            (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
              (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε
⊢ ∃ F ⊆ ⋃ (i : ℕ), s i,
    ∃ U ⊇ ⋃ (i : ℕ), s i,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U ∧
          (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε

Tactic:
rcases ENNReal.exists_pos_sum_of_countable' ε0' ℕ with ⟨δ, δ0, hδε⟩

Premises used: ENNReal.exists_pos_sum_of_countable', Nat
-- 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
iUnion :
  ∀ (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)),
    ∃ F ⊆ ⋃ (i : ℕ), s i,
      ∃ U ⊇ ⋃ (i : ℕ), s i,
        IsClosed[inst_1] F ∧
          IsOpen[inst_1] U ∧
            (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
              (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε
⊢ ∃ F ⊆ ⋃ (i : ℕ), s i,
    ∃ U ⊇ ⋃ (i : ℕ), s i,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U ∧
          (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε

Tactic:
choose F hFs U hsU hFc hUo hF hU using fun n => H n (δ n) (δ0 n).ne'

Premises used: LT.lt.ne'
-- 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)
rw :
  Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i) + ε / 2))
⊢ Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2)))

Tactic:
rw [measure_iUnion hsd hsm]

Premises used: MeasureTheory.measure_iUnion
-- 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)
⊢ Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i) + ε / 2))

Tactic:
Tendsto.add ENNReal.summable.hasSum tendsto_const_nhds

Premises used: tendsto_const_nhds, ENNReal.summable, Summable.hasSum, Filter.Tendsto.add
-- 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)
⊢ Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i) + ε / 2))

Tactic:
exact Tendsto.add ENNReal.summable.hasSum tendsto_const_nhds

Premises used: tendsto_const_nhds, ENNReal.summable, Summable.hasSum, Filter.Tendsto.add
-- 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)
⊢ Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2)))

Tactic:
have : Tendsto (fun t => (∑ k ∈ t, μ (s k)) + ε / 2) atTop (𝓝 <| μ (⋃ n, s n) + ε / 2) := by
      rw [measure_iUnion hsd hsm]
      exact Tendsto.add ENNReal.summable.hasSum tendsto_const_nhds
-- 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)))
iUnion :
  ∀ (t : Finset ℕ) (ht : (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) < ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2),
    ∃ F ⊆ ⋃ (i : ℕ), s i,
      ∃ U ⊇ ⋃ (i : ℕ), s i,
        IsClosed[inst_1] F ∧
          IsOpen[inst_1] U ∧
            (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
              (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε
⊢ ∃ F ⊆ ⋃ (i : ℕ), s i,
    ∃ U ⊇ ⋃ (i : ℕ), s i,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U ∧
          (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε

Tactic:
rcases (this.eventually <| lt_mem_nhds <| ENNReal.lt_add_right hfin ε0').exists with ⟨t, ht⟩

Premises used: ENNReal.lt_add_right, Filter.Eventually.exists, Filter.Tendsto.eventually, lt_mem_nhds
-- 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
⊢ ∃ F ⊆ ⋃ (i : ℕ), s i,
    ∃ U ⊇ ⋃ (i : ℕ), s i,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U ∧
          (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε

Tactic:
⟨⋃ k ∈ t, F k, iUnion_mono fun k => iUnion_subset fun _ => hFs _, ⋃ n, U n, iUnion_mono hsU,
        isClosed_biUnion_finset fun k _ => hFc k, isOpen_iUnion hUo, ht.le.trans ?_, ?_⟩

Premises used: Set.iUnion_subset, LT.lt.le, isOpen_iUnion, And.intro, Exists.intro, Set.iUnion_mono, LE.le.trans, isClosed_biUnion_finset, Set.iUnion
-- 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
iUnion :
  ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2 ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ k ∈ t, F k) : ℝ≥0∞) ε
iUnion₁ :
  (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε
⊢ ∃ F ⊆ ⋃ (i : ℕ), s i,
    ∃ U ⊇ ⋃ (i : ℕ), s i,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U ∧
          (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ε

Tactic:
refine
      ⟨⋃ k ∈ t, F k, iUnion_mono fun k => iUnion_subset fun _ => hFs _, ⋃ n, U n, iUnion_mono hsU,
        isClosed_biUnion_finset fun k _ => hFc k, isOpen_iUnion hUo, ht.le.trans ?_, ?_⟩