awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ Eq (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
refine_1 :
  LE.le (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
refine_2 :
  LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
    (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
refine_1 :
  ∀ (ε : ℝ≥0),
    0 < ε →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
apply ENNReal.le_of_forall_pos_le_add

Premises used: ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
refine_1 :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  ∀ (K' : Compacts G)
    (K'_hyp :
      K.carrier ⊆ interior K'.carrier ∧
        (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)),
    ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨K', K'_hyp⟩ := contentRegular_exists_compact μ H K (ne_bot_of_gt εpos)

Premises used: ne_bot_of_gt, MeasureTheory.Content.contentRegular_exists_compact
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
K' : Compacts G
K'_hyp :
  K.carrier ⊆ interior K'.carrier ∧
    (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)
    (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (interior (↑K' : Set G)) : ℝ≥0∞)

Tactic:
measure_mono K'_hyp.1

Premises used: And.left, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
K' : Compacts G
K'_hyp :
  K.carrier ⊆ interior K'.carrier ∧
    (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
rw :
  LE.le (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (interior (↑K' : Set G)) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K' : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (interior (↑K' : Set G)) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K' : ℝ≥0∞)

Tactic:
rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]

Premises used: isOpen_interior, IsOpen.measurableSet, MeasureTheory.Content.measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
K' : Compacts G
K'_hyp :
  K.carrier ⊆ interior K'.carrier ∧
    (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (interior (↑K' : Set G)) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K' : ℝ≥0∞)

Tactic:
μ.outerMeasure_interior_compacts K'

Premises used: MeasureTheory.Content.outerMeasure_interior_compacts
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
K' : Compacts G
K'_hyp :
  K.carrier ⊆ interior K'.carrier ∧
    (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (interior (↑K' : Set G)) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K' : ℝ≥0∞)

Tactic:
exact μ.outerMeasure_interior_compacts K'

Premises used: MeasureTheory.Content.outerMeasure_interior_compacts
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
K' : Compacts G
K'_hyp :
  K.carrier ⊆ interior K'.carrier ∧
    (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
K'_hyp.right

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
K' : Compacts G
K'_hyp :
  K.carrier ⊆ interior K'.carrier ∧
    (μ : (a : Compacts G) → ℝ≥0∞) K' ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
measure_mono :
  LE.le (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (interior (↑K' : Set G)) : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) K' : ℝ≥0∞)
⊢ ((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
calc
      μ.measure ↑K ≤ μ.measure (interior ↑K') := measure_mono K'_hyp.1
      _ ≤ μ K' := by
        rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]
        exact μ.outerMeasure_interior_compacts K'
      _ ≤ μ K + ε := K'_hyp.right

Premises used: SetLike.coe, And.right, And.left, MeasureTheory.Content.measure, interior, MeasureTheory.measure_mono, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
    ((μ : (a : Compacts G) → ℝ≥0∞) { carrier := closure (↑K : Set G), isCompact' := ⋯ } : ℝ≥0∞)

Tactic:
μ.mono _ _ subset_closure

Premises used: subset_closure, MeasureTheory.Content.mono
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
rw :
  LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) { carrier := closure (↑K : Set G), isCompact' := ⋯ } : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (closure (↑K : Set G)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) { carrier := closure (↑K : Set G), isCompact' := ⋯ } : ℝ≥0∞)
    (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (closure (↑K : Set G)) : ℝ≥0∞)

Tactic:
rw [μ.measure_apply (isClosed_closure.measurableSet)]

Premises used: IsClosed.measurableSet, isClosed_closure, MeasureTheory.Content.measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) { carrier := closure (↑K : Set G), isCompact' := ⋯ } : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (closure (↑K : Set G)) : ℝ≥0∞)

Tactic:
μ.le_outerMeasure_compacts _

Premises used: MeasureTheory.Content.le_outerMeasure_compacts, setOf, closure, Set.sInter
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) { carrier := closure (↑K : Set G), isCompact' := ⋯ } : ℝ≥0∞)
    ((μ.outerMeasure : (a : Set G) → ℝ≥0∞) (closure (↑K : Set G)) : ℝ≥0∞)

Tactic:
exact μ.le_outerMeasure_compacts _

Premises used: MeasureTheory.Content.le_outerMeasure_compacts
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ Eq (α := ℝ≥0∞) (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (closure (↑K : Set G)) : ℝ≥0∞)
    (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)

Tactic:
K.2.measure_closure _

Premises used: IsCompact.measure_closure, TopologicalSpace.Compacts.isCompact'
-- Module: Mathlib.MeasureTheory.Measure.Content
Goal:
G : Type w
inst : TopologicalSpace G
μ : Content G
inst_1 : MeasurableSpace G
inst_2 : R1Space G
inst_3 : BorelSpace G
H : μ.ContentRegular
K : Compacts G
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) { carrier := closure (↑K : Set G), isCompact' := ⋯ } : ℝ≥0∞)
    (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (closure (↑K : Set G)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Compacts G) → ℝ≥0∞) K : ℝ≥0∞)
    (((μ.measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K : Set G) : ℝ≥0∞)

Tactic:
calc
    μ K ≤ μ ⟨closure K, K.2.closure⟩ := μ.mono _ _ subset_closure
    _ ≤ μ.measure (closure K) := by
      rw [μ.measure_apply (isClosed_closure.measurableSet)]
      exact μ.le_outerMeasure_compacts _
    _ = μ.measure K := K.2.measure_closure _

Premises used: IsCompact.measure_closure, MeasureTheory.Content.mono, TopologicalSpace.Compacts.isCompact', IsCompact.closure, TopologicalSpace.Compacts.mk, SetLike.coe, closure, MeasureTheory.Content.measure, 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∞)
rw : Measure.InnerRegularCompactLTTop.{u_3} (α := Y) (Measure.map (⇑g : (a : X) → Y) μ)
⊢ ν.InnerRegularCompactLTTop

Tactic:
rw [← hg.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- 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∞)
⊢ Measure.InnerRegularCompactLTTop.{u_3} (α := Y) (Measure.map (⇑g : (a : X) → Y) μ)

Tactic:
.map_of_continuous (map_continuous _)

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.map_of_continuous, ContinuousMapClass.map_continuous
-- 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∞)
⊢ Measure.InnerRegularCompactLTTop.{u_3} (α := Y) (Measure.map (⇑g : (a : X) → Y) μ)

Tactic:
exact .map_of_continuous (map_continuous _)
-- 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∞)
⊢ ν.InnerRegularCompactLTTop

Tactic:
have : ν.InnerRegularCompactLTTop := by
    rw [← hg.map_eq]
    exact .map_of_continuous (map_continuous _)
-- 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 : ν.InnerRegularCompactLTTop
rw :
  ∀ ε > 0, ∀ᶠ (x : α) in l, (μ : (a : Set X) → ℝ≥0∞) (((⇑(f x) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s)) ≤ ε
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : α) ↦ (μ : (a : Set X) → ℝ≥0∞) (((⇑(f a) : (a : X) → Y) ⁻¹' s) ∆ ((⇑g : (a : X) → Y) ⁻¹' s))) l (𝓝 0)

Tactic:
rw [ENNReal.tendsto_nhds_zero]

Premises used: ENNReal.tendsto_nhds_zero
-- 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 : ν.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)) ≤ ε
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)) ≤ ε
⊢ ∀ᶠ (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 ε

Premises used: IsOpen
-- 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
⊢ 0 < ε / 3

Tactic:
have H : 0 < ε / 3 := ENNReal.div_pos hε.ne' ENNReal.coe_ne_top
-- 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
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)) ≤ ε
⊢ ∀ᶠ (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⟩

Premises used: MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt, 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∞)
hUs : (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) < ε / 3
⊢ NullMeasurableSet U ν

Tactic:
have hmU : NullMeasurableSet U ν := hUo.measurableSet.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)
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 ν
⊢ (ν : (a : Set Y) → ℝ≥0∞) (U ∆ s) ≤ ε / 3

Tactic:
replace hUs := hUs.le