have h1 : ContDiffOn ℝ n (derivWithin f (Icc a b)) (Icc a b) :=
  h.derivWithin (uniqueDiffOn_Icc hab) le_rfl
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)