-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
/-- In a space with an inner regular measure for finite measure sets, the everywhere positive subset
of a measurable set of finite measure is itself everywhere positive. This is not obvious as
`μ.everywherePosSubset s` is defined as the points whose neighborhoods intersect `s` along positive
measure subsets, but this does not say they also intersect `μ.everywherePosSubset s` along positive
measure subsets. -/
lemma isEverywherePos_everywherePosSubset_of_measure_ne_top
    [OpensMeasurableSpace α] [InnerRegularCompactLTTop μ] (hs : MeasurableSet s) (h's : μ s ≠ ∞) :
    μ.IsEverywherePos (μ.everywherePosSubset s)

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
⊢ 0 < μ n

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

Result:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ 0 < μ n

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ 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

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ s)
⊢ 0 < μ n

Tactic:
have B : (u ∩ μ.everywherePosSubset s : Set α) =ᵐ[μ] (u ∩ s : Set α) :=
  ae_eq_set_inter (ae_eq_refl _) (everywherePosSubset_ae_eq_of_measure_ne_top hs h's)

Result:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ s)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ 0 < μ n

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
⊢ μ.IsEverywherePos (μ.everywherePosSubset s)

Tactic:
intro x hx n hn

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
⊢ 0 < μ n

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
this : u ∩ s ∈ 𝓝[s] x
⊢ 0 < μ (u ∩ s)

Tactic:
exact hx.2 _ this

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ 0 < μ (u ∩ s)

Tactic:
have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
this : u ∩ s ∈ 𝓝[s] x
⊢ 0 < μ (u ∩ s)

Proof state:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ μ.everywherePosSubset s)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ 0 < μ n

Tactic:
exact A.trans_le (measure_mono hu)

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ u ∩ s ∈ 𝓝[s] x

Tactic:
rw [inter_comm]

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ 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

Proof state:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ s)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ 0 < μ n

Tactic:
rw [← B.measure_eq] at A

Result:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ μ.everywherePosSubset s)
B : u ∩ μ.everywherePosSubset s =ᶠ[ae μ] u ∩ s
⊢ 0 < μ n

Proof state:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
⊢ 0 < μ n

Tactic:
have A : 0 < μ (u ∩ s) := by
  have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
  exact hx.2 _ this

Result:
case intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ⊤
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ s)
⊢ 0 < μ n