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∞)
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥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∞) ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) s
r' : ℝ≥0∞
hsr' : (μ : (a : Set α) → ℝ≥0∞) s < r'
hr'r : r' < r
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
H :
  (μ : (a : Set α) → ℝ≥0∞) U ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (HSub.hSub (β := ℝ≥0∞) r' ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
⊢ ∃ U ⊇ s, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
have refine : (μ : (a : Set α) → ℝ≥0∞) U < r
Tactic: refine ⟨U, hsU, hUo, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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∞)
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥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∞) ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) s
r' : ℝ≥0∞
hsr' : (μ : (a : Set α) → ℝ≥0∞) s < r'
hr'r : r' < r
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
H :
  (μ : (a : Set α) → ℝ≥0∞) U ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (HSub.hSub (β := ℝ≥0∞) r' ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
⊢ (μ : (a : Set α) → ℝ≥0∞) U < r
have H₁ : (μ : (a : Set α) → ℝ≥0∞) U ≤ r'
Tactic: rw [add_tsub_cancel_of_le hsr'.le] at H
Cleared hypotheses: H
-- 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 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.WeaklyRegular
have suffices : ∀ (s : Set α),
  MeasurableSet s →
    ∀ (ε : ℝ≥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∞) ε
Tactic: suffices ∀ s, MeasurableSet s → ∀ ε, ε ≠ 0 → ∃ F, F ⊆ s ∧ ∃ U, U ⊇ s ∧
      IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε by
    refine
      { outerRegular := fun s hs r hr => ?_
        innerRegular := H }
    rcases exists_between hr with ⟨r', hsr', hr'r⟩
    rcases this s hs _ (tsub_pos_iff_lt.2 hsr').ne' with ⟨-, -, U, hsU, -, hUo, -, H⟩
    refine ⟨U, hsU, hUo, ?_⟩
    rw [add_tsub_cancel_of_le hsr'.le] at H
    exact H.trans_lt hr'r
-- 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 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥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∞) ε
have isOpen : ∀ (U : Set α) (hU : IsOpen[inst_1] U) (ε : ℝ≥0∞),
  ε ≠ 0 →
    ∃ F ⊆ U,
      ∃ U_1 ⊇ U,
        IsClosed[inst_1] F ∧
          IsOpen[inst_1] U_1 ∧
            (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
              (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε
Tactic: apply MeasurableSet.induction_on_open
-- 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 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
isOpen :
  ∀ (U : Set α) (hU : IsOpen[inst_1] U) (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ U,
        ∃ U_1 ⊇ U,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U_1 ∧
              (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥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∞) ε
have compl : ∀ (t : Set α) (ht : MeasurableSet t),
  (∀ (ε : ℝ≥0∞),
      ε ≠ 0 →
        ∃ F ⊆ t,
          ∃ U ⊇ t,
            IsClosed[inst_1] F ∧
              IsOpen[inst_1] U ∧
                (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                  (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε) →
    ∀ (ε : ℝ≥0∞),
      ε ≠ 0 →
        ∃ F ⊆ tᶜ,
          ∃ U ⊇ tᶜ,
            IsClosed[inst_1] F ∧
              IsOpen[inst_1] U ∧
                (μ : (a : Set α) → ℝ≥0∞) tᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                  (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ε
Tactic: apply MeasurableSet.induction_on_open
-- 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 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
isOpen :
  ∀ (U : Set α) (hU : IsOpen[inst_1] U) (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ U,
        ∃ U_1 ⊇ U,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U_1 ∧
              (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε
compl :
  ∀ (t : Set α) (ht : MeasurableSet t),
    (∀ (ε : ℝ≥0∞),
        ε ≠ 0 →
          ∃ F ⊆ t,
            ∃ U ⊇ t,
              IsClosed[inst_1] F ∧
                IsOpen[inst_1] U ∧
                  (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                    (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε) →
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 →
          ∃ F ⊆ tᶜ,
            ∃ U ⊇ tᶜ,
              IsClosed[inst_1] F ∧
                IsOpen[inst_1] U ∧
                  (μ : (a : Set α) → ℝ≥0∞) tᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                    (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ε
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥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∞) ε
have iUnion : ∀ (f : ℕ → Set α),
  Pairwise (Function.onFun Disjoint f) →
    ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)),
      (∀ (i : ℕ) (ε : ℝ≥0∞),
          ε ≠ 0 →
            ∃ F ⊆ f i,
              ∃ U ⊇ f i,
                IsClosed[inst_1] F ∧
                  IsOpen[inst_1] U ∧
                    (μ : (a : Set α) → ℝ≥0∞) (f i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                      (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) ε) →
        ∀ (ε : ℝ≥0∞),
          ε ≠ 0 →
            ∃ F ⊆ ⋃ (i : ℕ), f i,
              ∃ U ⊇ ⋃ (i : ℕ), f i,
                IsClosed[inst_1] F ∧
                  IsOpen[inst_1] U ∧
                    (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) ≤
                        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                      (μ : (a : Set α) → ℝ≥0∞) U ≤
                        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) ε
Tactic: apply MeasurableSet.induction_on_open
-- 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 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
hU : IsOpen[inst_1] U
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ F ⊆ U,
    ∃ U_1 ⊇ U,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U_1 ∧
          (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε
have isOpen : ∀ (F : Set α) (hsF : F ⊆ U) (hFc : IsClosed[inst_1] F)
  (hF : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε),
  ∃ F ⊆ U,
    ∃ U_1 ⊇ U,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U_1 ∧
          (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε
Tactic: rcases H.exists_subset_lt_add isClosed_empty hU hfin hε with ⟨F, hsF, hFc, hF⟩
-- 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 α
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 ⊆ 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∞) ε
have compl : ∀ (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: rcases H ε hε with ⟨F, hFs, U, hsU, hFc, hUo, hF, hU⟩
-- 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 α
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∞) ε
have 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∞) ε
Tactic: refine
      ⟨Uᶜ, compl_subset_compl.2 hsU, Fᶜ, compl_subset_compl.2 hFs, hUo.isClosed_compl,
        hFc.isOpen_compl, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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
⊢ ∃ 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∞) ε
have ε0' : ε / 2 ≠ 0
Tactic: have ε0' : ε / 2 ≠ 0 := (ENNReal.half_pos ε0).ne'
-- 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
⊢ ∃ 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∞) ε
have 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∞) ε
Tactic: rcases ENNReal.exists_pos_sum_of_countable' ε0' ℕ with ⟨δ, δ0, hδε⟩
-- 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 ⊆ ⋃ (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∞) ε
have 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∞) ε
Tactic: choose F hFs U hsU hFc hUo hF hU using fun n => H n (δ n) (δ0 n).ne'
-- 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)
⊢ Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
    (𝓝 (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (ε / 2)))
have rw : Tendsto (fun (t : Finset ℕ) ↦ ∑ k ∈ t, (μ : (a : Set α) → ℝ≥0∞) (s k) + ε / 2) atTop
  (𝓝 (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i) + ε / 2))
Tactic: rw [measure_iUnion hsd hsm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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)
⊢ ∃ 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∞) ε
have 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)))
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