awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f y) 0
have inl₁ : f =ᶠ[𝓝 y] fun (x : E) ↦ 0
Tactic: rw [Filter.EventuallyEq.fderiv_eq (f := fun _ ↦ 0)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ f z = (fun (x : E) ↦ (0 : F)) z
have rw : Eq.{v + 1} (α := F) 0 ((fun (x : E) ↦ (0 : F)) z)
Tactic: rw [h.eq_zero_of_bound_zero z hz]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 : ℕ
⊢ p.derivSeries n = 0
have 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)
Tactic: apply ContinuousMultilinearMap.ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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) ((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)
have 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)
Tactic: change (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOriginSeries 1 n a) = 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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)
        ((p.changeOriginSeries 1 n : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) a) :
      E →L[𝕜] F)
    (0 : E →L[𝕜] F)
have 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)
Tactic: rw [p.changeOriginSeries_finite_of_finite h.finite 1 (Nat.zero_le _)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (hypothesis)
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 := E →L[𝕜] F) (fderiv 𝕜 f) p.derivSeries x (n - 1) r
have h₁ : HasFiniteFPowerSeriesOnBall f p x n.pred.succ r
Tactic: rw [← Nat.succ_pred hn] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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
⊢ CPolynomialAt 𝕜 (F := E →L[𝕜] F) (_root_.fderiv 𝕜 f) y
have rcases : ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℕ) (n : ℝ≥0∞) (hp : HasFiniteFPowerSeriesOnBall f p y r n),
  CPolynomialAt 𝕜 (F := E →L[𝕜] F) (_root_.fderiv 𝕜 f) y
Tactic: rcases h y hy with ⟨p, r, n, hp⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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)
    (_root_.iteratedFDeriv 𝕜 (n + 1) f) s
have 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
Tactic: rw [iteratedFDeriv_succ_eq_comp_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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.{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
have 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)
Tactic: convert! ContinuousLinearMap.comp_cpolynomialOn ?g IH.fderiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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)
⊢ 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
have 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
Tactic: convert! ContinuousLinearMap.comp_cpolynomialOn ?g IH.fderiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 : ℕ
⊢ CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (_root_.iteratedFDeriv 𝕜 n f)
    s
have zero : CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F) (_root_.iteratedFDeriv 𝕜 0 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
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 : ℕ
zero :
  CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin 0) ↦ E) F) (_root_.iteratedFDeriv 𝕜 0 f)
    s
⊢ CPolynomialOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u, v} 𝕜 (fun (i : Fin n) ↦ E) F) (_root_.iteratedFDeriv 𝕜 n f)
    s
have succ : ∀ (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)
    (_root_.iteratedFDeriv 𝕜 (n + 1) 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
n : ℕ
⊢ CPolynomialOn 𝕜 (deriv^[n] f) s
have zero : CPolynomialOn 𝕜 (deriv^[0] f) s
Tactic: induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
n : ℕ
zero : CPolynomialOn 𝕜 (deriv^[0] f) s
⊢ CPolynomialOn 𝕜 (deriv^[n] f) s
have succ : ∀ (n : ℕ) (IH : CPolynomialOn 𝕜 (deriv^[n] f) s), CPolynomialOn 𝕜 (deriv^[n + 1] f) s
Tactic: induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
k l : ℕ
h : k + l ≠ Fintype.card ι
x : { s : Finset (Fin (k + l)) // s.card = l }
h_1 : Membership.mem (γ := Finset { s : Finset (Fin (k + l)) // s.card = l }) Finset.univ x
⊢ Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    (changeOriginSeriesTerm (f.toFormalMultilinearSeries (E := E)) k l (↑x : Finset (Fin (k + l))) ⋯) 0
have simp_rw : Eq (α :=
  ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
    (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
  ((curryFinFinset 𝕜 ((i : ι) → E i) F sorry sorry :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + l)) ↦ (i : ι) → E i) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
            (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
      (f.toFormalMultilinearSeries (E := E) (k + l)) :
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
  (0 :
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
Tactic: simp_rw [FormalMultilinearSeries.changeOriginSeriesTerm,
      toFormalMultilinearSeries, dif_neg h.symm, LinearIsometryEquiv.map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
k l : ℕ
h : k + l ≠ Fintype.card ι
x : { s : Finset (Fin (k + l)) // s.card = l }
h_1 : Membership.mem (γ := Finset { s : Finset (Fin (k + l)) // s.card = l }) Finset.univ x
simp_rw :
  Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    ((curryFinFinset 𝕜 ((i : ι) → E i) F ⋯ ⋯ :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + l)) ↦ (i : ι) → E i) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
              (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
        (f.toFormalMultilinearSeries (E := E) (k + l)) :
      ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
        (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    (0 :
      ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
        (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
⊢ Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    (changeOriginSeriesTerm (f.toFormalMultilinearSeries (E := E)) k l (↑x : Finset (Fin (k + l))) ⋯) 0
have simp_rw₁ : Eq (α :=
  ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
    (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
  ((curryFinFinset 𝕜 ((i : ι) → E i) F sorry sorry :
      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + l)) ↦ (i : ι) → E i) F) →
        ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
          (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    (if h : Fintype.card ι = k + l then
      domDomCongr (Fintype.equivFinOfCardEq h)
        (f.compContinuousLinearMap (M₁ := fun (i : ι) ↦ (i : ι) → E i) (M₁' := E) (ContinuousLinearMap.proj (φ := E)))
    else 0))
  0
Tactic: simp_rw [FormalMultilinearSeries.changeOriginSeriesTerm,
      toFormalMultilinearSeries, dif_neg h.symm, LinearIsometryEquiv.map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
k l : ℕ
h : k + l ≠ Fintype.card ι
x : { s : Finset (Fin (k + l)) // s.card = l }
h_1 : Membership.mem (γ := Finset { s : Finset (Fin (k + l)) // s.card = l }) Finset.univ x
simp_rw :
  Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    ((curryFinFinset 𝕜 ((i : ι) → E i) F ⋯ ⋯ :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + l)) ↦ (i : ι) → E i) F) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
              (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
        (f.toFormalMultilinearSeries (E := E) (k + l)) :
      ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
        (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    (0 :
      ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
        (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
simp_rw₁ :
  Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    ((curryFinFinset 𝕜 ((i : ι) → E i) F ⋯ ⋯ :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + l)) ↦ (i : ι) → E i) F) →
          ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
            (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
      (if h : Fintype.card ι = k + l then
        domDomCongr (Fintype.equivFinOfCardEq h)
          (f.compContinuousLinearMap (M₁ := fun (i : ι) ↦ (i : ι) → E i) (M₁' := E) (ContinuousLinearMap.proj (φ := E)))
      else 0))
    0
⊢ Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
      (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    (changeOriginSeriesTerm (f.toFormalMultilinearSeries (E := E)) k l (↑x : Finset (Fin (k + l))) ⋯) 0
have simp_rw₂ : Eq (α :=
  ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
    (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
  ((curryFinFinset 𝕜 ((i : ι) → E i) F sorry sorry :
      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (k + l)) ↦ (i : ι) → E i) F) →
        ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ (i : ι) → E i)
          (ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ (i : ι) → E i) F))
    0)
  0
Tactic: simp_rw [FormalMultilinearSeries.changeOriginSeriesTerm,
      toFormalMultilinearSeries, dif_neg h.symm, LinearIsometryEquiv.map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
⊢ (continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
      (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1) =
    f.linearDeriv (M₁ := E) x
have h : ∀ (y : (i : ι) → E i),
  Eq.{v + 1} (α := F)
    ((((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
              (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1) :
            ((i : ι) → E i) →L[𝕜] F) :
          (a : (i : ι) → E i) → F)
        y :
      F)
    ((f.linearDeriv (M₁ := E) x : (a : (i : ι) → E i) → F) y : F)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
⊢ Eq.{v + 1} (α := F)
    ((((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
              (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1) :
            ((i : ι) → E i) →L[𝕜] F) :
          (a : (i : ι) → E i) → F)
        y :
      F)
    ((f.linearDeriv (M₁ := E) x : (a : (i : ι) → E i) → F) y : F)
have h : Eq.{v + 1} (α := F)
  ((∑' (n : ℕ),
          (changeOriginSeries (f.toFormalMultilinearSeries (E := E)) 1 n :
              (a : (i : Fin n) → (i : ι) → E i) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F)
            fun (x_1 : Fin n) ↦ x :
        (a : (i : Fin 1) → (i : ι) → E i) → F)
      (Fin.snoc (α := fun (i : Fin 1) ↦ (i : ι) → E i) 0 y) :
    F)
  (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
Tactic: rw [continuousMultilinearCurryFin1_apply, linearDeriv_apply,
      changeOrigin, FormalMultilinearSeries.sum]