awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
this :
  ∀ (n : Set α) (ns : n ∈ 𝓝[s] x) (hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)),
    {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
⊢ Membership.mem (γ := Set α) {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} x →
    {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x

Tactic:
⟨n, ns, hx⟩
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
rcases :
  ∀ (v : Set α) (vx : v ∈ 𝓝 x) (hv : v ∩ s ⊆ n),
    {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
⊢ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 ns with ⟨v, vx, hv⟩

Premises used: Iff.mp, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
rcases :
  ∀ (w : Set α) (wv : w ⊆ v) (w_open : IsOpen[inst] w) (xw : x ∈ w),
    {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x
⊢ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x

Tactic:
rcases mem_nhds_iff.1 vx with ⟨w, wv, w_open, xw⟩

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ Membership.mem (γ := Set α) {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} y

Tactic:
⟨s ∩ w, inter_mem_nhdsWithin _ (w_open.mem_nhds yw), measure_mono_null ?_ hx⟩

Premises used: inter_mem_nhdsWithin, Set.Mem, setOf, MeasureTheory.measure_mono_null, Inter.inter, And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
y : α
yw : y ∈ w
refine : s ∩ w ⊆ n
⊢ Membership.mem (γ := Set α) {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} y

Tactic:
refine ⟨s ∩ w, inter_mem_nhdsWithin _ (w_open.mem_nhds yw), measure_mono_null ?_ hx⟩
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
y : α
yw : y ∈ w
rw : w ∩ s ⊆ n
⊢ s ∩ w ⊆ n

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ w ∩ s ⊆ n

Tactic:
(inter_subset_inter_left _ wv).trans hv

Premises used: HasSubset.Subset.trans, Set.inter_subset_inter_left
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ w ∩ s ⊆ n

Tactic:
exact (inter_subset_inter_left _ wv).trans hv

Premises used: HasSubset.Subset.trans, Set.inter_subset_inter_left
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
⊢ w ⊆ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}

Tactic:
have A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} := by
    intro y yw
    refine ⟨s ∩ w, inter_mem_nhdsWithin _ (w_open.mem_nhds yw), measure_mono_null ?_ hx⟩
    rw [inter_comm]
    exact (inter_subset_inter_left _ wv).trans hv
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
A : w ⊆ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
⊢ w ∈ 𝓝 x

Tactic:
have B : w ∈ 𝓝 x := w_open.mem_nhds xw
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
A : w ⊆ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
B : w ∈ 𝓝 x
⊢ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x

Tactic:
mem_of_superset B A

Premises used: Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst] w
xw : x ∈ w
A : w ⊆ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)}
B : w ∈ 𝓝 x
⊢ {x : α | ∃ n ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞) (0 : ℝ≥0∞)} ∈ 𝓝 x

Tactic:
exact mem_of_superset B A

Premises used: Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
hs : MeasurableSet s
rcases :
  ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : μ.everywherePosSubset s = s \ u),
    MeasurableSet (μ.everywherePosSubset s)
⊢ MeasurableSet (μ.everywherePosSubset s)

Tactic:
rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩

Premises used: MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
rw : MeasurableSet (s \ u)
⊢ MeasurableSet (μ.everywherePosSubset s)

Tactic:
rw [hu]
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
⊢ MeasurableSet (s \ u)

Tactic:
hs.diff u_open.measurableSet

Premises used: MeasurableSet.diff, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
⊢ MeasurableSet (s \ u)

Tactic:
exact hs.diff u_open.measurableSet

Premises used: MeasurableSet.diff, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed[inst] s
rcases :
  ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : μ.everywherePosSubset s = s \ u),
    IsClosed[inst] (μ.everywherePosSubset s)
⊢ IsClosed[inst] (μ.everywherePosSubset s)

Tactic:
rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩

Premises used: MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed[inst] s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
rw : IsClosed[inst] (s \ u)
⊢ IsClosed[inst] (μ.everywherePosSubset s)

Tactic:
rw [hu]
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed[inst] s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsClosed[inst] (s \ u)

Tactic:
hs.sdiff u_open

Premises used: IsClosed.sdiff
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed[inst] s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsClosed[inst] (s \ u)

Tactic:
exact hs.sdiff u_open

Premises used: IsClosed.sdiff
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
rcases :
  ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : μ.everywherePosSubset s = s \ u), IsCompact (μ.everywherePosSubset s)
⊢ IsCompact (μ.everywherePosSubset s)

Tactic:
rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩

Premises used: MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
rw : IsCompact (s \ u)
⊢ IsCompact (μ.everywherePosSubset s)

Tactic:
rw [hu]
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsCompact (s \ u)

Tactic:
hs.diff u_open

Premises used: IsCompact.diff
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen[inst] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsCompact (s \ u)

Tactic:
exact hs.diff u_open

Premises used: IsCompact.diff
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
he : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
hmono :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hunion :
  ∀ ⦃s t : Set α⦄,
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞)
hnhds : ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply hk.induction_on (p := fun t ↦ μ t = 0)

Premises used: IsCompact.induction_on
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_empty

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_empty

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ ∀ ⦃s t : Set α⦄,
    s ⊆ t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun s t hst ht ↦ measure_mono_null hst ht

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ ∀ ⦃s t : Set α⦄,
    s ⊆ t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact fun s t hst ht ↦ measure_mono_null hst ht

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ ∀ ⦃s t : Set α⦄,
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun s t hs ht ↦ measure_union_null hs ht

Premises used: MeasureTheory.measure_union_null
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ ∀ ⦃s t : Set α⦄,
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact fun s t hs ht ↦ measure_union_null hs ht

Premises used: MeasureTheory.measure_union_null
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
x : α
hx : x ∈ k
⊢ ∃ u ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [everywherePosSubset, (h'k hx).1] using (h'k hx).2

Premises used: And.right, And.left, MeasureTheory.Measure.everywherePosSubset
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
x : α
hx : x ∈ k
hnhds :
  ∀ (u : Set α) (ux : u ∈ 𝓝[s] x) (hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ t ∈ 𝓝[k] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ t ∈ 𝓝[k] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨u, ux, hu⟩ : ∃ u ∈ 𝓝[s] x, μ u = 0 := by
      simpa [everywherePosSubset, (h'k hx).1] using (h'k hx).2
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
x : α
hx : x ∈ k
u : Set α
ux : u ∈ 𝓝[s] x
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ t ∈ 𝓝[k] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨u, nhdsWithin_mono x (h'k.trans diff_subset) ux, hu⟩

Premises used: Set.diff_subset, HasSubset.Subset.trans, And.intro, Exists.intro, nhdsWithin_mono
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
x : α
hx : x ∈ k
u : Set α
ux : u ∈ 𝓝[s] x
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ t ∈ 𝓝[k] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ⟨u, nhdsWithin_mono x (h'k.trans diff_subset) ux, hu⟩
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
simp :
  ∀ (i : Set α) (i_1 : i ⊆ s \ μ.everywherePosSubset s) (i_2 : IsCompact i),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.everywherePosSubset s =ᶠ[ae μ] s

Tactic:
simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty,
    true_and, (hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact, ENNReal.iSup_eq_zero]

Premises used: Iff.mpr, MeasurableSet.diff, MeasurableSet.everywherePosSubset, MeasureTheory.ae_eq_set, MeasurableSet.measure_eq_iSup_isCompact, MeasureTheory.measure_empty, ENNReal.iSup_eq_zero, MeasureTheory.Measure.everywherePosSubset_subset, Set.diff_eq_empty, true_and
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_eq_zero_of_subset_diff_everywherePosSubset h'k hk

Premises used: MeasureTheory.Measure.measure_eq_zero_of_subset_diff_everywherePosSubset
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_eq_zero_of_subset_diff_everywherePosSubset h'k hk

Premises used: MeasureTheory.Measure.measure_eq_zero_of_subset_diff_everywherePosSubset
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ μ.everywherePosSubset s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have A : μ (s \ μ.everywherePosSubset s) ≠ ∞ :=
    ((measure_mono diff_subset).trans_lt h's.lt_top).ne
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ μ.everywherePosSubset s) : ℝ≥0∞) (∞ : ℝ≥0∞)
simp :
  ∀ (i : Set α) (i_1 : i ⊆ s \ μ.everywherePosSubset s) (i_2 : IsCompact i),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.everywherePosSubset s =ᶠ[ae μ] s

Tactic:
simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty,
    true_and, (hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact_of_ne_top A,
    ENNReal.iSup_eq_zero]

Premises used: Iff.mpr, MeasurableSet.diff, MeasurableSet.everywherePosSubset, MeasurableSet.measure_eq_iSup_isCompact_of_ne_top, MeasureTheory.ae_eq_set, MeasureTheory.measure_empty, ENNReal.iSup_eq_zero, MeasureTheory.Measure.everywherePosSubset_subset, Set.diff_eq_empty, true_and
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ μ.everywherePosSubset s) : ℝ≥0∞) (∞ : ℝ≥0∞)
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_eq_zero_of_subset_diff_everywherePosSubset h'k hk

Premises used: MeasureTheory.Measure.measure_eq_zero_of_subset_diff_everywherePosSubset
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ μ.everywherePosSubset s) : ℝ≥0∞) (∞ : ℝ≥0∞)
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) k : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_eq_zero_of_subset_diff_everywherePosSubset h'k hk

Premises used: MeasureTheory.Measure.measure_eq_zero_of_subset_diff_everywherePosSubset
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
rcases :
  ∀ (u : Set α) (u_mem : u ∈ 𝓝 x) (hu : u ∩ μ.everywherePosSubset s ⊆ n),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) n : ℝ≥0∞)

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 hn with ⟨u, u_mem, hu⟩

Premises used: Iff.mp, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
rw : s ∩ u ∈ 𝓝[s] x
⊢ u ∩ s ∈ 𝓝[s] x

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ s ∩ u ∈ 𝓝[s] x

Tactic:
inter_mem_nhdsWithin s u_mem

Premises used: inter_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.EverywherePos
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
inst_2 : OpensMeasurableSpace α
inst_3 : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ s ∩ u ∈ 𝓝[s] x

Tactic:
exact inter_mem_nhdsWithin s u_mem

Premises used: inter_mem_nhdsWithin