-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_eventually_measure_zero_of_singular (hρ : ρ ⟂ₘ μ) :
    ∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 0)

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
a : Set α
ha : ρ a < ↑(u n) * μ a
μa_pos : 0 < μ a
μa_lt_top : μ a < ⊤
⊢ ρ a / μ a < z

Tactic:
rw [ENNReal.div_lt_iff (Or.inl μa_pos.ne') (Or.inl μa_lt_top.ne)]

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
n : ℕ
hn : u n < w
a : Set α
ha : ρ a < ↑(u n) * μ a
μa_pos : 0 < μ a
μa_lt_top : μ a < ⊤
⊢ ρ a < z * μ a

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ (↑ε)⁻¹ * ρ (s ∩ o) ≤ (↑ε)⁻¹ * ρ o

Tactic:
gcongr

Result:
case bc.h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ s ∩ o ⊆ o

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 0)

Tactic:
obtain ⟨u, _, u_pos, u_lim⟩ :
  ∃ u : ℕ → ℝ≥0, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
  exists_seq_strictAnti_tendsto (0 : ℝ≥0)

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ρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 0)

Proof state:
case bc
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ (ε • μ) (s ∩ o) ≤ ρ (s ∩ o)

Tactic:
refine v.measure_le_of_frequently_le ρ smul_absolutelyContinuous _ ?_

Result:
case bc
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ ∀ x ∈ s ∩ o, ∃ᶠ (a : Set α) in v.filterAt x, (↑ENNReal.ofNNRealHom.toMonoidWithZeroHom ε • μ) a ≤ ρ a

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ μ (s ∩ o) = ↑ε * (↑ε)⁻¹ * μ (s ∩ o)

Tactic:
rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]

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ρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 0)

Tactic:
have B : ∀ᵐ x ∂μ, ∀ n, ∀ᶠ a in v.filterAt x, ρ a < u n * μ a :=
  ae_all_iff.2 fun n => A (u n) (u_pos n)

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ρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 0)