awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α ≃ₜ β
this : OuterRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
have this₁ : IsFiniteMeasureOnCompacts.{u_2} (α := β) (m0 := inst_3) (map (⇑f : (a : α) → β) μ)
Tactic: haveI := IsFiniteMeasureOnCompacts.map μ f
-- 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 β
f : α ≃ₜ β
⊢ Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ) ↔ μ.Regular
have refine : ∀ (h : Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)), μ.Regular
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩
-- 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 β
f : α ≃ₜ β
h : Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ μ.Regular
have h₁ : μ = map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ)
Tactic: convert! h.map f.symm
-- 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 β
f : α ≃ₜ β
h : Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ μ = map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ)
have h₁ : μ = map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) μ
Tactic: rw [map_map f.symm.continuous.measurable f.continuous.measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
mβ : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
μ : Measure β
inst_5 : μ.Regular
f : α → β
hf : IsOpenEmbedding f
⊢ Regular (comap f μ)
have this : OuterRegular (comap f μ)
Tactic: haveI := OuterRegular.comap' μ hf.continuous hf.measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
mβ : MeasurableSpace β
inst_3 : TopologicalSpace β
inst_4 : BorelSpace β
μ : Measure β
inst_5 : μ.Regular
f : α → β
hf : IsOpenEmbedding f
this : OuterRegular (comap f μ)
⊢ Regular (comap f μ)
have this₁ : IsFiniteMeasureOnCompacts (m0 := inst) (comap f μ)
Tactic: haveI := IsFiniteMeasureOnCompacts.comap' μ hf.continuous hf.measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
x : ℝ≥0∞
hx : x ≠ ∞
⊢ (x • μ).Regular
have this : (x • μ).OuterRegular
Tactic: haveI := OuterRegular.smul μ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
x : ℝ≥0∞
hx : x ≠ ∞
this : (x • μ).OuterRegular
⊢ (x • μ).Regular
have this₁ : IsFiniteMeasureOnCompacts (x • μ)
Tactic: haveI := IsFiniteMeasureOnCompacts.smul μ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
inst_3 : BorelSpace α
inst_4 : μ.Regular
A : Set α
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ.restrict A).Regular
have this : (μ.restrict A).WeaklyRegular
Tactic: have : WeaklyRegular (μ.restrict A) := WeaklyRegular.restrict_of_measure_ne_top h'A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
inst_3 : BorelSpace α
inst_4 : μ.Regular
A : Set α
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ.restrict A).WeaklyRegular
⊢ (μ.restrict A).Regular
have innerRegular : (μ.restrict A).InnerRegularWRT IsCompact IsOpen[inst_1]
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
inst_3 : BorelSpace α
inst_4 : μ.Regular
A : Set α
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst_1] V
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) V
⊢ Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (V ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [restrict_apply hV.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
inst_3 : BorelSpace α
inst_4 : μ.Regular
A : Set α
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst_1] V
r : ℝ≥0∞
hr : r < (μ.restrict A : (a : Set α) → ℝ≥0∞) V
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K
have R : Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have R : restrict μ A V ≠ ∞ := by
    rw [restrict_apply hV.measurableSet]
    exact ((measure_mono inter_subset_right).trans_lt h'A.lt_top).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : PseudoMetrizableSpace X
inst_3 : SigmaCompactSpace X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : SigmaFinite μ
⊢ μ.InnerRegular
have refine : μ.InnerRegularWRT IsClosed[inst_1] MeasurableSet
Tactic: refine ⟨(InnerRegularWRT.isCompact_isClosed μ).trans ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : PseudoMetrizableSpace X
inst_3 : SigmaCompactSpace X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : SigmaFinite μ
⊢ μ.InnerRegularWRT IsClosed[inst_1] MeasurableSet
have refine : ∀ (n : ℕ), (μ.restrict (spanningSets μ n)).InnerRegularWRT IsClosed[inst_1] MeasurableSet
Tactic: refine InnerRegularWRT.of_restrict (fun n ↦ ?_) (iUnion_spanningSets μ).superset
    (monotone_spanningSets μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : PseudoMetrizableSpace X
inst_3 : SigmaCompactSpace X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : SigmaFinite μ
n : ℕ
⊢ (μ.restrict (spanningSets μ n)).InnerRegularWRT IsClosed[inst_1] MeasurableSet
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (μ (spanningSets μ n) < ∞) := ⟨measure_spanningSets_lt_top μ n⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed
have mp : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed → μ.InnerRegularWRT IsCompact IsClosed
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
mp : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed → μ.InnerRegularWRT IsCompact IsClosed
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed
have mpr : μ.InnerRegularWRT IsCompact IsClosed → μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have mp : ∀ (K : Set α) (hK1 : K ⊆ A) (hK2 : (IsCompact ∘ closure) K) (hK3 : r < (μ : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have mpr : ∀ (K : Set α) (hK1 : K ⊆ A) (hK2 : IsCompact K) (hK3 : r < (μ : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have mpr : (IsCompact ∘ closure) (closure K)
Tactic: refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < (μ : (a : Set α) → ℝ≥0∞) K
mpr : (IsCompact ∘ closure) (closure K)
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have mpr₁ : r < (μ : (a : Set α) → ℝ≥0∞) (closure K)
Tactic: refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
⊢ μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed ↔
    μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
have mp : μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed →
  μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
mp :
  μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed →
    μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
⊢ μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed ↔
    μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
have mpr : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed →
  μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
h : μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have mp : ∀ (K : Set α) (hK1 : K ⊆ A) (hK4 : r < (μ : (a : Set α) → ℝ≥0∞) K) (hK2 : IsCompact K),
  IsClosed K → ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: obtain ⟨K, hK1, ⟨hK2, _⟩, hK4⟩ := h hA r hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
h : μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK1 : K ⊆ A
hK4 : r < (μ : (a : Set α) → ℝ≥0∞) K
hK2 : IsCompact K
right : IsClosed K
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have mp : (IsCompact ∘ closure) K
Tactic: refine ⟨K, hK1, ?_, hK4⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have mpr : ∀ (K : Set α) (hK1 : K ⊆ A) (hK2 : (IsCompact ∘ closure) K) (hK3 : r < (μ : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ A, (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: obtain ⟨K, hK1, hK2, hK3⟩ := h hA r hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ A, (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have mpr : (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) (closure K)
Tactic: refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < (μ : (a : Set α) → ℝ≥0∞) K
mpr : (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) (closure K)
⊢ ∃ K ⊆ A, (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have mpr₁ : r < (μ : (a : Set α) → ℝ≥0∞) (closure K)
Tactic: refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), p K ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ (K : Set α),
    p K ∧ K ⊆ A ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
have obtain : ∀ (K' : Set α) (hpK' : p K')
  (hK'_lt : (μ : (a : Set α) → ℝ≥0∞) K'ᶜ < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r),
  ∃ (K : Set α),
    p K ∧ K ⊆ A ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
Tactic: obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), p K ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K' : Set α
hpK' : p K'
hK'_lt : (μ : (a : Set α) → ℝ≥0∞) K'ᶜ < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
⊢ ∃ (K : Set α),
    p K ∧ K ⊆ A ∧ (μ : (a : Set α) → ℝ≥0∞) (A \ K) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
have refine : (μ : (a : Set α) → ℝ≥0∞) (A \ (K' ∩ A)) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
Tactic: refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), p K ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K' : Set α
hpK' : p K'
hK'_lt : (μ : (a : Set α) → ℝ≥0∞) K'ᶜ < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
⊢ (μ : (a : Set α) → ℝ≥0∞) (A \ (K' ∩ A)) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
have refine : ∀ x ∈ A \ (K' ∩ A), x ∈ K'ᶜ
Tactic: refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), p K ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have obtain : ∀ (K : Set α) (hK : p K) (hK_subset : K ⊆ A)
  (h_lt : (μ : (a : Set α) → ℝ≥0∞) (A \ K) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r),
  ∃ K ⊆ A, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: obtain ⟨K, hK, hK_subset, h_lt⟩ : ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r := by
    obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)
    refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
    · refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
      simp only [diff_inter_self_eq_diff, mem_diff, mem_compl_iff, and_imp, imp_self, imp_true_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), p K ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK : p K
hK_subset : K ⊆ A
h_lt : (μ : (a : Set α) → ℝ≥0∞) (A \ K) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
⊢ ∃ K ⊆ A, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have refine : r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: refine ⟨K, hK_subset, hK, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), p K ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
K : Set α
hK : p K
hK_subset : K ⊆ A
h_lt : (μ : (a : Set α) → ℝ≥0∞) (A \ K) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
⊢ r < (μ : (a : Set α) → ℝ≥0∞) K
have h_lt' : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) <
  HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r
Tactic: have h_lt' : μ A - μ K < μ A - r := le_measure_diff.trans_lt h_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
have refine : ∀ (s t : Set α) (hs : (IsCompact ∘ closure) s) (ht : IsClosed t), (IsCompact ∘ closure) (s ∩ t)
Tactic: refine innerRegularWRT_of_exists_compl_lt (fun s t hs ht ↦ ?_) hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
⊢ (IsCompact ∘ closure) (s ∩ t)
have this : IsCompact (closure s ∩ t)
Tactic: have : IsCompact (closure s ∩ t) := hs.inter_right ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ (IsCompact ∘ closure) (s ∩ t)
have refine : closure (s ∩ t) ⊆ closure s ∩ t
Tactic: refine this.of_isClosed_subset isClosed_closure ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ closure (s ∩ t) ⊆ closure s ∩ t
have refine : closure s ∩ closure t = closure s ∩ t
Tactic: refine (closure_inter_subset_inter_closure _ _).trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set α), IsCompact (closure K) ∧ (μ : (a : Set α) → ℝ≥0∞) Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ closure s ∩ closure t = closure s ∩ t
have rw : closure s ∩ t = closure s ∩ t
Tactic: rw [IsClosed.closure_eq ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have cases : IsEmpty α → ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
cases : IsEmpty α → ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have cases₁ : Nonempty α → ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.RegularityCompacts (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : IsEmpty α
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
have refine : (P : (a : Set α) → ℝ≥0∞) ∅ᶜ < ε
Tactic: refine ⟨∅, by simp, ?_⟩