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 :
  ∑' (n : ℕ), HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (δ n) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s i)) (∑' (n : ℕ), δ n)
rw₁ rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), δ a) =
    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∞)

Tactic:
rw [measure_iUnion hsd hsm, ENNReal.tsum_add]

Premises used: ENNReal.tsum_add, 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)
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∞) ε
grw₁ grw₂ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) ε ≤
    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∞) ε

Tactic:
grw [hδε, ENNReal.half_le_self]

Premises used: ENNReal.half_le_self
-- 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
μ₁ :
  ∑' (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∞)
μ₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∑' (n : ℕ), δ n : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), U n) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥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]

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.measure_iUnion_le, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
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
⊢ ∃ K ⊆ U, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K

Tactic:
rcases hU.exists_iUnion_isClosed with ⟨F, F_closed, -, rfl, F_mono⟩

Premises used: IsOpen.exists_iUnion_isClosed, MeasureTheory.Measure.InnerRegularWRT.rfl
-- Module: Mathlib.MeasureTheory.Measure.Regular
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)
⊢ r < ⨆ (i : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F i)

Tactic:
rw [F_mono.measure_iUnion] at hr

Premises used: Monotone.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Regular
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)
rcases :
  ∀ (n : ℕ) (hn : r < (μ : (a : Set X) → ℝ≥0∞) (F n)),
    ∃ K ⊆ ⋃ (n : ℕ), F n, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
⊢ ∃ K ⊆ ⋃ (n : ℕ), F n, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K

Tactic:
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩

Premises used: Iff.mp, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
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)
n : ℕ
hn : r < (μ : (a : Set X) → ℝ≥0∞) (F n)
⊢ ∃ K ⊆ ⋃ (n : ℕ), F n, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K

Tactic:
⟨F n, subset_iUnion _ _, F_closed n, hn⟩

Premises used: Set.subset_iUnion, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
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)
n : ℕ
hn : r < (μ : (a : Set X) → ℝ≥0∞) (F n)
⊢ ∃ K ⊆ ⋃ (n : ℕ), F n, IsClosed[inst] K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K

Tactic:
exact ⟨F n, subset_iUnion _ _, F_closed n, hn⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ ∀ (n : ℕ), IsCompact (F ∩ B n)

Tactic:
have hBc : ∀ n, IsCompact (F ∩ B n) := fun n => (isCompact_compactCovering X n).inter_left hF
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
rw₂ rw₃ : F = F
⊢ ⋃ (n : ℕ), F ∩ B n = F

Tactic:
rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]

Premises used: iUnion_compactCovering, Set.inter_univ, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Regular
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

Tactic:
have hBU : ⋃ n, F ∩ B n = F := by rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
rw : Monotone.{0, u_3} (β := Set X) fun (n : ℕ) ↦ F ∩ B n
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n) : ℝ≥0∞)

Tactic:
rw [← Monotone.measure_iUnion, hBU]

Premises used: Monotone.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ Monotone.{0, u_3} (β := Set X) fun (n : ℕ) ↦ F ∩ B n

Tactic:
monotone_const.inter monotone_accumulate

Premises used: monotone_const, Set.monotone_accumulate, Monotone.inter
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ Monotone.{0, u_3} (β := Set X) fun (n : ℕ) ↦ F ∩ B n

Tactic:
exact monotone_const.inter monotone_accumulate

Premises used: monotone_const, Set.monotone_accumulate, Monotone.inter
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)

Tactic:
have : μ F = ⨆ n, μ (F ∩ B n) := by
    rw [← Monotone.measure_iUnion, hBU]
    exact monotone_const.inter monotone_accumulate
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
⊢ r < ⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)

Tactic:
rw [this] at hr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)
⊢ ∀ (n : ℕ), IsCompact (F ∩ B n)

Tactic:
rw [this] at hr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)
hBc₁ : ∀ (n : ℕ), IsCompact (F ∩ B n)
⊢ ⋃ (n : ℕ), F ∩ B n = F

Tactic:
rw [this] at hr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)
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∞)

Tactic:
rw [this] at hr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
rcases : ∀ (n : ℕ) (hn : r < (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)), ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K
⊢ ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K

Tactic:
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩

Premises used: Iff.mp, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
n : ℕ
hn : r < (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K

Tactic:
⟨_, inter_subset_left, hBc n, hn⟩

Premises used: Set.inter_subset_left, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
n : ℕ
hn : r < (μ : (a : Set X) → ℝ≥0∞) (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < (μ : (a : Set X) → ℝ≥0∞) K

Tactic:
exact ⟨_, inter_subset_left, hBc n, hn⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
U : Set α
hU : MeasurableSet U
μ : Measure α
inst_2 : μ.InnerRegular
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
InnerRegular.innerRegular.measure_eq_iSup hU

Premises used: MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup, MeasureTheory.Measure.InnerRegular.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
⊢ InnerRegular.{u_1} (α := α) 0

Tactic:
⟨fun _ _ _r hr => ⟨∅, empty_subset _, isCompact_empty, hr⟩⟩

Premises used: And.intro, Set.empty_subset, Exists.intro, EmptyCollection.emptyCollection, MeasureTheory.Measure.InnerRegular.mk, isCompact_empty
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegular
c : ℝ≥0∞
⊢ (c • μ).InnerRegular

Tactic:
⟨InnerRegularWRT.smul h.innerRegular c⟩

Premises used: MeasureTheory.Measure.InnerRegularWRT.smul, MeasureTheory.Measure.InnerRegular.innerRegular, MeasureTheory.Measure.InnerRegular.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
c : ℝ≥0
⊢ (c • μ).InnerRegular

Tactic:
smul (c : ℝ≥0∞)

Premises used: ENNReal.ofNNReal, MeasureTheory.Measure.InnerRegular.smul
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
⊢ μ.InnerRegularCompactLTTop

Tactic:
⟨fun _s hs r hr ↦ InnerRegular.innerRegular hs.1 r hr⟩

Premises used: And.left, MeasureTheory.Measure.InnerRegularCompactLTTop.mk, MeasureTheory.Measure.InnerRegular.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
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
⊢ ∃ 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⟩

Premises used: IsOpen.measurableSet, MeasureTheory.Measure.InnerRegular.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : 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:
⟨closure K, K_comp.closure_subset_of_isOpen hU KU, isClosed_closure,
    hK.trans_le (measure_mono subset_closure)⟩

Premises used: subset_closure, closure, IsCompact.closure_subset_of_isOpen, LT.lt.trans_le, And.intro, MeasureTheory.measure_mono, Exists.intro, isClosed_closure
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : 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:
exact ⟨closure K, K_comp.closure_subset_of_isOpen hU KU, isClosed_closure,
    hK.trans_le (measure_mono subset_closure)⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
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∞)
simp_rw₄ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∃ (x : Set α) (_ : x ⊆ univ) (_ : IsCompact x), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₅ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∃ x ⊆ univ, IsCompact x ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₆ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∃ (x : Set α), True ∧ IsCompact x ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥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]

Premises used: Set.subset_univ, MeasurableSet.measure_eq_iSup_isCompact, Ne, exists_prop, ENNReal.iSup_eq_zero, MeasureTheory.Measure.measure_univ_eq_zero, Classical.not_forall, true_and, MeasurableSet.univ