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 : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
inr :
  ∀
    (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),
    ∀ᶠ (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)) ≤ ε
have wlog : ∀ {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)) ≤ ε
Tactic: wlog hso : IsOpen s generalizing s ε
Cleared hypotheses: s, hs, hνs, ε, hε
-- 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)
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
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have H : 0 < ε / 3
Tactic: have H : 0 < ε / 3 := ENNReal.div_pos hε.ne' ENNReal.coe_ne_top
-- 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
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have inr : ∀ (U : Set Y) (hUo : IsOpen[inst_4] U) (hU : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hUs : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) < ε / 3),
  ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
Tactic: rcases hs.exists_isOpen_symmDiff_lt hνs H.ne' with ⟨U, hUo, hU, hUs⟩
-- 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)
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∞)
hUs : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) < ε / 3
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have hmU : NullMeasurableSet U ν
Tactic: have hmU : NullMeasurableSet U ν := hUo.measurableSet.nullMeasurableSet
-- 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)
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∞)
hUs : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) < ε / 3
hmU : NullMeasurableSet U ν
⊢ ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
have hUs₁ : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) ≤ ε / 3
Tactic: replace hUs := hUs.le
Cleared hypotheses: hUs
-- 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
⊢ ∀ᶠ (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 : (μ : (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)) ≤ ε
Tactic: filter_upwards [hf, this hmU hU.ne _ H hUo] 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)
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∞)
have 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∞)
Tactic: refine (measure_symmDiff_le _ (g ⁻¹' U) _).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)
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
⊢ 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∞)
have 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∞)
Tactic: gcongr
-- 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
⊢ 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
have h₁ : (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) ≤ ε / 3
Tactic: gcongr
-- 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
h₁ : (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) ≤ ε / 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
have h₂ : (μ : (a : Set X) → ℝ≥0∞) (((⇑g : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε / 3
Tactic: gcongr
-- 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) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) ≤ ε / 3
have h₁ : (μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (a : X) → Y) ⁻¹' s ∆ U) ≤ ε / 3
Tactic: rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]
-- 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
h₁ : (μ : (a : Set X) → ℝ≥0∞) ((⇑(f a) : (a : X) → Y) ⁻¹' s ∆ U) ≤ ε / 3
⊢ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(f a) : (a : X) → Y) ⁻¹' U)) ≤ ε / 3
have h₂ : (ν : (a : Set Y) → ℝ≥0∞) (s ∆ U) ≤ ε / 3
Tactic: rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]
-- 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∞) (((⇑g : (a : X) → Y) ⁻¹' U) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε / 3
have h₂ : (μ : (a : Set X) → ℝ≥0∞) ((⇑g : (a : X) → Y) ⁻¹' U ∆ s) ≤ ε / 3
Tactic: rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs)]