awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
a : X
ha : a ∈ U ∩ {a : X | f a ≠ g a}
ha₁ : a ∈ U
⊢ (f a, g a) ∈ (diagonal Y)ᶜ

Tactic:
rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩

Premises used: Prod.mk, Set.diagonal
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
a : X
ha : a ∈ U
ha' : (f a, g a) ∈ (diagonal Y)ᶜ
⊢ {a : X | f a ≠ g a} ∈ 𝓝 a

Tactic:
(hf.continuousAt (hU.mem_nhds ha)).prodMk_nhds (hg.continuousAt (hU.mem_nhds ha))
        (isClosed_diagonal.isOpen_compl.mem_nhds ha')

Premises used: IsClosed.isOpen_compl, Set.Mem, setOf, Set.diagonal, Set.preimage, IsOpen.mem_nhds, ContinuousOn.continuousAt, Not, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
a : X
ha : a ∈ U
ha' : (f a, g a) ∈ (diagonal Y)ᶜ
⊢ {a : X | f a ≠ g a} ∈ 𝓝 a

Tactic:
exact
      (hf.continuousAt (hU.mem_nhds ha)).prodMk_nhds (hg.continuousAt (hU.mem_nhds ha))
        (isClosed_diagonal.isOpen_compl.mem_nhds ha')

Premises used: IsClosed.isOpen_compl, IsOpen.mem_nhds, ContinuousOn.continuousAt, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsOpen[inst] (U ∩ {a : X | f a ≠ g a})

Tactic:
have : IsOpen (U ∩ { a | f a ≠ g a }) := by
    refine isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) ?_
    rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
    exact
      (hf.continuousAt (hU.mem_nhds ha)).prodMk_nhds (hg.continuousAt (hU.mem_nhds ha))
        (isClosed_diagonal.isOpen_compl.mem_nhds ha')
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IsOpen[inst] (U ∩ {a : X | f a ≠ g a})
⊢ U ∩ {a : X | f a ≠ g a} ≤ ∅

Tactic:
replace := (this.eq_empty_of_measure_zero h).le
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
this : U ∩ {a : X | f a ≠ g a} ≤ ∅
⊢ EqOn f g U

Tactic:
fun x hx => Classical.not_not.1 fun h => this ⟨hx, h⟩

Premises used: Classical.not_not, Set.EqOn, And.intro, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
this : U ∩ {a : X | f a ≠ g a} ≤ ∅
⊢ EqOn f g U

Tactic:
exact fun x hx => Classical.not_not.1 fun h => this ⟨hx, h⟩

Premises used: Classical.not_not, And.intro, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
f g : X → Y
h : f =ᶠ[ae μ] g
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
⊢ f = g

Tactic:
suffices EqOn f g univ from funext fun _ => this trivial
  eqOn_open_of_ae_eq (ae_restrict_of_ae h) isOpen_univ hf.continuousOn hg.continuousOn

Premises used: Continuous.continuousOn, trivial, MeasureTheory.ae_restrict_of_ae, isOpen_univ, funext, MeasureTheory.Measure.eqOn_open_of_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
s : Set X
f g : X → Y
h : f =ᶠ[ae (μ.restrict s)] g
hf : ContinuousOn f s
hg : ContinuousOn g s
hU : s ⊆ closure[inst] (interior s)
⊢ EqOn f g s

Tactic:
have : interior s ⊆ s := interior_subset
  (eqOn_open_of_ae_eq (ae_restrict_of_ae_restrict_of_subset this h) isOpen_interior (hf.mono this)
        (hg.mono this)).of_subset_closure
    hf hg this hU

Premises used: Set.EqOn.of_subset_closure, interior_subset, isOpen_interior, MeasureTheory.ae_restrict_of_ae_restrict_of_subset, MeasureTheory.Measure.eqOn_open_of_ae_eq, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
f g : X → Y
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
⊢ f =ᶠ[ae μ] g ↔ f = g

Tactic:
⟨fun h => eq_of_ae_eq h hf hg, fun h => h ▸ EventuallyEq.rfl⟩

Premises used: MeasureTheory.Measure.eq_of_ae_eq, Eq.rec, Iff.intro, Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : OpensMeasurableSpace X
Z : Type u_3
inst_3 : TopologicalSpace Z
inst_4 : MeasurableSpace Z
inst_5 : BorelSpace Z
f : X → Z
hf : Continuous[inst, inst_3] f
hf_surj : Surjective f
⊢ IsOpenPosMeasure (m := inst_4) (map f μ)

Tactic:
⟨fun U hUo hUne => ?_⟩

Premises used: MeasureTheory.Measure.IsOpenPosMeasure.mk
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : OpensMeasurableSpace X
Z : Type u_3
inst_3 : TopologicalSpace Z
inst_4 : MeasurableSpace Z
inst_5 : BorelSpace Z
f : X → Z
hf : Continuous[inst, inst_3] f
hf_surj : Surjective f
refine :
  ∀ (U : Set Z) (hUo : IsOpen[inst_3] U) (hUne : U.Nonempty),
    Ne (α := ℝ≥0∞) (((map f μ : Measure Z) : (a : Set Z) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsOpenPosMeasure (m := inst_4) (map f μ)

Tactic:
refine ⟨fun U hUo hUne => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : OpensMeasurableSpace X
Z : Type u_3
inst_3 : TopologicalSpace Z
inst_4 : MeasurableSpace Z
inst_5 : BorelSpace Z
f : X → Z
hf : Continuous[inst, inst_3] f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen[inst_3] U
hUne : U.Nonempty
rw : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (f ⁻¹' U) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((map f μ : Measure Z) : (a : Set Z) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.map_apply hf.measurable hUo.measurableSet]

Premises used: MeasureTheory.Measure.map_apply, IsOpen.measurableSet, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : OpensMeasurableSpace X
Z : Type u_3
inst_3 : TopologicalSpace Z
inst_4 : MeasurableSpace Z
inst_5 : BorelSpace Z
f : X → Z
hf : Continuous[inst, inst_3] f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen[inst_3] U
hUne : U.Nonempty
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (f ⁻¹' U) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)

Premises used: Iff.mpr, Function.Surjective.nonempty_preimage, IsOpen.preimage, IsOpen.measure_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : OpensMeasurableSpace X
Z : Type u_3
inst_3 : TopologicalSpace Z
inst_4 : MeasurableSpace Z
inst_5 : BorelSpace Z
f : X → Z
hf : Continuous[inst, inst_3] f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen[inst_3] U
hUne : U.Nonempty
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (f ⁻¹' U) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)

Premises used: Iff.mpr, Function.Surjective.nonempty_preimage, IsOpen.preimage, IsOpen.measure_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : BorelSpace X
Z : Type u_3
inst_2 : TopologicalSpace Z
mZ : MeasurableSpace Z
inst_3 : BorelSpace Z
μ : Measure Z
inst_4 : μ.IsOpenPosMeasure
f : X → Z
hf : IsOpenEmbedding f
U : Set X
hU : IsOpen[inst] U
Une : U.Nonempty
rw : Ne (α := ℝ≥0∞) ((μ : (a : Set Z) → ℝ≥0∞) (f '' U) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (((comap f μ : Measure X) : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [hf.measurableEmbedding.comap_apply]

Premises used: MeasurableEmbedding.comap_apply, Topology.IsOpenEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : BorelSpace X
Z : Type u_3
inst_2 : TopologicalSpace Z
mZ : MeasurableSpace Z
inst_3 : BorelSpace Z
μ : Measure Z
inst_4 : μ.IsOpenPosMeasure
f : X → Z
hf : IsOpenEmbedding f
U : Set X
hU : IsOpen[inst] U
Une : U.Nonempty
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set Z) → ℝ≥0∞) (f '' U) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
IsOpenPosMeasure.open_pos _ (hf.isOpen_iff_image_isOpen.mp hU) (Une.image f)

Premises used: MeasureTheory.Measure.IsOpenPosMeasure.open_pos, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, Set.Nonempty.image, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : BorelSpace X
Z : Type u_3
inst_2 : TopologicalSpace Z
mZ : MeasurableSpace Z
inst_3 : BorelSpace Z
μ : Measure Z
inst_4 : μ.IsOpenPosMeasure
f : X → Z
hf : IsOpenEmbedding f
U : Set X
hU : IsOpen[inst] U
Une : U.Nonempty
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set Z) → ℝ≥0∞) (f '' U) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact IsOpenPosMeasure.open_pos _ (hf.isOpen_iff_image_isOpen.mp hU) (Une.image f)

Premises used: MeasureTheory.Measure.IsOpenPosMeasure.open_pos, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, Set.Nonempty.image, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
m : MeasurableSpace X
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
inst_4 : NoMaxOrder X
a : X
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Ioi a) : ℝ≥0∞)

Tactic:
isOpen_Ioi.measure_pos μ nonempty_Ioi

Premises used: IsOpen.measure_pos, Set.nonempty_Ioi, isOpen_Ioi
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
m : MeasurableSpace X
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
inst_4 : NoMinOrder X
a : X
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Iio a) : ℝ≥0∞)

Tactic:
isOpen_Iio.measure_pos μ nonempty_Iio

Premises used: IsOpen.measure_pos, isOpen_Iio, Set.nonempty_Iio
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
m : MeasurableSpace X
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
inst_4 : DenselyOrdered X
a b : X
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞) ↔ a < b

Tactic:
(isOpen_Ioo.measure_pos_iff μ).trans nonempty_Ioo

Premises used: isOpen_Ioo, Set.nonempty_Ioo, Iff.trans, IsOpen.measure_pos_iff
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
m : MeasurableSpace X
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
inst_4 : DenselyOrdered X
a b : X
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Ioo a b) : ℝ≥0∞) (0 : ℝ≥0∞) ↔ b ≤ a

Tactic:
(isOpen_Ioo.measure_eq_zero_iff μ).trans (Ioo_eq_empty_iff.trans not_lt)

Premises used: isOpen_Ioo, not_lt, Iff.trans, Set.Ioo_eq_empty_iff, IsOpen.measure_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
m : MeasurableSpace X
inst_3 : TopologicalSpace Y
inst_4 : T2Space Y
μ : Measure X
inst_5 : μ.IsOpenPosMeasure
a b : X
f g : X → Y
hfg : f =ᶠ[ae (μ.restrict (Ioo a b))] g
hf : ContinuousOn f (Ioo a b)
hg : ContinuousOn g (Ioo a b)
⊢ EqOn f g (Ioo a b)

Tactic:
eqOn_of_ae_eq hfg hf hg Ioo_subset_closure_interior

Premises used: Ioo_subset_closure_interior, MeasureTheory.Measure.eqOn_of_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
m : MeasurableSpace X
inst_3 : TopologicalSpace Y
inst_4 : T2Space Y
μ : Measure X
inst_5 : μ.IsOpenPosMeasure
inst_6 : DenselyOrdered X
a b : X
f g : X → Y
hfg : f =ᶠ[ae (μ.restrict (Ioc a b))] g
hf : ContinuousOn f (Ioc a b)
hg : ContinuousOn g (Ioc a b)
⊢ EqOn f g (Ioc a b)

Tactic:
eqOn_of_ae_eq hfg hf hg (Ioc_subset_closure_interior _ _)

Premises used: Ioc_subset_closure_interior, MeasureTheory.Measure.eqOn_of_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
m : MeasurableSpace X
inst_3 : TopologicalSpace Y
inst_4 : T2Space Y
μ : Measure X
inst_5 : μ.IsOpenPosMeasure
inst_6 : DenselyOrdered X
a b : X
f g : X → Y
hfg : f =ᶠ[ae (μ.restrict (Ico a b))] g
hf : ContinuousOn f (Ico a b)
hg : ContinuousOn g (Ico a b)
⊢ EqOn f g (Ico a b)

Tactic:
eqOn_of_ae_eq hfg hf hg (Ico_subset_closure_interior _ _)

Premises used: MeasureTheory.Measure.eqOn_of_ae_eq, Ico_subset_closure_interior
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
m : MeasurableSpace X
inst_3 : TopologicalSpace Y
inst_4 : T2Space Y
μ : Measure X
inst_5 : μ.IsOpenPosMeasure
inst_6 : DenselyOrdered X
a b : X
hne : a ≠ b
f g : X → Y
hfg : f =ᶠ[ae (μ.restrict (Icc a b))] g
hf : ContinuousOn f (Icc a b)
hg : ContinuousOn g (Icc a b)
⊢ EqOn f g (Icc a b)

Tactic:
eqOn_of_ae_eq hfg hf hg (closure_interior_Icc hne).symm.subset

Premises used: closure_interior_Icc, Eq.subset, MeasureTheory.Measure.eqOn_of_ae_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
x : X
r : ℝ
hr : 0 < r
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (ball x r) : ℝ≥0∞)

Tactic:
isOpen_ball.measure_pos μ (nonempty_ball.2 hr)

Premises used: Iff.mpr, IsOpen.measure_pos, Metric.nonempty_ball, Metric.isOpen_ball
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
x : X
r : ℝ
hr : 0 < r
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
(measure_ball_pos μ x hr).trans_le (measure_mono ball_subset_closedBall)

Premises used: Metric.ball_subset_closedBall, LT.lt.trans_le, MeasureTheory.measure_mono, Metric.measure_ball_pos
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_2
inst : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : NoAtoms μ
x : X
r : ℝ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ↔ 0 < r

Tactic:
⟨fun h ↦ ?_, measure_closedBall_pos μ x⟩

Premises used: Metric.measure_closedBall_pos, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_2
inst : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : NoAtoms μ
x : X
r : ℝ
refine : ∀ (h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)), 0 < r
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ↔ 0 < r

Tactic:
refine ⟨fun h ↦ ?_, measure_closedBall_pos μ x⟩
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_2
inst : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : NoAtoms μ
x : X
r : ℝ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
contrapose! : ∀ (h : r ≤ 0), LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 0 < r

Tactic:
contrapose! h
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_2
inst : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
inst_2 : NoAtoms μ
x : X
r : ℝ
h : r ≤ 0
rw rw₁ : LE.le (α := ℝ≥0∞) 0 0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [(subsingleton_closedBall x h).measure_zero μ]

Premises used: Set.Subsingleton.measure_zero, Metric.subsingleton_closedBall
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
x : X
r : ℝ≥0∞
hr : r ≠ 0
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (eball x r) : ℝ≥0∞)

Tactic:
isOpen_eball.measure_pos μ ⟨x, mem_eball_self hr.bot_lt⟩

Premises used: Metric.isOpen_eball, IsOpen.measure_pos, Exists.intro, Metric.mem_eball_self, Ne.bot_lt
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
x : X
r : ℝ≥0∞
hr : r ≠ 0
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (closedEBall x r) : ℝ≥0∞)

Tactic:
(measure_eball_pos μ x hr).trans_le (measure_mono eball_subset_closedEBall)

Premises used: Metric.eball_subset_closedEBall, LT.lt.trans_le, Metric.measure_eball_pos, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
h₁s : IsClosed[inst] s
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsNowhereDense s

Tactic:
h₁s.isNowhereDense_iff.mpr (interior_eq_empty_of_null h₂s)

Premises used: Iff.mpr, MeasureTheory.Measure.interior_eq_empty_of_null, IsClosed.isNowhereDense_iff
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₁s : IsSigmaCompact s
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rcases : ∀ (K : ℕ → Set X) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hcover : ⋃ (n : ℕ), K n = s), IsMeagre s
⊢ IsMeagre s

Tactic:
rcases h₁s with ⟨K, hcompact, hcover⟩
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (K n) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : μ (K n) = 0 := measure_mono_null (hcover ▸ subset_iUnion K n) h₂s
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
n : ℕ
this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (K n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsNowhereDense (K n)

Tactic:
.of_isClosed_null (hcompact n).isClosed this

Premises used: IsNowhereDense.of_isClosed_null, IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
n : ℕ
this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (K n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsNowhereDense (K n)

Tactic:
exact .of_isClosed_null (hcompact n).isClosed this
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
⊢ ∀ (n : ℕ), IsNowhereDense (K n)

Tactic:
have h (n : ℕ) : IsNowhereDense (K n) := by
    have : μ (K n) = 0 := measure_mono_null (hcover ▸ subset_iUnion K n) h₂s
    exact .of_isClosed_null (hcompact n).isClosed this
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
rw : ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
⊢ IsMeagre s

Tactic:
rw [isMeagre_iff_countable_union_isNowhereDense]

Premises used: isMeagre_iff_countable_union_isNowhereDense
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
⟨range K, fun t ⟨n, hn⟩ ↦ hn ▸ h n, countable_range K, hcover.symm.subset⟩

Premises used: _private.0.IsMeagre.of_isSigmaCompact_null.match_1, Eq.rec, Set.countable_range, Eq.subset, And.intro, Exists.intro, Set.range, Eq.symm, IsNowhereDense
-- Module: Mathlib.MeasureTheory.Measure.OpenPos
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
s : Set X
μ : Measure X
inst_2 : μ.IsOpenPosMeasure
inst_3 : T2Space X
h₂s : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ (n : ℕ), K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
exact ⟨range K, fun t ⟨n, hn⟩ ↦ hn ▸ h n, countable_range K, hcover.symm.subset⟩