-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
/-- The everywhere positive subset of a set is obtained by removing an open set. -/
lemma exists_isOpen_everywherePosSubset_eq_diff (μ : Measure α) (s : Set α) :
    ∃ u, IsOpen u ∧ μ.everywherePosSubset s = s \ u

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ s ∩ w ⊆ n

Tactic:
rw [inter_comm]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ w ∩ s ⊆ n

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ IsOpen {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Tactic:
rw [isOpen_iff_mem_nhds]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∀ x ∈ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}, {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

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

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∃ u, IsOpen u ∧ μ.everywherePosSubset s = s \ u

Tactic:
refine ⟨{x | ∃ n ∈ 𝓝[s] x, μ n = 0}, ?_, by ext x; simp [everywherePosSubset, zero_lt_iff]⟩

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ IsOpen {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∀ x ∈ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}, {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Tactic:
intro x ⟨n, ns, hx⟩

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.everywherePosSubset s = s \ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
⊢ x ∈ μ.everywherePosSubset s ↔ x ∈ s \ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

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

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Tactic:
have B : w ∈ 𝓝 x := w_open.mem_nhds xw

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}
B : w ∈ 𝓝 x
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ y ∈ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

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

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ s ∩ w ⊆ n

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
⊢ w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Tactic:
intro y yw

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ y ∈ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}
B : w ∈ 𝓝 x
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Tactic:
exact mem_of_superset B A

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ w ∩ s ⊆ n

Tactic:
exact (inter_subset_inter_left _ wv).trans hv

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

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

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Proof state:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
⊢ x ∈ μ.everywherePosSubset s ↔ x ∈ s \ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Tactic:
simp [everywherePosSubset, zero_lt_iff]

Result:
no goals