shake more

sgouezel · sgouezel · commit d9ab6ee37868 · 2024-02-07T17:25:02.000+01:00
diff --git a/Mathlib/Analysis/Calculus/SmoothSeries.lean b/Mathlib/Analysis/Calculus/SmoothSeries.lean
@@ -5,7 +5,6 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.UniformLimitsDeriv
-import Mathlib.Data.Nat.Cast.WithTop
 import Mathlib.Topology.Algebra.InfiniteSum.Module
 import Mathlib.Analysis.NormedSpace.FunctionSeries
 
@@ -243,7 +242,7 @@ theorem contDiff_tsum (hf : ∀ i, ContDiff 𝕜 N (f i)) (hv : ∀ k : ℕ, (k
       exact h'f _ _ _ hm
   · intro m hm
     have h'm : ((m + 1 : ℕ) : ℕ∞) ≤ N := by
-      simpa only [ENat.coe_add, Nat.cast_withBot, ENat.coe_one] using ENat.add_one_le_of_lt hm
+      simpa only [ENat.coe_add, ENat.coe_one] using ENat.add_one_le_of_lt hm
     rw [iteratedFDeriv_tsum hf hv h'f hm.le]
     have A :
       ∀ n x, HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x :=
