-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem CPolynomialOn.iteratedFDeriv (h : CPolynomialOn 𝕜 f s) (n : ℕ) :
    CPolynomialOn 𝕜 (iteratedFDeriv 𝕜 n f) s

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ CPolynomialOn 𝕜
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ _root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f)) s

Tactic:
convert ContinuousLinearMap.comp_cPolynomialOn ?g IH.fderiv

Result:
case h.e.h.e'_9.h.e'_4
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm = ⇑?g

case g
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s

Tactic:
exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F).comp_cPolynomialOn h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
⊢ CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s

Tactic:
induction n with
| zero =>
  rw [iteratedFDeriv_zero_eq_comp]
  exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F).comp_cPolynomialOn h
| succ n IH =>
  rw [iteratedFDeriv_succ_eq_comp_left]
  convert ContinuousLinearMap.comp_cPolynomialOn ?g IH.fderiv
  case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm
  simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F

Tactic:
exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 0 f) s

Tactic:
rw [iteratedFDeriv_zero_eq_comp]

Result:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s

Proof state:
case h.e.h.e'_9.h.e'_4
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm =
    ⇑↑{ toLinearEquiv := (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm.toLinearEquiv,
          continuous_toFun := ⋯, continuous_invFun := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
case h.e.h.e'_9.h.e'_4
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm = ⇑?g

case g
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F

Tactic:
case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm

Result:
case h.e.h.e'_9.h.e'_4
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm =
    ⇑↑{ toLinearEquiv := (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm.toLinearEquiv,
          continuous_toFun := ⋯, continuous_invFun := ⋯ }

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 (n + 1) f) s

Tactic:
rw [iteratedFDeriv_succ_eq_comp_left]

Result:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ CPolynomialOn 𝕜
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ _root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f)) s