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)
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
h :
  ∀ (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)) ≤ ε
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε

Tactic:
filter_upwards [hf, this hmU hU.ne _ H hUo] with a hfa ha

Premises used: LT.lt.ne
-- 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)
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∞)

Tactic:
(measure_symmDiff_le _ (g ⁻¹' U) _).trans ?_

Premises used: MeasureTheory.measure_symmDiff_le, Set.preimage, LE.le.trans, DFunLike.coe
-- 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)
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
refine :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑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∞)
⊢ (μ : (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:
refine (measure_symmDiff_le _ (g ⁻¹' U) _).trans ?_

Premises used: MeasureTheory.measure_symmDiff_le, Set.preimage, LE.le.trans, DFunLike.coe
-- 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)
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
bc :
  (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' U)) ≤
    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∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑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∞)

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)
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) ⁻¹' U)) ≤
    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∞)

Tactic:
apply measure_symmDiff_le

Premises used: MeasureTheory.measure_symmDiff_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)
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
h₁ : (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) ≤ ε / 3
h₂ : (μ : (a : Set X) → ℝ≥0∞) (((⇑g : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε / 3
⊢ 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:
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)
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
h₁ : (μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (a : X) → Y) ⁻¹' s ∆ U) ≤ ε / 3
h₂ : (ν : (a : Set Y) → ℝ≥0∞) (s ∆ U) ≤ ε / 3
h₃ h₄ h₅ h₆ : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) ≤ ε / 3
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) ≤ ε / 3

Tactic:
rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]

Premises used: symmDiff_comm, Set.preimage_symmDiff, MeasureTheory.NullMeasurableSet.symmDiff, 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)
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
h₂ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' U ∆ s) ≤ ε / 3
h₃ h₄ h₅ h₆ : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) ≤ ε / 3
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑g : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε / 3

Tactic:
rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs)]

Premises used: Set.preimage_symmDiff, MeasureTheory.NullMeasurableSet.symmDiff, 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)
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
⊢ ε / 3 + ε / 3 + ε / 3 = ε

Tactic:
simp
-- 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)
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
μ₃ : ε / 3 + ε / 3 + ε / 3 = ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε

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

Premises used: Set.preimage, DFunLike.coe, symmDiff
-- 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
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [hg.measure_preimage hs]

Premises used: 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
⊢ 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]
-- 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∞)
⊢ ε / 2 ≠ 0

Tactic:
simp [hε.ne']

Premises used: LT.lt.ne'