awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : IsLocallyFiniteMeasure μ
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ μ.Regular

Tactic:
exact ⟨(InnerRegularWRT.isCompact_isClosed μ).trans (InnerRegularWRT.of_pseudoMetrizableSpace μ)⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
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

Tactic:
⟨(InnerRegularWRT.isCompact_isClosed μ).trans ?_⟩

Premises used: MeasureTheory.Measure.InnerRegularWRT.trans, MeasureTheory.Measure.InnerRegular.mk, MeasureTheory.Measure.InnerRegularWRT.isCompact_isClosed
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 μ
refine : μ.InnerRegularWRT IsClosed[inst_1] MeasurableSet
⊢ μ.InnerRegular

Tactic:
refine ⟨(InnerRegularWRT.isCompact_isClosed μ).trans ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
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

Tactic:
InnerRegularWRT.of_restrict (fun n ↦ ?_) (iUnion_spanningSets μ).superset
    (monotone_spanningSets μ)

Premises used: MeasureTheory.monotone_spanningSets, MeasureTheory.iUnion_spanningSets, MeasureTheory.Measure.InnerRegularWRT.of_restrict, Eq.superset
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 μ
refine : ∀ (n : ℕ), (μ.restrict (spanningSets μ n)).InnerRegularWRT IsClosed[inst_1] MeasurableSet
⊢ μ.InnerRegularWRT IsClosed[inst_1] MeasurableSet

Tactic:
refine InnerRegularWRT.of_restrict (fun n ↦ ?_) (iUnion_spanningSets μ).superset
    (monotone_spanningSets μ)

Premises used: MeasureTheory.monotone_spanningSets, MeasureTheory.iUnion_spanningSets, MeasureTheory.Measure.InnerRegularWRT.of_restrict, Eq.superset
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : ℕ
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : Fact (μ (spanningSets μ n) < ∞) := ⟨measure_spanningSets_lt_top μ n⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : ℕ
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ (μ.restrict (spanningSets μ n)).InnerRegularWRT IsClosed[inst_1] MeasurableSet

Tactic:
WeaklyRegular.innerRegular_measurable.trans InnerRegularWRT.of_sigmaFinite

Premises used: MeasureTheory.Measure.InnerRegularWRT.of_sigmaFinite, MeasureTheory.Measure.InnerRegularWRT.trans, MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : ℕ
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ (μ.restrict (spanningSets μ n)).InnerRegularWRT IsClosed[inst_1] MeasurableSet

Tactic:
exact WeaklyRegular.innerRegular_measurable.trans InnerRegularWRT.of_sigmaFinite

Premises used: MeasureTheory.Measure.InnerRegularWRT.of_sigmaFinite, MeasureTheory.Measure.InnerRegularWRT.trans, MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
mp : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed → μ.InnerRegularWRT IsCompact IsClosed
mpr : μ.InnerRegularWRT IsCompact IsClosed → μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
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
⊢ ∃ K ⊆ A, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
⟨closure K, closure_minimal hK1 hA, hK2, hK3.trans_le (measure_mono subset_closure)⟩

Premises used: subset_closure, closure_minimal, closure, LT.lt.trans_le, And.intro, MeasureTheory.measure_mono, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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, IsCompact K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
exact ⟨closure K, closure_minimal hK1 hA, hK2, hK3.trans_le (measure_mono subset_closure)⟩
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
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
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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

Tactic:
⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩

Premises used: closure_minimal, closure, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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)
mpr₁ : r < (μ : (a : Set α) → ℝ≥0∞) (closure K)
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ (IsCompact ∘ closure) (closure K)

Tactic:
simpa only [closure_closure, Function.comp_apply] using hK2.closure

Premises used: IsCompact.closure, closure_closure, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ r < (μ : (a : Set α) → ℝ≥0∞) (closure K)

Tactic:
hK3.trans_le (measure_mono subset_closure)

Premises used: subset_closure, LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ r < (μ : (a : Set α) → ℝ≥0∞) (closure K)

Tactic:
exact hK3.trans_le (measure_mono subset_closure)

Premises used: subset_closure, LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
mpr :
  μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed →
    μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed
⊢ μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed ↔
    μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
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
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
obtain ⟨K, hK1, ⟨hK2, _⟩, hK4⟩ := h hA r hr
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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

Tactic:
⟨K, hK1, ?_, hK4⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
mp : (IsCompact ∘ closure) K
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
refine ⟨K, hK1, ?_, hK4⟩
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ IsCompact (closure K)

Tactic:
hK2.closure

Premises used: IsCompact.closure
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ IsCompact (closure K)

Tactic:
exact hK2.closure

Premises used: IsCompact.closure
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
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
⊢ ∃ 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
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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

Tactic:
⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩

Premises used: closure_minimal, closure, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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)
mpr₁ : r < (μ : (a : Set α) → ℝ≥0∞) (closure K)
⊢ ∃ K ⊆ A, (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) (closure K)

Tactic:
simpa only [isClosed_closure, and_true]

Premises used: and_true, isClosed_closure
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ r < (μ : (a : Set α) → ℝ≥0∞) (closure K)

Tactic:
hK3.trans_le (measure_mono subset_closure)

Premises used: subset_closure, LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
⊢ r < (μ : (a : Set α) → ℝ≥0∞) (closure K)

Tactic:
exact hK3.trans_le (measure_mono subset_closure)

Premises used: subset_closure, LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : R1Space α
⊢ μ.InnerRegularWRT (fun (s : Set α) ↦ IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed

Tactic:
innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure.trans
    innerRegularWRT_isCompact_closure_iff

Premises used: MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure, MeasureTheory.innerRegularWRT_isCompact_closure_iff, Iff.trans
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
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
⊢ ∃ (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)

Premises used: HSub.hSub, DFunLike.coe, tsub_pos_of_lt
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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

Tactic:
⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩

Premises used: Inter.inter, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
refine : (μ : (a : Set α) → ℝ≥0∞) (A \ (K' ∩ A)) < 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:
refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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

Tactic:
(measure_mono fun x ↦ ?_).trans_lt hK'_lt

Premises used: MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
refine : ∀ x ∈ A \ (K' ∩ A), x ∈ K'ᶜ
⊢ (μ : (a : Set α) → ℝ≥0∞) (A \ (K' ∩ A)) < HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) r

Tactic:
refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt

Premises used: MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
x : α
⊢ x ∈ A \ (K' ∩ A) → x ∈ K'ᶜ

Tactic:
simp only [diff_inter_self_eq_diff, mem_diff, mem_compl_iff, and_imp, imp_self, imp_true_iff]

Premises used: and_imp, imp_true_iff, Set.diff_inter_self_eq_diff, imp_self, Set.mem_diff, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
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
⊢ ∃ 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]

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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

Tactic:
⟨K, hK_subset, hK, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
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
refine : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ A, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
refine ⟨K, hK_subset, hK, ?_⟩