-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem measure_limRatioMeas_zero : ρ {x | v.limRatioMeas hρ x = 0} = 0

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
this : v.limRatioMeas hρ y = 0
⊢ y ∈ {x | v.limRatioMeas hρ x < ↑q}

Tactic:
simp only [this, mem_setOf_eq, hq, ENNReal.coe_pos]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
⊢ Tendsto ENNReal.ofNNReal (𝓝[>] 0) (𝓝 ↑0)

Tactic:
rw [ENNReal.tendsto_coe]

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
⊢ Tendsto (fun a => a) (𝓝[>] 0) (𝓝 0)

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
⊢ Tendsto (fun a => a) (𝓝[>] 0) (𝓝 0)

Tactic:
exact nhdsWithin_le_nhds

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
B : Tendsto (fun q => ↑q * μ s) (𝓝[>] 0) (𝓝 (↑0 * μ s))
⊢ ρ s ≤ 0

Tactic:
simp only [zero_mul, ENNReal.coe_zero] at B

Result:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
B : Tendsto (fun q => ↑q * μ s) (𝓝[>] 0) (𝓝 0)
⊢ ρ s ≤ 0

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
⊢ ρ s ≤ 0

Tactic:
have μs : μ s ≠ ∞ := ((measure_mono inter_subset_right).trans_lt μo).ne

Result:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
⊢ ρ s ≤ 0

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
B : Tendsto (fun q => ↑q * μ s) (𝓝[>] 0) (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0, ρ s ≤ ↑c * μ s

Tactic:
filter_upwards [self_mem_nhdsWithin] using A

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
B : Tendsto (fun q => ↑q * μ s) (𝓝[>] 0) (𝓝 0)
⊢ ρ s ≤ 0

Tactic:
apply ge_of_tendsto B

Result:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
B : Tendsto (fun q => ↑q * μ s) (𝓝[>] 0) (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0, ρ s ≤ ↑c * μ s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
⊢ ∃ u ∈ 𝓝[{x | v.limRatioMeas hρ x = 0}] x, ρ u = 0

Tactic:
refine ⟨s, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), le_antisymm ?_ bot_le⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
⊢ ρ s ≤ 0

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ρ {x | v.limRatioMeas hρ x = 0} = 0

Tactic:
refine measure_null_of_locally_null _ fun x _ => ?_

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
⊢ ∃ u ∈ 𝓝[{x | v.limRatioMeas hρ x = 0}] x, ρ u = 0