cases n with
| zero => simp
| succ n =>
  simp [iteratedFDeriv_succ_eq_comp_right]
  simp_rw [fderiv_innerSL_apply]
  cases n with
  | zero =>
    simp
    refine le_trans (norm_innerSL_le_one ℝ) (by simp)
  | succ n =>
    rw [iteratedFDeriv_const_of_ne]
    . change ‖0‖ ≤ _
      simp
    . simp
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 + ‖x‖
no goals