awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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∞)
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)) ≤ ε
⊢ ∀ᶠ (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']

Premises used: MeasurableSet.exists_isCompact_isClosed_diff_lt, IsOpen.measurableSet, MeasureTheory.MeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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
⊢ NullMeasurableSet K μ

Tactic:
have hKm : NullMeasurableSet K μ := hKcl.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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 μ
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)) ≤ ε
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (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

Premises used: Iff.mp, ContinuousMap.tendsto_nhds_compactOpen
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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
h : (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε / 2 + ε / 2
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε

Tactic:
rw [← ENNReal.add_halves ε]

Premises used: ENNReal.add_halves
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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

Tactic:
(measure_symmDiff_le _ K _).trans ?_

Premises used: MeasureTheory.measure_symmDiff_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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
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
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε / 2 + ε / 2

Tactic:
refine (measure_symmDiff_le _ K _).trans ?_

Premises used: MeasureTheory.measure_symmDiff_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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
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
⊢ 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:
rw [symmDiff_of_ge ha.subset_preimage, symmDiff_of_le hKg.subset_preimage]

Premises used: symmDiff_of_ge, Set.MapsTo.subset_preimage, symmDiff_of_le
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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
h : (μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (a : X) → Y) ⁻¹' s \ K) ≤ ε / 2
⊢ 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:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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∞)
h : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) ≤ ε / 2
⊢ (μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (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']

Premises used: MeasureTheory.measure_diff_le_iff_le_add, Set.MapsTo.subset_preimage, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) ≤ ε / 2

Tactic:
hKμ.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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∞) ((⇑g : (a : X) → Y) ⁻¹' s \ K) ≤ ε / 2

Tactic:
exact hKμ.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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∞)
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
⊢ IsClosed[inst_8] {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds, isOpen_compl_iff
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
⊢ ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < (μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s)

Tactic:
apply gt_mem_nhds

Premises used: gt_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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
h : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞) (0 : ℝ≥0∞)
h₂ h₃ h₄ h₅ : ¬(⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)

Tactic:
rwa [pos_iff_ne_zero, ne_eq, measure_symmDiff_eq_zero_iff]

Premises used: ne_eq, pos_iff_ne_zero, MeasureTheory.measure_symmDiff_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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)

Tactic:
replace hz : ∀ᶠ ε : ℝ≥0∞ in 𝓝 0, ε < μ ((f z ⁻¹' t) ∆ s) := by
    apply gt_mem_nhds
    rwa [pos_iff_ne_zero, ne_eq, measure_symmDiff_eq_zero_iff]
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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 : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < (μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s)
h :
  ∀ (w : Z)
    (hw :
      LT.lt (α := ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f w) : (a : X) → Y) ⁻¹' t) ∆ ((⇑(f z) : (a : X) → Y) ⁻¹' t)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)),
    Membership.mem (γ := Set Z) {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ w
⊢ {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ ∈ 𝓝 z

Tactic:
filter_upwards [(tendsto_measure_symmDiff_preimage_nhds_zero (hf.tendsto z)
    (.of_forall hfm) (hfm z) htm ht).eventually hz] with w hw

Premises used: Filter.Eventually.of_forall, MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero, Continuous.tendsto, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
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 : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < (μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s)
w : Z
hw :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f w) : (a : X) → Y) ⁻¹' t) ∆ ((⇑(f z) : (a : X) → Y) ⁻¹' t)) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
hw' : (⇑(f w) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)

Tactic:
rw [measure_congr (hw'.symmDiff (ae_eq_refl _)), symmDiff_comm] at hw

Premises used: MeasureTheory.measure_congr, symmDiff_comm, MeasureTheory.ae_eq_refl, Filter.EventuallyEq.symmDiff