-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_rnDeriv_of_absolutelyContinuous :
    ∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Tactic:
rw [v.withDensity_limRatioMeas_eq hρ] at A

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Tactic:
have A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ :=
  rnDeriv_withDensity μ (v.limRatioMeas_measurable hρ)

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : (μ.withDensity (v.limRatioMeas hρ)).rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Tactic:
filter_upwards [v.ae_tendsto_limRatioMeas hρ, A] with _ _ h'x

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
a✝¹ : α
a✝ : Tendsto (fun a => ρ a / μ a) (v.filterAt a✝¹) (𝓝 (v.limRatioMeas hρ a✝¹))
h'x : ρ.rnDeriv μ a✝¹ = v.limRatioMeas hρ a✝¹
⊢ Tendsto (fun a => ρ a / μ a) (v.filterAt a✝¹) (𝓝 (ρ.rnDeriv μ a✝¹))

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 : ρ.rnDeriv μ =ᶠ[ae μ] v.limRatioMeas hρ
a✝¹ : α
a✝ : Tendsto (fun a => ρ a / μ a) (v.filterAt a✝¹) (𝓝 (v.limRatioMeas hρ a✝¹))
h'x : ρ.rnDeriv μ a✝¹ = v.limRatioMeas hρ a✝¹
⊢ Tendsto (fun a => ρ a / μ a) (v.filterAt a✝¹) (𝓝 (ρ.rnDeriv μ a✝¹))

Tactic:
rwa [h'x]

Result:
no goals