case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3482095
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ (a : α),
    Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 (limRatio v ρ a)) →
      limRatio v ρ a = AEMeasurable.mk (limRatio v ρ) (_ : AEMeasurable (limRatio v ρ)) a →
        Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 (limRatioMeas v hρ a))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3482095
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))
filter_upwards [v.ae_tendsto_limRatio hρ, AEMeasurable.ae_eq_mk (v.aemeasurable_limRatio hρ)]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3482095
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
h'x : limRatio v ρ x = AEMeasurable.mk (limRatio v ρ) (_ : AEMeasurable (limRatio v ρ)) x
⊢ Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3482095
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ (a : α),
    Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 (limRatio v ρ a)) →
      limRatio v ρ a = AEMeasurable.mk (limRatio v ρ) (_ : AEMeasurable (limRatio v ρ)) a →
        Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 (limRatioMeas v hρ a))
intro x hx h'x
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.3482095
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
h'x : limRatio v ρ x = AEMeasurable.mk (limRatio v ρ) (_ : AEMeasurable (limRatio v ρ)) x
⊢ Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatioMeas v hρ x))
rwa [h'x] at hx