case zero =>
simp only [CharP.cast_eq_zero, contDiff_zero, contDiffOn_zero] at h ⊢
refine ⟨IccExtend hab.le (restrict (Icc a b) f), h.restrict.Icc_extend', ?_⟩
exact λ t ht => IccExtend_of_mem _ _ ht
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContDiffOn ℝ (↑Nat.zero) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑Nat.zero) g ∧ EqOn g f (Icc a b)
no goals