awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y} (hs : NullMeasurableSet s ν) (hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
    (ε : ℝ≥0∞) (hε : ε > 0) (hso : IsOpen[inst_4] s),
    ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst_4] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst_4] U
hU : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hmU : NullMeasurableSet U ν
hUs : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
ha : (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' U)) ≤ ε / 3
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have μ₁ : (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤
  HAdd.hAdd (β := ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞))
    ((μ : (a : Set X) → ℝ≥0∞) (((⇑g : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) : ℝ≥0∞)
Tactic: calc
      μ ((f a ⁻¹' s) ∆ (g ⁻¹' s))
        ≤ μ ((f a ⁻¹' s) ∆ (f a ⁻¹' U)) + μ ((f a ⁻¹' U) ∆ (g ⁻¹' U))
          + μ ((g ⁻¹' U) ∆ (g ⁻¹' s)) := by
        refine (measure_symmDiff_le _ (g ⁻¹' U) _).trans ?_
        gcongr
        apply measure_symmDiff_le
      _ ≤ ε / 3 + ε / 3 + ε / 3 := by
        gcongr
        · rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]
        · rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs)]
      _ = ε := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y} (hs : NullMeasurableSet s ν) (hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
    (ε : ℝ≥0∞) (hε : ε > 0) (hso : IsOpen[inst_4] s),
    ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst_4] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst_4] U
hU : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hmU : NullMeasurableSet U ν
hUs : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
ha : (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' U)) ≤ ε / 3
μ₁ :
  (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞))
      ((μ : (a : Set X) → ℝ≥0∞) (((⇑g : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) : ℝ≥0∞)
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have μ₂ : HAdd.hAdd (β := ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞))
    ((μ : (a : Set X) → ℝ≥0∞) (((⇑g : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) : ℝ≥0∞) ≤
  ε / 3 + ε / 3 + ε / 3
Tactic: calc
      μ ((f a ⁻¹' s) ∆ (g ⁻¹' s))
        ≤ μ ((f a ⁻¹' s) ∆ (f a ⁻¹' U)) + μ ((f a ⁻¹' U) ∆ (g ⁻¹' U))
          + μ ((g ⁻¹' U) ∆ (g ⁻¹' s)) := by
        refine (measure_symmDiff_le _ (g ⁻¹' U) _).trans ?_
        gcongr
        apply measure_symmDiff_le
      _ ≤ ε / 3 + ε / 3 + ε / 3 := by
        gcongr
        · rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]
        · rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs)]
      _ = ε := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this_1 : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y} (hs : NullMeasurableSet s ν) (hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
    (ε : ℝ≥0∞) (hε : ε > 0) (hso : IsOpen[inst_4] s),
    ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst_4] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst_4] U
hU : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hmU : NullMeasurableSet U ν
hUs : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
ha : (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' U)) ≤ ε / 3
μ₁ :
  (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤
    HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞))
      ((μ : (a : Set X) → ℝ≥0∞) (((⇑g : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) : ℝ≥0∞)
μ₂ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' U)) : ℝ≥0∞))
      ((μ : (a : Set X) → ℝ≥0∞) (((⇑g : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) : ℝ≥0∞) ≤
    ε / 3 + ε / 3 + ε / 3
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have μ₃ : ε / 3 + ε / 3 + ε / 3 = ε
Tactic: calc
      μ ((f a ⁻¹' s) ∆ (g ⁻¹' s))
        ≤ μ ((f a ⁻¹' s) ∆ (f a ⁻¹' U)) + μ ((f a ⁻¹' U) ∆ (g ⁻¹' U))
          + μ ((g ⁻¹' U) ∆ (g ⁻¹' s)) := by
        refine (measure_symmDiff_le _ (g ⁻¹' U) _).trans ?_
        gcongr
        apply measure_symmDiff_le
      _ ≤ ε / 3 + ε / 3 + ε / 3 := by
        gcongr
        · rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]
        · rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs)]
      _ = ε := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (hypothesis)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hνs' : μ (g ⁻¹' s) ≠ ∞ := by rwa [hg.measure_preimage hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have obtain : ∀ (K : Set X) (hKg : MapsTo (⇑g : (a : X) → Y) K s) (hKco : IsCompact K) (hKcl : IsClosed[inst] K)
  (hKμ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) < ε / 2),
  ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
Tactic: obtain ⟨K, hKg, hKco, hKcl, hKμ⟩ :
      ∃ K, MapsTo g K s ∧ IsCompact K ∧ IsClosed K ∧ μ (g ⁻¹' s \ K) < ε / 2 :=
    (hg.measurable hso.measurableSet).exists_isCompact_isClosed_diff_lt hνs' <| by simp [hε.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (hypothesis)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set X
hKg : MapsTo (⇑g : (a : X) → Y) K s
hKco : IsCompact K
hKcl : IsClosed[inst] K
hKμ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) < ε / 2
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have hKm : NullMeasurableSet K μ
Tactic: have hKm : NullMeasurableSet K μ := hKcl.nullMeasurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set X
hKg : MapsTo (⇑g : (a : X) → Y) K s
hKco : IsCompact K
hKcl : IsClosed[inst] K
hKμ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have h : ∀ (a : α) (hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν) (ha : MapsTo (⇑(f a) : (a : X) → Y) K s),
  (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
Tactic: filter_upwards [hf, ContinuousMap.tendsto_nhds_compactOpen.mp hfg K hKco s hso hKg] with a hfa ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set X
hKg : MapsTo (⇑g : (a : X) → Y) K s
hKco : IsCompact K
hKcl : IsClosed[inst] K
hKμ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
ha : MapsTo (⇑(f a) : (a : X) → Y) K s
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have h : (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε / 2 + ε / 2
Tactic: rw [← ENNReal.add_halves ε]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set X
hKg : MapsTo (⇑g : (a : X) → Y) K s
hKco : IsCompact K
hKcl : IsClosed[inst] K
hKμ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
ha : MapsTo (⇑(f a) : (a : X) → Y) K s
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε / 2 + ε / 2
have h : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ K) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (K ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) : ℝ≥0∞) ≤
  ε / 2 + ε / 2
Tactic: refine (measure_symmDiff_le _ K _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set X
hKg : MapsTo (⇑g : (a : X) → Y) K s
hKco : IsCompact K
hKcl : IsClosed[inst] K
hKμ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
ha : MapsTo (⇑(f a) : (a : X) → Y) K s
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ K) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (K ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) : ℝ≥0∞) ≤
    ε / 2 + ε / 2
have h : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (a : X) → Y) ⁻¹' s \ K) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) : ℝ≥0∞) ≤
  ε / 2 + ε / 2
Tactic: rw [symmDiff_of_ge ha.subset_preimage, symmDiff_of_le hKg.subset_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set X
hKg : MapsTo (⇑g : (a : X) → Y) K s
hKco : IsCompact K
hKcl : IsClosed[inst] K
hKμ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
ha : MapsTo (⇑(f a) : (a : X) → Y) K s
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (a : X) → Y) ⁻¹' s \ K) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) : ℝ≥0∞) ≤
    ε / 2 + ε / 2
have h : (μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (a : X) → Y) ⁻¹' s \ K) ≤ ε / 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (hypothesis)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set X
hKg : MapsTo (⇑g : (a : X) → Y) K s
hKco : IsCompact K
hKcl : IsClosed[inst] K
hKμ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
ha : MapsTo (⇑(f a) : (a : X) → Y) K s
⊢ (μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (a : X) → Y) ⁻¹' s \ K) ≤ ε / 2
have hK' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hK' : μ K ≠ ∞ := ne_top_of_le_ne_top hνs' <| measure_mono hKg.subset_preimage
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
hg : MeasurePreserving (⇑g : (a : X) → Y) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst_4] s
hνs' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set X
hKg : MapsTo (⇑g : (a : X) → Y) K s
hKco : IsCompact K
hKcl : IsClosed[inst] K
hKμ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a) : (a : X) → Y) μ ν
ha : MapsTo (⇑(f a) : (a : X) → Y) K s
hK' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (a : X) → Y) ⁻¹' s \ K) ≤ ε / 2
have h : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) ≤ ε / 2
Tactic: rw [measure_diff_le_iff_le_add hKm ha.subset_preimage hK', hfa.measure_preimage hs,
    ← hg.measure_preimage hs, ← measure_diff_le_iff_le_add hKm hKg.subset_preimage hK']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
inst_8 : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst_8, _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z) : (a : X) → Y) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsClosed[inst_8] {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}
have rw : ∀ (x : Z),
  Membership.mem (γ := Set Z) {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ x →
    {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ ∈ 𝓝 x
Tactic: rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
inst_8 : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst_8, _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z) : (a : X) → Y) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
z : Z
hz : Membership.mem (γ := Set Z) {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ z
⊢ ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < (μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s)
have h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
Tactic: apply gt_mem_nhds