awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
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) < ε
rwa rwa₁ rwa₂ rwa₃ : (μ : (a : Set α) → ℝ≥0∞) (U ∆ t) < ε
⊢ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
rwa [measure_congr <| (ae_eq_refl _).symmDiff hst]

Premises used: MeasureTheory.measure_congr, MeasureTheory.ae_eq_refl, Filter.EventuallyEq.symmDiff
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
pos : ∀ (hc : c = 0), (c • μ).InnerRegularCompactLTTop
neg : ∀ (hc : ¬c = 0), (c • μ).InnerRegularCompactLTTop
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : c = 0
pos : InnerRegularCompactLTTop.{u_1} (α := α) 0
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
simp only [hc, zero_smul]

Premises used: zero_smul
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : c = 0
⊢ InnerRegularCompactLTTop.{u_1} (α := α) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
neg : ∀ (h'c : ¬c = ∞), (c • μ).InnerRegularCompactLTTop
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
by_cases h'c : c = ∞
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
pos :
  (c • μ).InnerRegularWRT IsCompact fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
neg :
  ∀ (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

Tactic:
by_cases h's : μ s = 0

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
h's : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (c • μ : (a : Set α) → ℝ≥0∞) K

Tactic:
simp [h's] at hr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
h's : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (c • μ : (a : Set α) → ℝ≥0∞) K

Tactic:
simp [h'c, h's] at hs
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
neg :
  (c • μ).InnerRegularWRT IsCompact fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
InnerRegularWRT.smul h.innerRegular c

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, MeasureTheory.Measure.InnerRegularWRT.smul
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : ¬c = ∞
h₁ :
  ∀ (s : Set α),
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
      MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (c • μ).InnerRegularWRT IsCompact fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
convert! InnerRegularWRT.smul h.innerRegular c using 2 with s

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, MeasureTheory.Measure.InnerRegularWRT.smul
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 α
⊢ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [ENNReal.mul_eq_top, hc, h'c]

Premises used: ENNReal.mul_eq_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 α
⊢ 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]
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 α
this :
  Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [this]
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
c : ℝ≥0
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
inferInstanceAs (InnerRegularCompactLTTop ((c : ℝ≥0∞) • μ))

Premises used: _private.0.MeasureTheory.Measure.InnerRegularCompactLTTop.smul_nnreal._proof_1
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : SigmaFinite μ
⊢ μ.InnerRegular

Tactic:
⟨InnerRegularCompactLTTop.innerRegular.trans InnerRegularWRT.of_sigmaFinite⟩

Premises used: MeasureTheory.Measure.InnerRegularWRT.of_sigmaFinite, MeasureTheory.Measure.InnerRegularWRT.trans, MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, MeasureTheory.Measure.InnerRegular.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
h : μ.InnerRegularCompactLTTop
f : α → β
hf : Continuous[inst_1, inst_4] f
innerRegular :
  @InnerRegularWRT _ inst_3 (map f μ) IsCompact fun (s : Set β) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ InnerRegularCompactLTTop (map f μ)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)

Tactic:
InnerRegularWRT.map h.innerRegular hf.aemeasurable ?_ (fun K hK ↦ hK.image hf) ?_

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, Continuous.aemeasurable, MeasureTheory.Measure.InnerRegularWRT.map, IsCompact.image
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
innerRegular₁ :
  ∀ (U : Set β),
    MeasurableSet U ∧ Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) →
      MeasurableSet U
⊢ @InnerRegularWRT _ inst_3 (map f μ) IsCompact fun (s : Set β) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine InnerRegularWRT.map h.innerRegular hf.aemeasurable ?_ (fun K hK ↦ hK.image hf) ?_

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, Continuous.aemeasurable, MeasureTheory.Measure.InnerRegularWRT.map, IsCompact.image
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    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

Premises used: MeasureTheory.Measure.map_apply, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
⊢ MeasurableSet (f ⁻¹' s) ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨hf.measurable hs, by rwa [map_apply hf.measurable hs] at h's⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ MeasurableSet s

Tactic:
hs
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ MeasurableSet s

Tactic:
exact hs
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
⊢ WeaklyRegular.{u_1} (α := α) 0

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

Premises used: MeasureTheory.Measure.WeaklyRegular.mk, isClosed_empty, And.intro, Set.empty_subset, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
U : Set α
hU : IsOpen[inst_1] U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) U
⊢ ∃ F ⊆ U, IsClosed[inst_1] F ∧ r < (μ : (a : Set α) → ℝ≥0∞) F

Tactic:
WeaklyRegular.innerRegular hU r hr

Premises used: MeasureTheory.Measure.WeaklyRegular.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
U : Set α
hU : IsOpen[inst_1] U
μ : Measure α
inst_2 : μ.WeaklyRegular
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    (⨆ (F : Set α), ⨆ (_ : F ⊆ U), ⨆ (_ : IsClosed[inst_1] F), (μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞)

Tactic:
WeaklyRegular.innerRegular.measure_eq_iSup hU

Premises used: MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup, MeasureTheory.Measure.WeaklyRegular.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
⊢ μ.InnerRegularWRT IsClosed[inst_1] fun (s : Set α) ↦
    MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
WeaklyRegular.innerRegular.measurableSet_of_isOpen (fun _ _ h₁ h₂ ↦ h₁.inter h₂.isClosed_compl)

Premises used: IsOpen.isClosed_compl, IsClosed.inter, MeasureTheory.Measure.WeaklyRegular.innerRegular, MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ K ⊆ s, IsClosed[inst_1] K ∧ (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
innerRegular_measurable.exists_subset_lt_add isClosed_empty ⟨hs, hμs⟩ hμs hε

Premises used: MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable, isClosed_empty, And.intro, MeasureTheory.Measure.InnerRegularWRT.exists_subset_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
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) < ε
⊢ ∃ 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⟩

Premises used: MeasurableSet.exists_isClosed_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : 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:
⟨F, hFA, hFc, measure_diff_lt_of_lt_add hFc.nullMeasurableSet hFA
    (ne_top_of_le_ne_top h'A <| measure_mono hFA) hF⟩

Premises used: MeasureTheory.measure_diff_lt_of_lt_add, ne_top_of_le_ne_top, And.intro, IsClosed.nullMeasurableSet, MeasureTheory.measure_mono, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : 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:
exact ⟨F, hFA, hFc, measure_diff_lt_of_lt_add hFc.nullMeasurableSet hFA
    (ne_top_of_le_ne_top h'A <| measure_mono hFA) hF⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∃ K ⊆ A, IsClosed[inst_1] K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
innerRegular_measurable ⟨hA, h'A⟩ _ hr

Premises used: MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
A : Set α
hA : MeasurableSet A
h'A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ A), ⨆ (_ : IsClosed[inst_1] K), (μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
innerRegular_measurable.measure_eq_iSup ⟨hA, h'A⟩

Premises used: MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable, And.intro, MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
haveI : Fact (μ A < ∞) := ⟨h'A.lt_top⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
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

Tactic:
InnerRegularWRT.weaklyRegular_of_finite (μ.restrict A) (fun V V_open r hr ↦ ?_)

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞))
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
⊢ (μ.restrict A).WeaklyRegular

Tactic:
refine InnerRegularWRT.weaklyRegular_of_finite (μ.restrict A) (fun V V_open r hr ↦ ?_)

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
⊢ (μ.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
-- Module: Mathlib.MeasureTheory.Measure.Regular
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_1 : 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
this : (μ.restrict A).InnerRegularWRT IsClosed[inst_1] fun (s : Set α) ↦ MeasurableSet s
⊢ ∃ K ⊆ V, IsClosed[inst_1] K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K

Tactic:
this V_open.measurableSet r hr

Premises used: IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Regular
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_1 : 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
this : (μ.restrict A).InnerRegularWRT IsClosed[inst_1] fun (s : Set α) ↦ MeasurableSet s
⊢ ∃ K ⊆ V, IsClosed[inst_1] K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K

Tactic:
exact this V_open.measurableSet r hr

Premises used: IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : IsFiniteMeasure μ
⊢ μ.WeaklyRegular

Tactic:
(InnerRegularWRT.of_pseudoMetrizableSpace μ).weaklyRegular_of_finite μ

Premises used: MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite, MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace
-- Module: Mathlib.MeasureTheory.Measure.Regular
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

Tactic:
(μ.finiteSpanningSetsInOpen'.mono' fun U hU => ?_).outerRegular

Premises used: MeasureTheory.Measure.finiteSpanningSetsInOpen', MeasureTheory.Measure.FiniteSpanningSetsIn.outerRegular, MeasureTheory.Measure.FiniteSpanningSetsIn.mono'