awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
refine :
  ∀ (r : ℝ≥0∞) (hr : (μ : (a : Set α) → ℝ≥0∞) A < r),
    ⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ LE.le (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
refine le_of_forall_gt fun r hr => ?_

Premises used: le_of_forall_gt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) A < r
⊢ ⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
simpa only [iInf_lt_iff, exists_prop] using A.exists_isOpen_lt_of_lt r hr

Premises used: exists_prop, Set.exists_isOpen_lt_of_lt, iInf_lt_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
hA : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε

Tactic:
A.exists_isOpen_lt_of_lt _ (ENNReal.lt_add_right hA hε)

Premises used: ENNReal.lt_add_right, Set.exists_isOpen_lt_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
inl :
  ∀ (H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
inr :
  ∀ (H : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε

Tactic:
rcases eq_or_ne (μ A) ∞ with (H | H)

Premises used: eq_or_ne, Top.top, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) univ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε

Tactic:
simp only [H, _root_.top_add, le_top]

Premises used: le_top, top_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε

Tactic:
exact ⟨univ, subset_univ _, isOpen_univ, by simp only [H, _root_.top_add, le_top]⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
inr :
  ∀ (U : Set α) (AU : U ⊇ A) (U_open : IsOpen[inst_1] U)
    (hU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε),
    ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε

Tactic:
rcases A.exists_isOpen_lt_add H hε with ⟨U, AU, U_open, hU⟩

Premises used: Set.exists_isOpen_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
AU : U ⊇ A
U_open : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε

Tactic:
⟨U, AU, U_open, hU.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
H : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
AU : U ⊇ A
U_open : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε

Tactic:
exact ⟨U, AU, U_open, hU.le⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
rcases :
  ∀ (U : Set α) (hAU : U ⊇ A) (hUo : IsOpen[inst_1] U)
    (hU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε),
    ∃ U ⊇ A,
      IsOpen[inst_1] U ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U \ A) < ε
⊢ ∃ U ⊇ A,
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U \ A) < ε

Tactic:
rcases A.exists_isOpen_lt_add hA' hε with ⟨U, hAU, hUo, hU⟩

Premises used: Set.exists_isOpen_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
right : (μ : (a : Set α) → ℝ≥0∞) (U \ A) < ε
⊢ ∃ U ⊇ A,
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U \ A) < ε

Tactic:
use U, hAU, hUo, hU.trans_le le_top

Premises used: LT.lt.trans_le, le_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) (U \ A) < ε

Tactic:
measure_diff_lt_of_lt_add hA.nullMeasurableSet hAU hA' hU

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_diff_lt_of_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) (U \ A) < ε

Tactic:
exact measure_diff_lt_of_lt_add hA.nullMeasurableSet hAU hA' hU

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_diff_lt_of_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst_6 : μ.OuterRegular
⊢ OuterRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)

Tactic:
⟨fun A hA r hr => ?_⟩

Premises used: MeasureTheory.Measure.OuterRegular.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst_6 : μ.OuterRegular
refine :
  ∀ (A : Set β) (hA : MeasurableSet A) (r : ℝ≥0∞)
    (hr : r > ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) A),
    ∃ U ⊇ A, IsOpen[inst_4] U ∧ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) U < r
⊢ OuterRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)

Tactic:
refine ⟨fun A hA r hr => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst_6 : μ.OuterRegular
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) A
⊢ r > (μ : (a : Set α) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) '' A)

Tactic:
rw [map_apply f.measurable hA, ← f.image_symm] at hr

Premises used: MeasureTheory.Measure.map_apply, Homeomorph.image_symm, Homeomorph.measurable
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst_6 : μ.OuterRegular
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) '' A)
rcases :
  ∀ (U : Set α) (hAU : U ⊇ (⇑f.symm : (a : β) → α) '' A) (hUo : IsOpen[inst_1] U) (hU : (μ : (a : Set α) → ℝ≥0∞) U < r),
    ∃ U ⊇ A, IsOpen[inst_4] U ∧ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ A, IsOpen[inst_4] U ∧ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) U < r

Tactic:
rcases Set.exists_isOpen_lt_of_lt _ r hr with ⟨U, hAU, hUo, hU⟩

Premises used: Set.exists_isOpen_lt_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst_6 : μ.OuterRegular
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) '' A)
U : Set α
hAU : U ⊇ (⇑f.symm : (a : β) → α) '' A
hUo : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ IsOpen[inst_4] ((⇑f.symm : (a : β) → α) ⁻¹' U)

Tactic:
have : IsOpen (f.symm ⁻¹' U) := hUo.preimage f.symm.continuous
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst_6 : μ.OuterRegular
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) '' A)
U : Set α
hAU : U ⊇ (⇑f.symm : (a : β) → α) '' A
hUo : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < r
this : IsOpen[inst_4] ((⇑f.symm : (a : β) → α) ⁻¹' U)
⊢ ∃ U ⊇ A, IsOpen[inst_4] U ∧ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) U < r

Tactic:
⟨f.symm ⁻¹' U, image_subset_iff.1 hAU, this, ?_⟩

Premises used: Set.preimage, Homeomorph.symm, And.intro, Exists.intro, Iff.mp, Set.image_subset_iff, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst_6 : μ.OuterRegular
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) '' A)
U : Set α
hAU : U ⊇ (⇑f.symm : (a : β) → α) '' A
hUo : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < r
this : IsOpen[inst_4] ((⇑f.symm : (a : β) → α) ⁻¹' U)
refine : ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) ⁻¹' U) < r
⊢ ∃ U ⊇ A, IsOpen[inst_4] U ∧ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) U < r

Tactic:
refine ⟨f.symm ⁻¹' U, image_subset_iff.1 hAU, this, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst_6 : μ.OuterRegular
A : Set β
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) '' A)
U : Set α
hAU : U ⊇ (⇑f.symm : (a : β) → α) '' A
hUo : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < r
this : IsOpen[inst_4] ((⇑f.symm : (a : β) → α) ⁻¹' U)
rwa : (μ : (a : Set α) → ℝ≥0∞) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f.symm : (a : β) → α) ⁻¹' U)) < r
rwa₁ : (μ : (a : Set α) → ℝ≥0∞) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' U)) < r
rwa₂ rwa₃ rwa₄ rwa₅ : (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) ⁻¹' U) < r

Tactic:
rwa [map_apply f.measurable this.measurableSet, f.preimage_symm, f.preimage_image]

Premises used: MeasureTheory.Measure.map_apply, IsOpen.measurableSet, Homeomorph.preimage_symm, Homeomorph.preimage_image, Homeomorph.measurable
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
mβ : MeasurableSpace β
inst_2 : TopologicalSpace β
μ : Measure β
inst_3 : μ.OuterRegular
f : α → β
f_cont : Continuous[inst_1, inst_2] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) A
⊢ r > (μ : (a : Set β) → ℝ≥0∞) (f '' A)

Tactic:
rw [f_me.comap_apply] at hr

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
mβ : MeasurableSpace β
inst_2 : TopologicalSpace β
μ : Measure β
inst_3 : μ.OuterRegular
f : α → β
f_cont : Continuous[inst_1, inst_2] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set β) → ℝ≥0∞) (f '' A)
obtain :
  ∀ (U : Set β) (hUA : U ⊇ f '' A) (Uopen : IsOpen[inst_2] U) (hμU : (μ : (a : Set β) → ℝ≥0∞) U < r),
    ∃ U ⊇ A, IsOpen[inst_1] U ∧ ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) U < r

Tactic:
obtain ⟨U, hUA, Uopen, hμU⟩ := OuterRegular.outerRegular (f_me.measurableSet_image' hA) r hr

Premises used: MeasurableEmbedding.measurableSet_image', MeasureTheory.Measure.OuterRegular.outerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
mβ : MeasurableSpace β
inst_2 : TopologicalSpace β
μ : Measure β
inst_3 : μ.OuterRegular
f : α → β
f_cont : Continuous[inst_1, inst_2] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set β) → ℝ≥0∞) (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst_2] U
hμU : (μ : (a : Set β) → ℝ≥0∞) U < r
rwa : A ⊆ f ⁻¹' U
rwa₁ rwa₂ rwa₃ rwa₄ : f '' A ⊆ U
⊢ f ⁻¹' U ⊇ A

Tactic:
rwa [Superset, ← image_subset_iff]

Premises used: Superset, Set.image_subset_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
mβ : MeasurableSpace β
inst_2 : TopologicalSpace β
μ : Measure β
inst_3 : μ.OuterRegular
f : α → β
f_cont : Continuous[inst_1, inst_2] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set β) → ℝ≥0∞) (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst_2] U
hμU : (μ : (a : Set β) → ℝ≥0∞) U < r
refine : ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' U) < r
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) U < r

Tactic:
refine ⟨f ⁻¹' U, by rwa [Superset, ← image_subset_iff], Uopen.preimage f_cont, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
mβ : MeasurableSpace β
inst_2 : TopologicalSpace β
μ : Measure β
inst_3 : μ.OuterRegular
f : α → β
f_cont : Continuous[inst_1, inst_2] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set β) → ℝ≥0∞) (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst_2] U
hμU : (μ : (a : Set β) → ℝ≥0∞) U < r
rw : (μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' U) < r
⊢ ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' U) < r

Tactic:
rw [f_me.comap_apply]

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
mβ : MeasurableSpace β
inst_2 : TopologicalSpace β
μ : Measure β
inst_3 : μ.OuterRegular
f : α → β
f_cont : Continuous[inst_1, inst_2] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set β) → ℝ≥0∞) (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst_2] U
hμU : (μ : (a : Set β) → ℝ≥0∞) U < r
⊢ (μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' U) < r

Tactic:
(measure_mono (image_preimage_subset _ _)).trans_lt hμU

Premises used: Set.image_preimage_subset, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
mβ : MeasurableSpace β
inst_2 : TopologicalSpace β
μ : Measure β
inst_3 : μ.OuterRegular
f : α → β
f_cont : Continuous[inst_1, inst_2] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set β) → ℝ≥0∞) (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst_2] U
hμU : (μ : (a : Set β) → ℝ≥0∞) U < r
⊢ (μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' U) < r

Tactic:
exact (measure_mono (image_preimage_subset _ _)).trans_lt hμU

Premises used: Set.image_preimage_subset, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 : μ.OuterRegular
f : α ≃ₜ β
⊢ OuterRegular.{u_1} (α := α) (comap (⇑f : (a : α) → β) μ)

Tactic:
OuterRegular.comap' μ f.continuous f.measurableEmbedding

Premises used: Homeomorph.continuous, Homeomorph.measurableEmbedding, MeasureTheory.Measure.OuterRegular.comap'
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
μ : Measure α
inst_2 : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
inl : ∀ (hx : Ne (α := ℝ≥0∞) 0 ∞), (HSMul.hSMul (α := ℝ≥0∞) 0 μ).OuterRegular
inr : ∀ (h0 : x ≠ 0), (x • μ).OuterRegular
⊢ (x • μ).OuterRegular

Tactic:
rcases eq_or_ne x 0 with (rfl | h0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
μ : Measure α
inst_2 : μ.OuterRegular
hx : Ne (α := ℝ≥0∞) 0 ∞
inl : OuterRegular.{u_1} (α := α) 0
⊢ (HSMul.hSMul (α := ℝ≥0∞) 0 μ).OuterRegular

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
μ : Measure α
inst_2 : μ.OuterRegular
hx : Ne (α := ℝ≥0∞) 0 ∞
⊢ OuterRegular.{u_1} (α := α) 0

Tactic:
OuterRegular.zero

Premises used: MeasureTheory.Measure.OuterRegular.zero
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
μ : Measure α
inst_2 : μ.OuterRegular
hx : Ne (α := ℝ≥0∞) 0 ∞
⊢ OuterRegular.{u_1} (α := α) 0

Tactic:
exact OuterRegular.zero

Premises used: MeasureTheory.Measure.OuterRegular.zero
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
μ : Measure α
inst_2 : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
⊢ (x • μ).OuterRegular

Tactic:
⟨fun A _ r hr => ?_⟩

Premises used: MeasureTheory.Measure.OuterRegular.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
μ : Measure α
inst_2 : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
inr :
  ∀ (A : Set α),
    MeasurableSet A →
      ∀ (r : ℝ≥0∞) (hr : r > (x • μ : (a : Set α) → ℝ≥0∞) A),
        ∃ U ⊇ A, IsOpen[inst_1] U ∧ (x • μ : (a : Set α) → ℝ≥0∞) U < r
⊢ (x • μ).OuterRegular

Tactic:
refine ⟨fun A _ r hr => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
μ : Measure α
inst_2 : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
A : Set α
h : MeasurableSet A
r : ℝ≥0∞
hr : r > (x • μ : (a : Set α) → ℝ≥0∞) A
⊢ r > x * ⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U

Tactic:
rw [smul_apply, A.measure_eq_iInf_isOpen, smul_eq_mul] at hr

Premises used: MeasureTheory.Measure.smul_apply, Set.measure_eq_iInf_isOpen, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
μ : Measure α
inst_2 : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
A : Set α
h : MeasurableSet A
r : ℝ≥0∞
hr : r > x * ⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (x • μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
simpa only [ENNReal.mul_iInf_of_ne h0 hx, gt_iff_lt, iInf_lt_iff, exists_prop] using hr

Premises used: exists_prop, ENNReal.mul_iInf_of_ne, iInf_lt_iff, gt_iff_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ : Measure α
inst_2 : μ.OuterRegular
c : ℝ≥0
⊢ (c • μ).OuterRegular

Tactic:
OuterRegular.smul μ coe_ne_top

Premises used: MeasureTheory.Measure.OuterRegular.smul, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst_1] (s n)
h'' : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
⊢ μ.OuterRegular

Tactic:
⟨fun A hA r hr => ?_⟩

Premises used: MeasureTheory.Measure.OuterRegular.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst_1] (s n)
h'' : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
refine :
  ∀ (A : Set α) (hA : MeasurableSet A) (r : ℝ≥0∞) (hr : r > (μ : (a : Set α) → ℝ≥0∞) A),
    ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ μ.OuterRegular

Tactic:
refine ⟨fun A hA r hr => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst_1] (s n)
h'' : Subset.{u_1} (α := Set α) univ (⋃ (n : ℕ), s n)
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) A
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have HA : μ A < ∞ := lt_of_lt_of_le hr le_top