awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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
⊢ ∃ K ⊆ U, pb K ∧ r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K
have hr₁ : r < (μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' U)
Tactic: rw [f.map_apply U] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊆ U, pb K ∧ r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K
have 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
Tactic: rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
have refine : r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) ((⇑f : (a : α) → β) '' K)
Tactic: refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ r < ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) ((⇑f : (a : α) → β) '' K)
have rwa : r < (μ : (a : Set α) → ℝ≥0∞) (preimage.{u_2, u_3} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' K))
Tactic: rwa [f.map_apply, f.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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
⊢ ∃ K ⊆ U, pa K ∧ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K
have hr₁ : r < (μ : (a : Set β) → ℝ≥0∞) (f '' U)
Tactic: rw [hf.comap_apply] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊆ U, pa K ∧ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K
have 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
Tactic: obtain ⟨K, hKU, hK, hμU⟩ := H (hAB U hU) r hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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 ⊆ U, pa K ∧ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K
have hKrange : K ⊆ range f
Tactic: have hKrange := hKU.trans (image_subset_range _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
have refine_1 : f ⁻¹' K ⊆ U
Tactic: refine ⟨f ⁻¹' K, ?_, hAB' K hKrange hK, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ ∃ K ⊆ U, pa K ∧ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) K
have refine_2 : r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' K)
Tactic: refine ⟨f ⁻¹' K, ?_, hAB' K hKrange hK, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊆ U
have refine_1 : f ⁻¹' K ⊆ f ⁻¹' f '' U
Tactic: rw [← hf.injective.preimage_image U]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ r < ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' K)
have refine_2 : r < (μ : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' K)
Tactic: rwa [hf.comap_apply, image_preimage_eq_iff.mpr hKrange]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ : (a : Set α) → ℝ≥0∞) K
have hr₁ : 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
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ ∃ K ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have rcases : ∀ (F : Set α) (hFU : F ⊆ U) (hqF : q F) (hF : r < (μ : (a : Set α) → ℝ≥0∞) F),
  ∃ K ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases H' hU r hr with ⟨F, hFU, hqF, hF⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have rcases : ∀ (K : Set α) (hKF : K ⊆ F) (hpK : p K) (hrK : r < (μ : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ U, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases H hqF _ hF with ⟨K, hKF, hpK, hrK⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) A < r
⊢ r > (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ A)
have rwa : r > (μ : (a : Set α) → ℝ≥0∞) A
Tactic: rwa [measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) A < r
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
have 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
Tactic: rcases OuterRegular.outerRegular (measurableSet_toMeasurable μ A) r
      (by rwa [measure_toMeasurable]) with
    ⟨U, hAU, hUo, hU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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∞)
have refine : LE.le (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: refine le_antisymm (le_iInf₂ fun s hs => le_iInf fun _ => μ.mono hs) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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∞)
have refine : ∀ (r : ℝ≥0∞) (hr : (μ : (a : Set α) → ℝ≥0∞) A < r),
  ⨅ (U : Set α), ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U < r
Tactic: refine le_of_forall_gt fun r hr => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
A : Set α
μ : Measure α
inst_2 : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
have 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∞) ε
Tactic: rcases eq_or_ne (μ A) ∞ with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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∞) ε
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
have 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∞) ε
Tactic: rcases eq_or_ne (μ A) ∞ with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊇ A, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ε
have 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∞) ε
Tactic: rcases A.exists_isOpen_lt_add H hε with ⟨U, AU, U_open, hU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊇ A,
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U \ A) < ε
have 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) < ε
Tactic: rcases A.exists_isOpen_lt_add hA' hε with ⟨U, hAU, hUo, hU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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∞) ε
⊢ ∃ U ⊇ A,
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U \ A) < ε
have right : (μ : (a : Set α) → ℝ≥0∞) (U \ A) < ε
Tactic: use U, hAU, hUo, hU.trans_le le_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 : α) → β) μ)
have 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
Tactic: refine ⟨fun A hA r hr => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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
⊢ ∃ U ⊇ A, IsOpen[inst_4] U ∧ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) U < r
have hr₁ : r > (μ : (a : Set α) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) '' A)
Tactic: rw [map_apply f.measurable hA, ← f.image_symm] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊇ A, IsOpen[inst_4] U ∧ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) U < r
have 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
Tactic: rcases Set.exists_isOpen_lt_of_lt _ r hr with ⟨U, hAU, hUo, hU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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
⊢ ∃ U ⊇ A, IsOpen[inst_4] U ∧ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) U < r
have this : IsOpen[inst_4] ((⇑f.symm : (a : β) → α) ⁻¹' U)
Tactic: have : IsOpen (f.symm ⁻¹' U) := hUo.preimage f.symm.continuous
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
have refine : ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) ⁻¹' U) < r
Tactic: refine ⟨f.symm ⁻¹' U, image_subset_iff.1 hAU, this, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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)
⊢ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) ⁻¹' U) < r
have rwa : (μ : (a : Set α) → ℝ≥0∞) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f.symm : (a : β) → α) ⁻¹' U)) < r
Tactic: rwa [map_apply f.measurable this.measurableSet, f.preimage_symm, f.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ ((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) ((⇑f.symm : (a : β) → α) ⁻¹' U) < r
have rwa₁ : (μ : (a : Set α) → ℝ≥0∞) (preimage.{u_1, u_2} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' U)) < r
Tactic: rwa [map_apply f.measurable this.measurableSet, f.preimage_symm, f.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
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
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) U < r
have hr₁ : r > (μ : (a : Set β) → ℝ≥0∞) (f '' A)
Tactic: rw [f_me.comap_apply] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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 ⊇ A, IsOpen[inst_1] U ∧ ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) U < r
have 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
Tactic: obtain ⟨U, hUA, Uopen, hμU⟩ := OuterRegular.outerRegular (f_me.measurableSet_image' hA) r hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ f ⁻¹' U ⊇ A
have rwa : A ⊆ f ⁻¹' U
Tactic: rwa [Superset, ← image_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ f ⁻¹' U ⊇ A
have rwa₁ : f '' A ⊆ U
Tactic: rwa [Superset, ← image_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
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
⊢ ∃ U ⊇ A, IsOpen[inst_1] U ∧ ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) U < r
have refine : ((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' U) < r
Tactic: refine ⟨f ⁻¹' U, by rwa [Superset, ← image_subset_iff], Uopen.preimage f_cont, ?_⟩