-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem measure_limRatioMeas_top : μ {x | v.limRatioMeas hρ x = ∞} = 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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
y : α
hy : y ∈ s
⊢ y ∈ {x | ↑q < v.limRatioMeas hρ x}

Tactic:
have : v.limRatioMeas hρ y = ∞ := hy.1

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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
y : α
hy : y ∈ s
this : v.limRatioMeas hρ y = ⊤
⊢ y ∈ {x | ↑q < v.limRatioMeas hρ x}

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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
q : ℝ≥0
hq : 1 ≤ q
⊢ ↑q ≠ 0 ∨ ρ s ≠ 0

Tactic:
simp only [(zero_lt_one.trans_le hq).ne', true_or, ENNReal.coe_eq_zero, Ne,
  not_false_iff]

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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
⊢ ∃ u ∈ 𝓝[{x | v.limRatioMeas hρ x = ⊤}] x, μ u = 0

Tactic:
let s := {x : α | v.limRatioMeas hρ x = ∞} ∩ o

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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
⊢ ∃ u ∈ 𝓝[{x | v.limRatioMeas hρ x = ⊤}] x, μ u = 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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
⊢ Tendsto (fun x => (↑x)⁻¹) atTop (𝓝 ⊤⁻¹)

Tactic:
exact ENNReal.tendsto_inv_iff.2 (ENNReal.tendsto_coe_nhds_top.2 tendsto_id)

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 = ⊤}
⊢ ∃ u ∈ 𝓝[{x | v.limRatioMeas hρ x = ⊤}] x, μ u = 0

Tactic:
obtain ⟨o, xo, o_open, μo⟩ : ∃ o : Set α, x ∈ o ∧ IsOpen o ∧ ρ o < ∞ :=
  Measure.exists_isOpen_measure_lt_top ρ x

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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
⊢ ∃ u ∈ 𝓝[{x | v.limRatioMeas hρ x = ⊤}] x, μ u = 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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
⊢ Tendsto (fun q => (↑q)⁻¹ * ρ s) atTop (𝓝 (⊤⁻¹ * ρ s))

Tactic:
apply ENNReal.Tendsto.mul_const _ (Or.inr ρs)

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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
⊢ Tendsto (fun x => (↑x)⁻¹) atTop (𝓝 ⊤⁻¹)

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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ρ s) atTop (𝓝 0)
⊢ ∀ᶠ (c : ℝ≥0) in atTop, μ s ≤ (↑c)⁻¹ * ρ s

Tactic:
exact eventually_atTop.2 ⟨1, 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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
⊢ μ s ≤ 0

Tactic:
have B : Tendsto (fun q : ℝ≥0 => (q : ℝ≥0∞)⁻¹ * ρ s) atTop (𝓝 (∞⁻¹ * ρ s)) := by
  apply ENNReal.Tendsto.mul_const _ (Or.inr ρs)
  exact ENNReal.tendsto_inv_iff.2 (ENNReal.tendsto_coe_nhds_top.2 tendsto_id)

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 = ⊤}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : ρ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = ⊤} ∩ o
ρs : ρ s ≠ ⊤
A : ∀ (q : ℝ≥0), 1 ≤ q → μ s ≤ (↑q)⁻¹ * ρ s
B : Tendsto (fun q => (↑q)⁻¹ * ρ s) atTop (𝓝 (⊤⁻¹ * ρ s))
⊢ μ s ≤ 0