no goals
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type uG
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
X : Type ?u.2834577
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
f : E → F
⊢ ContDiff 𝕜 (↑(n + 1)) f ↔ Differentiable 𝕜 f ∧ ∀ (y : E), ContDiff 𝕜 ↑n fun x => ↑(fderiv 𝕜 f x) y
rw [contDiff_succ_iff_fderiv, contDiff_clm_apply_iff]