diff --git a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean
index d9cf55a6de35e9..e000659ce34903 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean
@@ -34,8 +34,8 @@ theorem withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [Sigm
     rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub,
       setIntegral_toReal_rnDeriv h.1 i, setIntegral_toReal_rnDeriv h.2 i]
     · conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]
-      erw [VectorMeasure.sub_apply]
-      rw [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
+      rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply,
+        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
         measureReal_def]
     all_goals
       refine Integrable.integrableOn ?_