awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
⊢ Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
have simp : Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ ∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s) atTop
  (𝓝 (∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) s))
Tactic: simp only [hs, Measure.sum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K
have this : Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
  (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
Tactic: have : Tendsto (fun (a : Finset ι) ↦ ∑ i ∈ a, μ i s) atTop (𝓝 (Measure.sum μ s)) := by
    simp only [hs, Measure.sum_apply]
    exact ENNReal.summable.hasSum
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ ∃ (a : Finset ι), r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
have simp : ∃ (a : Finset ι), r < ∑ c ∈ a, (μ c : (a : Set α) → ℝ≥0∞) s
Tactic: simp only [coe_finsetSum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (a : Finset ι) (ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s),
  ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K
Tactic: obtain ⟨a, ha⟩ : ∃ (a : Finset ι), r < (∑ i ∈ a, μ i) s := by
    simp only [coe_finsetSum, Finset.sum_apply]
    exact ((tendsto_order.1 this).1 r hr).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : Finset ι
ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (K : Set α) (Ks : K ⊆ s) (hK : IsCompact K) (h'K : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases MeasurableSet.exists_lt_isCompact hs ha with ⟨K, Ks, hK, h'K⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : Finset ι
ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ : (a : Set α) → ℝ≥0∞) K
have innerRegular : LE.le (α := ℝ≥0∞) (((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: refine ⟨K, Ks, hK, h'K.trans_le ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ : (a : Set α) → ℝ≥0∞) s
this :
  Tendsto (β := ℝ≥0∞) (fun (a : Finset ι) ↦ (∑ i ∈ a, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((sum μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : Finset ι
ha : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < ((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K
⊢ LE.le (α := ℝ≥0∞) (((∑ i ∈ a, μ i : Measure α) : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
have innerRegular : LE.le (α := ℝ≥0∞) (∑ c ∈ a, (μ c : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: simp only [coe_finsetSum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : T2Space α
inst_4 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ K ⊆ A, IsCompact K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε
have rcases : ∀ (K : Set α) (hKA : K ⊆ A) (hKc : IsCompact K)
  (hK : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε),
  ∃ K ⊆ A, IsCompact K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε
Tactic: rcases hA.exists_isCompact_lt_add h'A hε with ⟨K, hKA, hKc, hK⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : R1Space α
inst_4 : μ.InnerRegularCompactLTTop
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ K ⊆ A, IsCompact K ∧ IsClosed[inst_1] K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε
have rcases : ∀ (K : Set α) (hKA : K ⊆ A) (hKco : IsCompact K) (hKcl : IsClosed[inst_1] K)
  (hK : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε),
  ∃ K ⊆ A, IsCompact K ∧ IsClosed[inst_1] K ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < ε
Tactic: rcases hA.exists_isCompact_isClosed_lt_add h'A hε with ⟨K, hKA, hKco, hKcl, hK⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst_2 : IsFiniteMeasure μ
⊢ μ.InnerRegular
have innerRegular : μ.InnerRegularWRT IsCompact MeasurableSet
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst_2 : IsFiniteMeasure μ
⊢ μ.InnerRegularWRT IsCompact MeasurableSet
have h₁ : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: convert! h.innerRegular with s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
⊢ ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
have rcases : ∀ (V : Set α) (hKV : V ⊇ K) (hVo : IsOpen[inst_1] V)
  (hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
Tactic: rcases hK.exists_open_superset_measure_lt_top μ with ⟨V, hKV, hVo, hμV⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have := Fact.mk hμV
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
have obtain : ∀ (U : Set α) (hKU : K ⊆ U) (hUo : IsOpen[inst_1] U) (hμU : (μ.restrict V : (a : Set α) → ℝ≥0∞) U < r),
  ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
Tactic: obtain ⟨U, hKU, hUo, hμU⟩ : ∃ U, K ⊆ U ∧ IsOpen U ∧ μ.restrict V U < r :=
    exists_isOpen_lt_of_lt K r <| (restrict_apply_le _ _).trans_lt hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ.restrict V : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
have refine : (μ : (a : Set α) → ℝ≥0∞) (U ∩ V) < r
Tactic: refine ⟨U ∩ V, subset_inter hKU hKV, hUo.inter hVo, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ.restrict V : (a : Set α) → ℝ≥0∞) U < r
⊢ (μ : (a : Set α) → ℝ≥0∞) (U ∩ V) < r
have rwa : ∀ (hμU : (μ : (a : Set α) → ℝ≥0∞) (U ∩ V) < r), (μ : (a : Set α) → ℝ≥0∞) (U ∩ V) < r
Tactic: rwa [restrict_apply hUo.measurableSet] at hμU
Cleared hypotheses: hμU
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
have a : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
  (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
a :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
have a₁ : LE.le (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
have a : ∀ (i : Set α) (i_1 : K ⊆ i) (i_2 : IsOpen[inst_1] i),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: simp only [le_iInf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
⊢ LE.le (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
have a : ∀ (c : ℝ≥0∞),
  (μ : (a : Set α) → ℝ≥0∞) K < c →
    ⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U < c
Tactic: apply le_of_forall_gt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
have this : ε / 2 ≠ 0
Tactic: have : ε / 2 ≠ 0 := (ENNReal.half_pos hε).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
have rcases : ∀ (K : Set α) (hKs : K ⊆ s) (hKco : IsCompact K) (hKcl : IsClosed[inst_1] K)
  (hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2),
  ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
Tactic: rcases hs.exists_isCompact_isClosed_diff_lt hμs this with ⟨K, hKs, hKco, hKcl, hμK⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
have rcases : ∀ (U : Set α) (hKU : K ⊆ U) (hUo : IsOpen[inst_1] U)
  (hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)),
  ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
Tactic: rcases hKco.exists_isOpen_lt_add (μ := μ) this with ⟨U, hKU, hUo, hμU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
have refine : (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
Tactic: refine ⟨U, hUo, hμU.trans_le le_top, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ U) : ℝ≥0∞) <
  ε / 2 + ε / 2
Tactic: rw [← ENNReal.add_halves ε, measure_symmDiff_eq hUo.nullMeasurableSet hs.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ U) : ℝ≥0∞) <
    ε / 2 + ε / 2
have xz : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε / 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
xz : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε / 2
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ U) : ℝ≥0∞) <
    ε / 2 + ε / 2
have yw : (μ : (a : Set α) → ℝ≥0∞) (s \ U) < ε / 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ (μ : (a : Set α) → ℝ≥0∞) (U \ K) < ε / 2
have apply : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKU _ hμU
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε / 2
have μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ K) : ℝ≥0∞)
Tactic: calc
      μ (U \ s) ≤ μ (U \ K) := by gcongr
      _ < ε / 2 := by
        apply measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKU _ hμU
        exact ne_top_of_le_ne_top hμs (by gcongr)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ K) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε / 2
have μ₂ : (μ : (a : Set α) → ℝ≥0∞) (U \ K) < ε / 2
Tactic: calc
      μ (U \ s) ≤ μ (U \ K) := by gcongr
      _ < ε / 2 := by
        apply measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKU _ hμU
        exact ne_top_of_le_ne_top hμs (by gcongr)