Fix

leanprover-community · Jan 3, 2025 · c812665 · c812665
1 parent 7be0b06
commit c812665
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
@@ -196,7 +196,7 @@ theorem HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum
   apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
   · exact h.mono inter_subset_left
   · exact h'.mono inter_subset_left
-  · exact hs.inter EMetric.isOpen_ball
+  · exact hs.inter_isOpen EMetric.isOpen_ball
   · exact ⟨hx, EMetric.mem_ball_self h.r_pos⟩
   · exact inter_subset_right
 

diff --git a/Mathlib/Analysis/Calculus/Taylor.lean b/Mathlib/Analysis/Calculus/Taylor.lean
@@ -305,8 +305,7 @@ theorem taylor_mean_remainder_bound {f : ℝ → E} {a b C x : ℝ} {n : ℕ} (h
     simp [hx]
   -- The nth iterated derivative is differentiable
   have hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b) :=
-    hf.differentiableOn_iteratedDerivWithin (mod_cast n.lt_succ_self)
-      (uniqueDiffOn_Icc h)
+    hf.differentiableOn_iteratedDerivWithin (mod_cast n.lt_succ_self) (.Icc h)
   -- We can uniformly bound the derivative of the Taylor polynomial
   have h' : ∀ y ∈ Ico a x,
       ‖((n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤
@@ -350,4 +349,4 @@ theorem exists_taylor_mean_remainder_bound {f : ℝ → E} {a b : ℝ} {n : ℕ}
   intro x hx
   rw [div_mul_eq_mul_div₀]
   refine taylor_mean_remainder_bound hab hf hx fun y => ?_
-  exact (hf.continuousOn_iteratedDerivWithin rfl.le <| uniqueDiffOn_Icc h).norm.le_sSup_image_Icc
+  exact (hf.continuousOn_iteratedDerivWithin le_rfl <| .Icc h).norm.le_sSup_image_Icc