awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ
refine :
  ∀ (U : Set X)
    (hU :
      Membership.mem (γ := Set (Set X))
        ({K : Set X | IsOpen[inst_2] K} ∩
          {s : Set X | LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)})
        U),
    Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst_2] U ∧ (μ.restrict U).OuterRegular} U
⊢ μ.OuterRegular

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

Premises used: MeasureTheory.Measure.finiteSpanningSetsInOpen', MeasureTheory.Measure.FiniteSpanningSetsIn.outerRegular, MeasureTheory.Measure.FiniteSpanningSetsIn.mono'
-- 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 μ
U : Set X
hU :
  Membership.mem (γ := Set (Set X))
    ({K : Set X | IsOpen[inst_2] K} ∩ {s : Set X | LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}) U
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : Fact (μ U < ∞) := ⟨hU.2⟩
-- 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 μ
U : Set X
hU :
  Membership.mem (γ := Set (Set X))
    ({K : Set X | IsOpen[inst_2] K} ∩ {s : Set X | LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}) U
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst_2] U ∧ (μ.restrict U).OuterRegular} U

Tactic:
⟨hU.1, inferInstance⟩

Premises used: Set.Mem, setOf, inferInstance, And.left, And.intro
-- 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 μ
U : Set X
hU :
  Membership.mem (γ := Set (Set X))
    ({K : Set X | IsOpen[inst_2] K} ∩ {s : Set X | LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}) U
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst_2] U ∧ (μ.restrict U).OuterRegular} U

Tactic:
exact ⟨hU.1, inferInstance⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
x : ℝ≥0∞
hx : x ≠ ∞
⊢ (x • μ).OuterRegular

Tactic:
haveI := OuterRegular.smul μ hx
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
x : ℝ≥0∞
hx : x ≠ ∞
this : (x • μ).OuterRegular
⊢ (x • μ).WeaklyRegular

Tactic:
⟨WeaklyRegular.innerRegular.smul x⟩

Premises used: MeasureTheory.Measure.WeaklyRegular.mk, MeasureTheory.Measure.InnerRegularWRT.smul, MeasureTheory.Measure.WeaklyRegular.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
x : ℝ≥0∞
hx : x ≠ ∞
this : (x • μ).OuterRegular
⊢ (x • μ).WeaklyRegular

Tactic:
exact ⟨WeaklyRegular.innerRegular.smul x⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.WeaklyRegular
c : ℝ≥0
⊢ (c • μ).WeaklyRegular

Tactic:
WeaklyRegular.smul coe_ne_top

Premises used: MeasureTheory.Measure.WeaklyRegular.smul, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
⊢ Regular.{u_1} (α := α) 0

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

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

Tactic:
Regular.innerRegular hU r hr

Premises used: MeasureTheory.Measure.Regular.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 : μ.Regular
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
Regular.innerRegular.measure_eq_iSup hU

Premises used: MeasureTheory.Measure.Regular.innerRegular, MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
simp_rw₁ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), (μ : (a : Set α) → ℝ≥0∞) K) 0
simp_rw₃ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬∀ (i : Set α) (i_1 : i ⊆ univ) (i_2 : IsCompact i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₄ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∃ (x : Set α) (_ : x ⊆ univ) (_ : IsCompact x), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₅ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∃ x ⊆ univ, IsCompact x ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₆ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∃ (x : Set α), True ∧ IsCompact x ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0

Tactic:
simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]

Premises used: Set.subset_univ, Ne, exists_prop, IsOpen.measure_eq_iSup_isCompact, isOpen_univ, ENNReal.iSup_eq_zero, MeasureTheory.Measure.measure_univ_eq_zero, Classical.not_forall, true_and
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
⊢ μ.InnerRegularCompactLTTop

Tactic:
⟨Regular.innerRegular.measurableSet_of_isOpen (fun _ _ hs hU ↦ hs.diff hU)⟩

Premises used: MeasureTheory.Measure.Regular.innerRegular, IsCompact.diff, MeasureTheory.Measure.InnerRegularCompactLTTop.mk, MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen
-- 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 β
inst_6 : μ.Regular
f : α ≃ₜ β
⊢ OuterRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)

Tactic:
haveI := OuterRegular.map f μ
-- 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 β
inst_6 : μ.Regular
f : α ≃ₜ β
this : OuterRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ IsFiniteMeasureOnCompacts.{u_2} (α := β) (m0 := inst_3) (map (⇑f : (a : α) → β) μ)

Tactic:
haveI := IsFiniteMeasureOnCompacts.map μ f
-- 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 β
inst_6 : μ.Regular
f : α ≃ₜ β
this_1 : OuterRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
this : IsFiniteMeasureOnCompacts.{u_2} (α := β) (m0 := inst_3) (map (⇑f : (a : α) → β) μ)
⊢ Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)

Tactic:
⟨Regular.innerRegular.map' f.toMeasurableEquiv
        (fun U hU => hU.preimage f.continuous)
        (fun K hK => hK.image f.continuous)⟩

Premises used: MeasureTheory.Measure.Regular.innerRegular, Homeomorph.continuous, MeasureTheory.Measure.InnerRegularWRT.map', Homeomorph.toMeasurableEquiv, IsOpen.preimage, IsCompact.image, MeasureTheory.Measure.Regular.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 β
inst_6 : μ.Regular
f : α ≃ₜ β
this_1 : OuterRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
this : IsFiniteMeasureOnCompacts.{u_2} (α := β) (m0 := inst_3) (map (⇑f : (a : α) → β) μ)
⊢ Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)

Tactic:
exact
    ⟨Regular.innerRegular.map' f.toMeasurableEquiv
        (fun U hU => hU.preimage f.continuous)
        (fun K hK => hK.image f.continuous)⟩
-- 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 β
f : α ≃ₜ β
⊢ Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ) ↔ μ.Regular

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.map f⟩

Premises used: Iff.intro, MeasureTheory.Measure.Regular.map
-- 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 β
f : α ≃ₜ β
refine : ∀ (h : Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)), μ.Regular
⊢ Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ) ↔ μ.Regular

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩
-- 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 β
f : α ≃ₜ β
h : Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ Regular.{u_1} (α := α) (map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ))

Tactic:
h.map f.symm

Premises used: Homeomorph.symm, MeasureTheory.Measure.Regular.map
-- 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 β
f : α ≃ₜ β
h : Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
h₁ : μ = map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ)
⊢ μ.Regular

Tactic:
convert! h.map f.symm

Premises used: Homeomorph.symm, MeasureTheory.Measure.Regular.map
-- 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 β
f : α ≃ₜ β
h : Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
h₁ : μ = map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) μ
⊢ μ = map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ)

Tactic:
rw [map_map f.symm.continuous.measurable f.continuous.measurable]

Premises used: Homeomorph.continuous, Homeomorph.symm, Continuous.measurable, MeasureTheory.Measure.map_map
-- 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 β
f : α ≃ₜ β
h : Regular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ μ = map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) μ

Tactic:
simp
-- 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 : μ.Regular
f : α → β
hf : IsOpenEmbedding f
⊢ OuterRegular (comap f μ)

Tactic:
haveI := OuterRegular.comap' μ hf.continuous hf.measurableEmbedding
-- 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 : μ.Regular
f : α → β
hf : IsOpenEmbedding f
this : OuterRegular (comap f μ)
⊢ IsFiniteMeasureOnCompacts (m0 := inst) (comap f μ)

Tactic:
haveI := IsFiniteMeasureOnCompacts.comap' μ hf.continuous hf.measurableEmbedding
-- 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 : μ.Regular
f : α → β
hf : IsOpenEmbedding f
this_1 : OuterRegular (comap f μ)
this : IsFiniteMeasureOnCompacts (m0 := inst) (comap f μ)
⊢ Regular (comap f μ)

Tactic:
⟨InnerRegularWRT.comap Regular.innerRegular hf.measurableEmbedding
    (fun _ hU ↦ hf.isOpen_iff_image_isOpen.mp hU)
    (fun _ hKrange hK ↦ hf.isInducing.isCompact_preimage' hK hKrange)⟩

Premises used: MeasureTheory.Measure.Regular.innerRegular, MeasureTheory.Measure.InnerRegularWRT.comap, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, Topology.IsOpenEmbedding.measurableEmbedding, Topology.IsOpenEmbedding.isInducing, Topology.IsInducing.isCompact_preimage', Iff.mp, MeasureTheory.Measure.Regular.mk
-- 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 : μ.Regular
f : α → β
hf : IsOpenEmbedding f
this_1 : OuterRegular (comap f μ)
this : IsFiniteMeasureOnCompacts (m0 := inst) (comap f μ)
⊢ Regular (comap f μ)

Tactic:
exact ⟨InnerRegularWRT.comap Regular.innerRegular hf.measurableEmbedding
    (fun _ hU ↦ hf.isOpen_iff_image_isOpen.mp hU)
    (fun _ hKrange hK ↦ hf.isInducing.isCompact_preimage' hK hKrange)⟩
-- 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 : μ.Regular
f : α ≃ₜ β
⊢ Regular.{u_1} (α := α) (comap (⇑f : (a : α) → β) μ)

Tactic:
Regular.comap' μ f.isOpenEmbedding

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

Tactic:
haveI := OuterRegular.smul μ hx
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
x : ℝ≥0∞
hx : x ≠ ∞
this : (x • μ).OuterRegular
⊢ IsFiniteMeasureOnCompacts (x • μ)

Tactic:
haveI := IsFiniteMeasureOnCompacts.smul μ hx
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
x : ℝ≥0∞
hx : x ≠ ∞
this_1 : (x • μ).OuterRegular
this : IsFiniteMeasureOnCompacts (x • μ)
⊢ (x • μ).Regular

Tactic:
⟨Regular.innerRegular.smul x⟩

Premises used: MeasureTheory.Measure.Regular.innerRegular, MeasureTheory.Measure.InnerRegularWRT.smul, MeasureTheory.Measure.Regular.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
x : ℝ≥0∞
hx : x ≠ ∞
this_1 : (x • μ).OuterRegular
this : IsFiniteMeasureOnCompacts (x • μ)
⊢ (x • μ).Regular

Tactic:
exact ⟨Regular.innerRegular.smul x⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.Regular
c : ℝ≥0
⊢ (c • μ).Regular

Tactic:
Regular.smul coe_ne_top

Premises used: MeasureTheory.Measure.Regular.smul, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
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).WeaklyRegular

Tactic:
have : WeaklyRegular (μ.restrict A) := WeaklyRegular.restrict_of_measure_ne_top h'A
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
innerRegular : (μ.restrict A).InnerRegularWRT IsCompact IsOpen[inst_1]
⊢ (μ.restrict A).Regular

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
rw : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (V ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [restrict_apply hV.measurableSet]

Premises used: MeasureTheory.Measure.restrict_apply, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) ((μ : (a : Set α) → ℝ≥0∞) (V ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
((measure_mono inter_subset_right).trans_lt h'A.lt_top).ne

Premises used: Ne.lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) ((μ : (a : Set α) → ℝ≥0∞) (V ∩ A) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ((measure_mono inter_subset_right).trans_lt h'A.lt_top).ne

Premises used: Ne.lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)

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
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
R : Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K

Tactic:
MeasurableSet.exists_lt_isCompact_of_ne_top hV.measurableSet R hr

Premises used: IsOpen.measurableSet, MeasurableSet.exists_lt_isCompact_of_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
R : Ne (α := ℝ≥0∞) ((μ.restrict A : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A : (a : Set α) → ℝ≥0∞) K

Tactic:
exact MeasurableSet.exists_lt_isCompact_of_ne_top hV.measurableSet R hr

Premises used: IsOpen.measurableSet, MeasurableSet.exists_lt_isCompact_of_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
G : Type u_3
A : Type u_4
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : DistribMulAction G A
inst_4 : MeasurableSpace A
inst_5 : TopologicalSpace A
inst_6 : BorelSpace A
inst_7 : ContinuousConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
inst_8 : μ.Regular
⊢ (g • μ).Regular

Tactic:
.map <| .smul ((DomMulAct.mk.symm g : G)⁻¹)

Premises used: Homeomorph.smul, DomMulAct.mk, Inv.inv, MeasureTheory.Measure.Regular.map, MulOpposite.unop, Equiv.symm, DFunLike.coe
-- 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:
⟨(InnerRegularWRT.isCompact_isClosed μ).trans (InnerRegularWRT.of_pseudoMetrizableSpace μ)⟩

Premises used: MeasureTheory.Measure.InnerRegularWRT.trans, MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace, MeasureTheory.Measure.InnerRegularWRT.isCompact_isClosed, MeasureTheory.Measure.Regular.mk