awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n r
inl :
  ∀ (h : HasFiniteFPowerSeriesOnBall f p x 0 r),
    HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (HSub.hSub (α := ℕ) 0 1) r
inr : ∀ (hn : n ≠ 0), HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (n - 1) r
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (n - 1) r

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x 0 r

Tactic:
HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (fun y hy ↦ ?_) h.r_pos fun n ↦ ?_

Premises used: HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero, HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
inl : ∀ (y : E) (hy : y ∈ Metric.eball x r), Eq (α := E →L[𝕜] F) (fderiv 𝕜 f y) 0
inl₁ : ∀ (n : ℕ), p.derivSeries n = 0
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x 0 r

Tactic:
refine HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (fun y hy ↦ ?_) h.r_pos fun n ↦ ?_

Premises used: HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero, HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
y : E
hy : y ∈ Metric.eball x r
inl : Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ 0) y) 0
inl₁ : f =ᶠ[𝓝 y] fun (x : E) ↦ 0
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f y) 0

Tactic:
rw [Filter.EventuallyEq.fderiv_eq (f := fun _ ↦ 0)]

Premises used: Filter.EventuallyEq.fderiv_eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ 0) y) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
y : E
hy : y ∈ Metric.eball x r
z : E
hz : z ∈ Metric.eball x r
rw rw₁ : Eq.{v + 1} (α := F) 0 ((fun (x : E) ↦ (0 : F)) z)
⊢ f z = (fun (x : E) ↦ (0 : F)) z

Tactic:
rw [h.eq_zero_of_bound_zero z hz]

Premises used: HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ f =ᶠ[𝓝 y] fun (x : E) ↦ 0

Tactic:
exact Filter.eventuallyEq_iff_exists_mem.mpr ⟨Metric.eball x r,
          Metric.isOpen_eball.mem_nhds hy, fun z hz ↦ by rw [h.eq_zero_of_bound_zero z hz]⟩

Premises used: Metric.isOpen_eball, Iff.mpr, Metric.eball, And.intro, IsOpen.mem_nhds, Exists.intro, Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
inl :
  ∀ (x : (i : Fin n) → E),
    Eq (α := E →L[𝕜] F) ((p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) x : E →L[𝕜] F)
      ((0 : (a : (i : Fin n) → E) → E →L[𝕜] F) x : E →L[𝕜] F)
⊢ p.derivSeries n = 0

Tactic:
apply ContinuousMultilinearMap.ext

Premises used: ContinuousMultilinearMap.ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
a : (i : Fin n) → E
inl :
  Eq (α := E →L[𝕜] F)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        ((p.changeOriginSeries 1 n : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) a) :
      E →L[𝕜] F)
    (0 : E →L[𝕜] F)
⊢ Eq (α := E →L[𝕜] F) ((p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) a : E →L[𝕜] F)
    ((0 : (a : (i : Fin n) → E) → E →L[𝕜] F) a : E →L[𝕜] F)

Tactic:
change (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOriginSeries 1 n a) = 0

Premises used: FormalMultilinearSeries.changeOriginSeries, continuousMultilinearCurryFin1, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
a : (i : Fin n) → E
inl :
  Eq (α := E →L[𝕜] F)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        ((0 : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) a) :
      E →L[𝕜] F)
    (0 : E →L[𝕜] F)
⊢ Eq (α := E →L[𝕜] F)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        ((p.changeOriginSeries 1 n : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) a) :
      E →L[𝕜] F)
    (0 : E →L[𝕜] F)

Tactic:
rw [p.changeOriginSeries_finite_of_finite h.finite 1 (Nat.zero_le _)]

Premises used: Nat.zero_le, HasFiniteFPowerSeriesOnBall.finite, FormalMultilinearSeries.changeOriginSeries_finite_of_finite, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
a : (i : Fin n) → E
⊢ Eq (α := E →L[𝕜] F)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        ((0 : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) a) :
      E →L[𝕜] F)
    (0 : E →L[𝕜] F)

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
a : (i : Fin n) → E
⊢ Eq (α := E →L[𝕜] F)
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
        ((0 : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) a) :
      E →L[𝕜] F)
    (0 : E →L[𝕜] F)

Tactic:
exact map_zero _

Premises used: map_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n r
hn : n ≠ 0
⊢ HasFiniteFPowerSeriesOnBall f p x n.pred.succ r

Tactic:
rw [← Nat.succ_pred hn] at h

Premises used: Nat.succ_pred
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n r
hn : n ≠ 0
h₁ : HasFiniteFPowerSeriesOnBall f p x n.pred.succ r
⊢ n ≠ 0

Tactic:
rw [← Nat.succ_pred hn] at h

Premises used: Nat.succ_pred
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n.pred.succ r
hn : n ≠ 0
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (n - 1) r

Tactic:
h.fderiv

Premises used: Nat.pred, HasFiniteFPowerSeriesOnBall.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x n.pred.succ r
hn : n ≠ 0
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (n - 1) r

Tactic:
exact h.fderiv

Premises used: HasFiniteFPowerSeriesOnBall.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
y : E
hy : y ∈ s
rcases :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℕ) (n : ℝ≥0∞) (hp : HasFiniteFPowerSeriesOnBall f p y r n),
    CPolynomialAt 𝕜 (F := E →L[𝕜] F) (_root_.fderiv 𝕜 f) y
⊢ CPolynomialAt 𝕜 (F := E →L[𝕜] F) (_root_.fderiv 𝕜 f) y

Tactic:
rcases h y hy with ⟨p, r, n, hp⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
y : E
hy : y ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℕ
n : ℝ≥0∞
hp : HasFiniteFPowerSeriesOnBall f p y r n
⊢ CPolynomialAt 𝕜 (F := E →L[𝕜] F) (_root_.fderiv 𝕜 f) y

Tactic:
hp.fderiv'.cpolynomialAt

Premises used: HasFiniteFPowerSeriesOnBall.cpolynomialAt, HasFiniteFPowerSeriesOnBall.fderiv'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
y : E
hy : y ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℕ
n : ℝ≥0∞
hp : HasFiniteFPowerSeriesOnBall f p y r n
⊢ CPolynomialAt 𝕜 (F := E →L[𝕜] F) (_root_.fderiv 𝕜 f) y

Tactic:
exact hp.fderiv'.cpolynomialAt

Premises used: HasFiniteFPowerSeriesOnBall.cpolynomialAt, HasFiniteFPowerSeriesOnBall.fderiv'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
      f)
    s

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

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, ContinuousLinearMap.comp_cpolynomialOn, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F)
    ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
      f)
    s

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

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, ContinuousLinearMap.comp_cpolynomialOn, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH :
  CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (_root_.iteratedFDeriv 𝕜 n f)
    s
succ :
  CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (Function.comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (_root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f)))
    s
⊢ CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (_root_.iteratedFDeriv 𝕜 (n + 1) f) s

Tactic:
rw [iteratedFDeriv_succ_eq_comp_left]

Premises used: iteratedFDeriv_succ_eq_comp_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH :
  CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (_root_.iteratedFDeriv 𝕜 n f)
    s
⊢ CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (Function.comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F)
      (⇑((↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)) :
                  (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) ≃L[𝕜]
                    ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
                ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
      (_root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f)))
    s

Tactic:
ContinuousLinearMap.comp_cpolynomialOn ?g IH.fderiv

Premises used: ContinuousLinearMap.comp_cpolynomialOn, CPolynomialOn.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH :
  CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (_root_.iteratedFDeriv 𝕜 n f)
    s
h₁ :
  Eq (α :=
    (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →
      ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
    (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
      (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
        ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
    (⇑((↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)) :
                (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) ≃L[𝕜]
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
      (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
        ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
convert! :
  (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
    ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F
⊢ CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (Function.comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
      (_root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f)))
    s

Tactic:
convert! ContinuousLinearMap.comp_cpolynomialOn ?g IH.fderiv

Premises used: ContinuousLinearMap.comp_cpolynomialOn, CPolynomialOn.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH :
  CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (_root_.iteratedFDeriv 𝕜 n f)
    s
⊢ (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
    ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F

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

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryLeftEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH :
  CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (_root_.iteratedFDeriv 𝕜 n f)
    s
⊢ (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
    ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F

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

Premises used: LinearIsometryEquiv.symm, continuousMultilinearCurryLeftEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ
IH :
  CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (_root_.iteratedFDeriv 𝕜 n f)
    s
⊢ Eq (α :=
    (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →
      ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
    (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) ≃ₗᵢ[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
      (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
        ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)
    (⇑((↑(↑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) ↦ E) F)) :
                (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) ≃L[𝕜]
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
              ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
          (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) →L[𝕜]
            ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (x : Fin (n + 1)) ↦ E) F) :
      (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) F) →
        ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)

Tactic:
simp