awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NullMeasurableSet 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 rcases : ∀ (t : Set α) (htm : MeasurableSet t) (hst : s =ᶠ[ae μ] t),
  ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
Tactic: rcases hs with ⟨t, htm, hst⟩
Cleared hypotheses: hs
-- 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 α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
have rcases : ∀ (U : Set α) (hUo : IsOpen[inst_1] U) (hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hUs : (μ : (a : Set α) → ℝ≥0∞) (U ∆ t) < ε),
  ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
Tactic: rcases htm.exists_isOpen_symmDiff_lt (by rwa [← measure_congr hst]) hε with ⟨U, hUo, hμU, hUs⟩
-- 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 α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
U : Set α
hUo : IsOpen[inst_1] U
hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hUs : (μ : (a : Set α) → ℝ≥0∞) (U ∆ t) < ε
⊢ ∃ (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, ?_⟩
-- 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
c : ℝ≥0∞
⊢ (c • μ).InnerRegularCompactLTTop
have pos : ∀ (hc : c = 0), (c • μ).InnerRegularCompactLTTop
Tactic: by_cases hc : c = 0
-- 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
c : ℝ≥0∞
pos : ∀ (hc : c = 0), (c • μ).InnerRegularCompactLTTop
⊢ (c • μ).InnerRegularCompactLTTop
have neg : ∀ (hc : ¬c = 0), (c • μ).InnerRegularCompactLTTop
Tactic: by_cases hc : c = 0
-- 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
c : ℝ≥0∞
hc : c = 0
⊢ (c • μ).InnerRegularCompactLTTop
have pos : InnerRegularCompactLTTop.{u_1} (α := α) 0
Tactic: simp only [hc, zero_smul]
-- 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
c : ℝ≥0∞
hc : ¬c = 0
⊢ (c • μ).InnerRegularCompactLTTop
have pos : ∀ (h'c : c = ∞), (c • μ).InnerRegularCompactLTTop
Tactic: by_cases h'c : c = ∞
-- 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
c : ℝ≥0∞
hc : ¬c = 0
pos : ∀ (h'c : c = ∞), (c • μ).InnerRegularCompactLTTop
⊢ (c • μ).InnerRegularCompactLTTop
have neg : ∀ (h'c : ¬c = ∞), (c • μ).InnerRegularCompactLTTop
Tactic: by_cases h'c : c = ∞
-- 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
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
⊢ (c • μ).InnerRegularCompactLTTop
have pos : (c • μ).InnerRegularWRT IsCompact fun (s : Set α) ↦
  MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
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
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
s : Set α
hs : MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (c • μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (c • μ : (a : Set α) → ℝ≥0∞) K
have pos : ∀ (h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ K ⊆ s, IsCompact K ∧ r < (c • μ : (a : Set α) → ℝ≥0∞) K
Tactic: by_cases h's : μ s = 0
-- 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
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
s : Set α
hs : MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (c • μ : (a : Set α) → ℝ≥0∞) s
pos :
  ∀ (h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ s, IsCompact K ∧ r < (c • μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (c • μ : (a : Set α) → ℝ≥0∞) K
have neg : ∀ (h's : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ K ⊆ s, IsCompact K ∧ r < (c • μ : (a : Set α) → ℝ≥0∞) K
Tactic: by_cases h's : μ s = 0
-- 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
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
⊢ (c • μ).InnerRegularCompactLTTop
have neg : (c • μ).InnerRegularWRT IsCompact fun (s : Set α) ↦
  MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
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
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
⊢ (c • μ).InnerRegularWRT IsCompact fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have h₁ : ∀ (s : Set α),
  MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: convert! InnerRegularWRT.smul h.innerRegular c using 2 with s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
s : Set α
⊢ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have : (c • μ) s ≠ ∞ ↔ μ s ≠ ∞ := by simp [ENNReal.mul_eq_top, hc, h'c]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous[inst_1, inst_4] f
⊢ InnerRegularCompactLTTop (map f μ)
have innerRegular : @InnerRegularWRT _ inst_3 (map f μ) IsCompact fun (s : Set β) ↦
  MeasurableSet s ∧ Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
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 α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous[inst_1, inst_4] f
⊢ @InnerRegularWRT _ inst_3 (map f μ) IsCompact fun (s : Set β) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have innerRegular : ∀ (U : Set β),
  MeasurableSet U ∧ Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) →
    MeasurableSet (f ⁻¹' U) ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine InnerRegularWRT.map h.innerRegular hf.aemeasurable ?_ (fun K hK ↦ hK.image hf) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous[inst_1, inst_4] f
innerRegular :
  ∀ (U : Set β),
    MeasurableSet U ∧ Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) →
      MeasurableSet (f ⁻¹' U) ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ @InnerRegularWRT _ inst_3 (map f μ) IsCompact fun (s : Set β) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have innerRegular₁ : ∀ (U : Set β),
  MeasurableSet U ∧ Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) → MeasurableSet U
Tactic: refine InnerRegularWRT.map h.innerRegular hf.aemeasurable ?_ (fun K hK ↦ hK.image hf) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous[inst_1, inst_4] f
s : Set β
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rwa : ∀ (h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [map_apply hf.measurable hs] at h's
Cleared hypotheses: h's
-- 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 : μ.WeaklyRegular
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ F ⊆ A, IsClosed[inst_1] F ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ F) < ε
have rcases : ∀ (F : Set α) (hFA : F ⊆ A) (hFc : IsClosed[inst_1] F)
  (hF : (μ : (a : Set α) → ℝ≥0∞) A < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε),
  ∃ F ⊆ A, IsClosed[inst_1] F ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ F) < ε
Tactic: rcases hA.exists_isClosed_lt_add h'A hε with ⟨F, hFA, hFc, hF⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : μ.WeaklyRegular
A : Set α
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ.restrict A).WeaklyRegular
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: haveI : Fact (μ A < ∞) := ⟨h'A.lt_top⟩
-- 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 : μ.WeaklyRegular
A : Set α
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ (μ.restrict A).WeaklyRegular
have refine : ∀ (V : Set α) (V_open : IsOpen[inst_1] V) (r : ℝ≥0∞) (hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) V),
  ∃ K ⊆ V, IsClosed[inst_1] K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
Tactic: refine InnerRegularWRT.weaklyRegular_of_finite (μ.restrict A) (fun V V_open r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : μ.WeaklyRegular
A : Set α
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set α
V_open : IsOpen[inst_1] V
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) V
⊢ ∃ K ⊆ V, IsClosed[inst_1] K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
have this₁ : (μ.restrict A).InnerRegularWRT IsClosed[inst_1] fun (s : Set α) ↦ MeasurableSet s
Tactic: have : InnerRegularWRT (μ.restrict A) IsClosed (fun s ↦ MeasurableSet s) :=
    InnerRegularWRT.restrict_of_measure_ne_top innerRegular_measurable h'A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
X : Type u_3
inst_2 : TopologicalSpace X
inst_3 : PseudoMetrizableSpace X
inst_4 : SecondCountableTopology X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
μ : Measure X
inst_7 : IsLocallyFiniteMeasure μ
⊢ μ.OuterRegular
have refine : ∀ (U : Set X)
  (hU :
    Membership.mem (γ := Set (Set X))
      ({K : Set X | IsOpen[inst_2] K} ∩ {s : Set X | LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)})
      U),
  Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst_2] U ∧ (μ.restrict U).OuterRegular} U
Tactic: refine (μ.finiteSpanningSetsInOpen'.mono' fun U hU => ?_).outerRegular
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
X : Type u_3
inst_2 : TopologicalSpace X
inst_3 : PseudoMetrizableSpace X
inst_4 : SecondCountableTopology X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
μ : Measure X
inst_7 : IsLocallyFiniteMeasure μ
U : Set X
hU :
  Membership.mem (γ := Set (Set X))
    ({K : Set X | IsOpen[inst_2] K} ∩ {s : Set X | LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}) U
⊢ Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst_2] U ∧ (μ.restrict U).OuterRegular} U
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (μ U < ∞) := ⟨hU.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
x : ℝ≥0∞
hx : x ≠ ∞
⊢ (x • μ).WeaklyRegular
have this : (x • μ).OuterRegular
Tactic: haveI := OuterRegular.smul μ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have simp_rw₁ : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
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∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have 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
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
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
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have 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∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
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∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have 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∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
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∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have 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∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
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∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have 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∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
inst_6 : μ.Regular
f : α ≃ₜ β
⊢ Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
have this : OuterRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
Tactic: haveI := OuterRegular.map f μ