induction n generalizing x with
| zero =>
  rw [orderedIteratedFPiDeriv_zero_eq_comp]
  rw [LinearIsometryEquiv.comp_hasFDerivAt_iff']
  refine HasFDerivAt.congr_fderiv (hf.hasFDerivAt (by simp) x) ?_
  ext m
  simp only [continuousMultilinearCurryFin1_apply, Nat.zero_eq, LinearIsometryEquiv.symm_symm,
    ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe,
    Function.comp_apply, ContinuousMultilinearMap.compContinuousLinearMapL_apply,
    continuousMultilinearIsEmptyEquiv_apply,
    ContinuousMultilinearMap.compContinuousLinearMap_apply, Pi.zero_apply, map_zero,
    ContinuousMultilinearMap.curryLeft_apply]
  congr
  funext i
  rw [Fin.eq_zero i]
  simp only [Fin.cons_zero]
  have : (0 : Fin 1) = Fin.last 0 := rfl
  simp [this]
| succ n ih =>
  rw [← hasFTaylorSeriesUpToOn_univ_iff] at hf
  rw [hasFTaylorSeriesUpToOn_succ_iff_left] at hf
  rcases hf with ⟨hf_pred, hf_diff, _⟩
  rw [hasFTaylorSeriesUpToOn_univ_iff] at hf_pred
  simp at hf_diff
  specialize @ih hf_pred
  rw [orderedIteratedFPiDeriv_succ_eq_comp_left]
  conv =>
    arg 1; intro y; arg 2; intro x
    rw [fpideriv_eq_fderiv_comp_single ih.differentiableAt]
    rw [ih.fderiv]
    rw [ContinuousLinearMap.comp_assoc]
    simp [Fin.tail]
    rw [← ContinuousMultilinearMap.curryLeft_compContinuousLinearMap (f' x (n + 1)) (fun i => ContinuousLinearMap.single (js i))]
  simp
  simp_rw [← ContinuousMultilinearMap.compContinuousLinearMapL_apply]
  refine ((ContinuousLinearMap.hasFDerivAt _).comp _ (hf_diff _)).congr_fderiv ?_
  ext m v
  simp
ι : 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
n : ℕ
hf : HasFTaylorSeriesUpTo (↑n + 1) f f'
js : Fin n → ι
x : (i : ι) → M i
⊢ HasFDerivAt (orderedIteratedFPiDeriv 𝕜 js f)
    (ContinuousLinearMap.comp
      (ContinuousMultilinearMap.compContinuousLinearMapL fun i => ContinuousLinearMap.single (js i))
      (ContinuousMultilinearMap.curryLeft (f' x (n + 1))))
    x
no goals