awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
inr :
  ∀ (K : Set α) (hKU : K ⊆ U) (hKc : p K)
    (hrK : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε < (μ : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
rcases H hU _ (ENNReal.sub_lt_self hμU h₀ hε) with ⟨K, hKU, hKc, hrK⟩

Premises used: ENNReal.sub_lt_self
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
K : Set α
hKU : K ⊆ U
hKc : p K
hrK : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
⟨K, hKU, hKc, ENNReal.lt_add_of_sub_lt_right (Or.inl hμU) hrK⟩

Premises used: ENNReal.lt_add_of_sub_lt_right, And.intro, Exists.intro, Or.inl
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
K : Set α
hKU : K ⊆ U
hKc : p K
hrK : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
exact ⟨K, hKU, hKc, ENNReal.lt_add_of_sub_lt_right (Or.inl hμU) hrK⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) U
⊢ r < (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U)

Tactic:
rw [map_apply_of_aemeasurable hf (hB₂ _ hU)] at hr

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U)
rcases :
  ∀ (K : Set α) (hKU : K ⊆ f ⁻¹' U) (hKc : pa K) (hK : r < (μ : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ U, pb K ∧ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, pb K ∧ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) K

Tactic:
rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U)
K : Set α
hKU : K ⊆ f ⁻¹' U
hKc : pa K
hK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, pb K ∧ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) K

Tactic:
⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Set.image, Set.image_subset_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U)
K : Set α
hKU : K ⊆ f ⁻¹' U
hKc : pa K
hK : r < (μ : (a : Set α) → ℝ≥0∞) K
refine : r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' K)
⊢ ∃ K ⊆ U, pb K ∧ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) K

Tactic:
refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U)
K : Set α
hKU : K ⊆ f ⁻¹' U
hKc : pa K
hK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' K)

Tactic:
hK.trans_le (le_map_apply_image hf _)

Premises used: LT.lt.trans_le, MeasureTheory.Measure.le_map_apply_image
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U)
K : Set α
hKU : K ⊆ f ⁻¹' U
hKc : pa K
hK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' K)

Tactic:
exact hK.trans_le (le_map_apply_image hf _)

Premises used: LT.lt.trans_le, MeasureTheory.Measure.le_map_apply_image
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa ((⇑f : (a : α) → β) ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb ((⇑f : (a : α) → β) '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) U
⊢ r < (μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' U)

Tactic:
rw [f.map_apply U] at hr

Premises used: MeasurableEquiv.map_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa ((⇑f : (a : α) → β) ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb ((⇑f : (a : α) → β) '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' U)
rcases :
  ∀ (K : Set α) (hKU : K ⊆ (⇑f : (a : α) → β) ⁻¹' U) (hKc : pa K) (hK : r < (μ : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ U, pb K ∧ r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, pb K ∧ r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K

Tactic:
rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa ((⇑f : (a : α) → β) ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb ((⇑f : (a : α) → β) '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' U)
K : Set α
hKU : K ⊆ (⇑f : (a : α) → β) ⁻¹' U
hKc : pa K
hK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, pb K ∧ r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K

Tactic:
⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Set.image, Set.image_subset_iff, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa ((⇑f : (a : α) → β) ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb ((⇑f : (a : α) → β) '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' U)
K : Set α
hKU : K ⊆ (⇑f : (a : α) → β) ⁻¹' U
hKc : pa K
hK : r < (μ : (a : Set α) → ℝ≥0∞) K
refine : r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) ((⇑f : (a : α) → β) '' K)
⊢ ∃ K ⊆ U, pb K ∧ r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K

Tactic:
refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α ≃ᵐ β
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa ((⇑f : (a : α) → β) ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb ((⇑f : (a : α) → β) '' K)
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' U)
K : Set α
hKU : K ⊆ (⇑f : (a : α) → β) ⁻¹' U
hKc : pa K
hK : r < (μ : (a : Set α) → ℝ≥0∞) K
rwa : r < (μ : (a : Set α) → ℝ≥0∞) (preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' K))
rwa₁ rwa₂ rwa₃ rwa₄ : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) ((⇑f : (a : α) → β) '' K)

Tactic:
rwa [f.map_apply, f.preimage_image]

Premises used: MeasurableEquiv.map_apply, MeasurableEquiv.preimage_image
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) U
⊢ r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)

Tactic:
rw [hf.comap_apply] at hr

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)
obtain :
  ∀ (K : Set β) (hKU : K ⊆ f '' U) (hK : pb K) (hμU : r < (μ : (a : Set β) → ℝ≥0∞) K),
    ∃ K ⊆ U, pa K ∧ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, pa K ∧ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K

Tactic:
obtain ⟨K, hKU, hK, hμU⟩ := H (hAB U hU) r hr
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < (μ : (a : Set β) → ℝ≥0∞) K
⊢ K ⊆ range f

Tactic:
have hKrange := hKU.trans (image_subset_range _ _)
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < (μ : (a : Set β) → ℝ≥0∞) K
hKrange : K ⊆ range f
⊢ ∃ K ⊆ U, pa K ∧ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K

Tactic:
⟨f ⁻¹' K, ?_, hAB' K hKrange hK, ?_⟩

Premises used: Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < (μ : (a : Set β) → ℝ≥0∞) K
hKrange : K ⊆ range f
refine_1 : f ⁻¹' K ⊆ U
refine_2 : r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' K)
⊢ ∃ K ⊆ U, pa K ∧ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K

Tactic:
refine ⟨f ⁻¹' K, ?_, hAB' K hKrange hK, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < (μ : (a : Set β) → ℝ≥0∞) K
hKrange : K ⊆ range f
refine_1 : f ⁻¹' K ⊆ f ⁻¹' f '' U
⊢ f ⁻¹' K ⊆ U

Tactic:
rw [← hf.injective.preimage_image U]

Premises used: MeasurableEmbedding.injective, Function.Injective.preimage_image
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < (μ : (a : Set β) → ℝ≥0∞) K
hKrange : K ⊆ range f
⊢ f ⁻¹' K ⊆ f ⁻¹' f '' U

Tactic:
preimage_mono hKU

Premises used: Set.preimage_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < (μ : (a : Set β) → ℝ≥0∞) K
hKrange : K ⊆ range f
⊢ f ⁻¹' K ⊆ f ⁻¹' f '' U

Tactic:
exact preimage_mono hKU

Premises used: Set.preimage_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < (μ : (a : Set β) → ℝ≥0∞) K
hKrange : K ⊆ range f
refine_2 : r < (μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' K)
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : r < (μ : (a : Set β) → ℝ≥0∞) K
⊢ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' K)

Tactic:
rwa [hf.comap_apply, image_preimage_eq_iff.mpr hKrange]

Premises used: Iff.mpr, MeasurableEmbedding.comap_apply, Set.image_preimage_eq_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < (c • μ : (a : Set α) → ℝ≥0∞) U
⊢ r < c * ⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rw [smul_apply, H.measure_eq_iSup hU, smul_eq_mul] at hr

Premises used: MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup, MeasureTheory.Measure.smul_apply, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < c * ⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ : (a : Set α) → ℝ≥0∞) K

Tactic:
simpa only [ENNReal.mul_iSup, lt_iSup_iff, exists_prop] using hr

Premises used: exists_prop, ENNReal.mul_iSup, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) U
rcases :
  ∀ (F : Set α) (hFU : F ⊆ U) (hqF : q F) (hF : r < (μ : (a : Set α) → ℝ≥0∞) F),
    ∃ K ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases H' hU r hr with ⟨F, hFU, hqF, hF⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < (μ : (a : Set α) → ℝ≥0∞) F
rcases :
  ∀ (K : Set α) (hKF : K ⊆ F) (hpK : p K) (hrK : r < (μ : (a : Set α) → ℝ≥0∞) K),
    ∃ K ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
rcases H hqF _ hF with ⟨K, hKF, hpK, hrK⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < (μ : (a : Set α) → ℝ≥0∞) F
K : Set α
hKF : K ⊆ F
hpK : p K
hrK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
⟨K, hKF.trans hFU, hpK, hrK⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < (μ : (a : Set α) → ℝ≥0∞) F
K : Set α
hKF : K ⊆ F
hpK : p K
hrK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
exact ⟨K, hKF.trans hFU, hpK, hrK⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : Set α → Prop
⊢ μ.InnerRegularWRT p p

Tactic:
fun U hU _r hr ↦ ⟨U, Subset.rfl, hU, hr⟩

Premises used: MeasureTheory.Measure.InnerRegularWRT, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
h : ∀ (s : Set α), q s → p s
⊢ μ.InnerRegularWRT p q

Tactic:
fun U hU _ hr ↦ ⟨U, Subset.rfl, h U hU, hr⟩

Premises used: MeasureTheory.Measure.InnerRegularWRT, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q p' q' : Set α → Prop
H : μ.InnerRegularWRT p q
h : ∀ (s : Set α), q' s → q s
h' : ∀ (s : Set α), p s → p' s
⊢ μ.InnerRegularWRT p' q'

Tactic:
of_imp h' |>.trans H |>.trans (of_imp h)

Premises used: MeasureTheory.Measure.InnerRegularWRT.trans, MeasureTheory.Measure.InnerRegularWRT.of_imp
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
⊢ OuterRegular.{u_1} (α := α) 0

Tactic:
⟨fun A _ _r hr => ⟨univ, subset_univ A, isOpen_univ, hr⟩⟩

Premises used: Set.subset_univ, Set.univ, isOpen_univ, And.intro, Exists.intro, MeasureTheory.Measure.OuterRegular.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) A < r
rwa rwa₁ rwa₂ rwa₃ : r > (μ : (a : Set α) → ℝ≥0∞) A
⊢ r > (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ A)

Tactic:
rwa [measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) A < r
rcases :
  ∀ (U : Set α) (hAU : U ⊇ toMeasurable μ A) (hUo : IsOpen[inst_1] U) (hU : (μ : (a : Set α) → ℝ≥0∞) U < r),
    ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
rcases OuterRegular.outerRegular (measurableSet_toMeasurable μ A) r
      (by rwa [measure_toMeasurable]) with
    ⟨U, hAU, hUo, hU⟩

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasureTheory.Measure.OuterRegular.outerRegular
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) A < r
U : Set α
hAU : U ⊇ toMeasurable μ A
hUo : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
⟨U, (subset_toMeasurable _ _).trans hAU, hUo, hU⟩

Premises used: HasSubset.Subset.trans, MeasureTheory.subset_toMeasurable, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) A < r
U : Set α
hAU : U ⊇ toMeasurable μ A
hUo : IsOpen[inst_1] U
hU : (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
exact ⟨U, (subset_toMeasurable _ _).trans hAU, hUo, hU⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
le_antisymm (le_iInf₂ fun s hs => le_iInf fun _ => μ.mono hs) ?_

Premises used: MeasureTheory.OuterMeasure.mono, le_iInf, le_iInf₂, MeasureTheory.Measure.toOuterMeasure, le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
refine :
  LE.le (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
refine le_antisymm (le_iInf₂ fun s hs => le_iInf fun _ => μ.mono hs) ?_

Premises used: MeasureTheory.OuterMeasure.mono, le_iInf, le_iInf₂, MeasureTheory.Measure.toOuterMeasure, le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
⊢ LE.le (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
le_of_forall_gt fun r hr => ?_

Premises used: le_of_forall_gt