cases n with
| zero => simp
| succ n =>
  rw [iteratedFDeriv_succ_eq_comp_right]
  simp
  cases n with
  | zero => simp; refine le_trans ContinuousLinearMap.norm_id_le (by simp)
  | succ n => simp [iteratedFDeriv_const_of_ne]
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n id x‖ ≤ 1 + ‖x‖
no goals