simp
case succ.zero
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
x : E
⊢ ‖iteratedFDeriv ℝ Nat.zero (fun y => ContinuousLinearMap.id ℝ E) x‖ ≤ 1 + ‖x‖
case succ.zero
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
x : E
⊢ ‖ContinuousLinearMap.id ℝ E‖ ≤ 1 + ‖x‖