analysis.calculus.uniformlimitsderiv

leanprover-community · Oct 2, 2024 · a796333 · a796333
1 parent ecc94ee
commit a796333
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
@@ -356,8 +356,8 @@ theorem hasFDerivAt_of_tendstoUniformlyOnFilter [NeBot l]
     apply ((this ε hε).filter_mono curry_le_prod).mono
     intro n hn
     rw [dist_eq_norm] at hn ⊢
-    rw [← smul_sub] at hn
-    rwa [sub_zero]
+    convert hn using 2
+    module
   · -- (Almost) the definition of the derivatives
     rw [Metric.tendsto_nhds]
     intro ε hε