induction n generalizing m with
| zero =>
  rw [orderedIteratedFPiDeriv_zero_eq_comp]
  simp at hn
  exact (LinearIsometryEquiv.contDiff _).comp (hf.of_le hn)
| succ n ih =>
  rw [orderedIteratedFPiDeriv_succ_eq_comp_left]
  refine ContDiff.comp ?_ ?_
  . exact LinearIsometryEquiv.contDiff _  have hn' : n < N  . simp at hn
    rw [← add_assoc] at hn
    refine lt_of_lt_of_le ?_ hn
    rw [← ENat.add_one_le_iff (ENat.coe_ne_top n)]
    rw [add_assoc]
    exact le_add_self
  conv =>
    arg 3; intro x
    rw [fpideriv_eq_fderiv_comp_single (hf.differentiable_orderedIteratedFPiDeriv hn' _)]
  refine ContDiff.clm_comp ?_ contDiff_const
  specialize @ih (m + 1) ?_
  . rw [add_assoc]
    rw [add_comm 1]
    exact hn
  exact ContDiff.fderiv_right ih (le_refl _)
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
m N : ℕ∞
n : ℕ
hn : m + ↑n ≤ N
hf : ContDiff 𝕜 N f
js : Fin n → ι
⊢ ContDiff 𝕜 m (orderedIteratedFPiDeriv 𝕜 js f)
no goals