have d_lt_succ_d := Nat.lt.base d
d : ℕ
l r : ℝ
h : l < r
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)
d : ℕ
l r : ℝ
h : l < r
d_lt_succ_d : d < d.succ
⊢ DifferentiableOn ℝ (iteratedDerivWithin d Real.exp (Set.Icc l r)) (Set.Ioo l r)