awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
⊢ Eq (α := (x : E) → F) (fun (x : E) ↦ ∑' (n : α), f n x) 0

Tactic:
have : (fun x => ∑' n, f n x) = 0 := by ext1 x; exact tsum_eq_zero_of_not_summable (h x)
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
this : Eq (α := (x : E) → F) (fun (x : E) ↦ ∑' (n : α), f n x) 0
neg : Differentiable.{u_3, u_4, u_5} 𝕜 (E := E) (F := F) 0
⊢ Differentiable.{u_3, u_4, u_5} 𝕜 (F := F) fun (y : E) ↦ ∑' (n : α), f n y

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
this : Eq (α := (x : E) → F) (fun (x : E) ↦ ∑' (n : α), f n x) 0
⊢ Differentiable.{u_3, u_4, u_5} 𝕜 (E := E) (F := F) 0

Tactic:
differentiable_const 0

Premises used: differentiable_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
this : Eq (α := (x : E) → F) (fun (x : E) ↦ ∑' (n : α), f n x) 0
⊢ Differentiable.{u_3, u_4, u_5} 𝕜 (E := E) (F := F) 0

Tactic:
exact differentiable_const 0

Premises used: differentiable_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
⊢ ∀ (n : α) (y : 𝕜), HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y

Tactic:
simp_rw [hasDerivAt_iff_hasFDerivAt] at hg

Premises used: hasDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ Differentiable.{u_3, u_3, u_5} 𝕜 (F := F) fun (z : 𝕜) ↦ ∑' (n : α), g n z

Tactic:
differentiable_tsum hu hg ?_

Premises used: differentiable_tsum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
refine : ∀ (n : α) (x : 𝕜), norm (E := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)) ≤ u n
⊢ Differentiable.{u_3, u_3, u_5} 𝕜 (F := F) fun (z : 𝕜) ↦ ∑' (n : α), g n z

Tactic:
refine differentiable_tsum hu hg ?_

Premises used: differentiable_tsum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ ∀ (n : α) (x : 𝕜), norm (E := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)) ≤ u n

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
x₀ : E
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), norm (E := E →L[𝕜] F) (fderiv 𝕜 (f n) x) ≤ u n
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
x : E
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ ∑' (n : α), f n y) x) (∑' (n : α), fderiv 𝕜 (f n) x)

Tactic:
(hasFDerivAt_tsum hu (fun n x => (hf n x).hasFDerivAt) hf' hf0 _).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, hasFDerivAt_tsum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
y : 𝕜
⊢ Eq.{u_5 + 1} (α := F) (deriv (fun (z : 𝕜) ↦ ∑' (n : α), g n z) y) (∑' (n : α), deriv (g n) y)

Tactic:
(hasDerivAt_tsum hu (fun n y => (hg n y).hasDerivAt) hg' hg0 _).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, hasDerivAt_tsum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
x₀ : E
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), norm (E := E →L[𝕜] F) (fderiv 𝕜 (f n) x) ≤ u n
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
h : ∀ (x : E), Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ ∑' (n : α), f n y) x) (∑' (n : α), fderiv 𝕜 (f n) x)
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderiv 𝕜 fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), fderiv 𝕜 (f n) x

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
x₀ : E
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), norm (E := E →L[𝕜] F) (fderiv 𝕜 (f n) x) ≤ u n
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
x : E
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ ∑' (n : α), f n y) x) (∑' (n : α), fderiv 𝕜 (f n) x)

Tactic:
fderiv_tsum_apply hu hf hf' hf0 x

Premises used: fderiv_tsum_apply
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
x₀ : E
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), norm (E := E →L[𝕜] F) (fderiv 𝕜 (f n) x) ≤ u n
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
x : E
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ ∑' (n : α), f n y) x) (∑' (n : α), fderiv 𝕜 (f n) x)

Tactic:
exact fderiv_tsum_apply hu hf hf' hf0 x

Premises used: fderiv_tsum_apply
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
h : ∀ (x : 𝕜), Eq.{u_5 + 1} (α := F) (deriv (fun (y : 𝕜) ↦ ∑' (n : α), g n y) x) (∑' (n : α), deriv (g n) x)
⊢ Eq (α := (x : 𝕜) → F) (deriv fun (y : 𝕜) ↦ ∑' (n : α), g n y) fun (y : 𝕜) ↦ ∑' (n : α), deriv (g n) y

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
x : 𝕜
⊢ Eq.{u_5 + 1} (α := F) (deriv (fun (y : 𝕜) ↦ ∑' (n : α), g n y) x) (∑' (n : α), deriv (g n) x)

Tactic:
deriv_tsum_apply hu hg hg' hg0 x

Premises used: deriv_tsum_apply
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y₀
x : 𝕜
⊢ Eq.{u_5 + 1} (α := F) (deriv (fun (y : 𝕜) ↦ ∑' (n : α), g n y) x) (∑' (n : α), deriv (g n) x)

Tactic:
exact deriv_tsum_apply hu hg hg' hg0 x

Premises used: deriv_tsum_apply
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
hk : (↑0 : ℕ∞) ≤ N
zero :
  ∀ (x : E),
    Eq (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (iteratedFDeriv 𝕜 0 (fun (y : E) ↦ ∑' (n : α), f n y) x) (∑' (n : α), iteratedFDeriv 𝕜 0 (f n) x)
⊢ Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDeriv 𝕜 0 fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 0 (f n) x

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
hk : (↑0 : ℕ∞) ≤ N
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (comp (β := F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      (fun (y : E) ↦ ∑' (n : α), f n y) x)
    (∑' (n : α),
      ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
          f n)
        x)

Tactic:
(continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv.map_tsum

Premises used: ContinuousLinearEquiv.map_tsum, LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
hk : (↑0 : ℕ∞) ≤ N
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (comp (β := F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
        (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F)
      (fun (y : E) ↦ ∑' (n : α), f n y) x)
    (∑' (n : α),
      ((⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) :
            (a : F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) F) ∘
          f n)
        x)

Tactic:
exact (continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv.map_tsum

Premises used: ContinuousLinearEquiv.map_tsum, LinearIsometryEquiv.symm, continuousMultilinearCurryFin0, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
IH :
  ∀ (hk : (↑k : ℕ∞) ≤ N),
    Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : (↑(k + 1) : ℕ∞) ≤ N
⊢ (↑k : ℕ∞) < N

Tactic:
have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
IH :
  ∀ (hk : (↑k : ℕ∞) ≤ N),
    Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : (↑(k + 1) : ℕ∞) ≤ N
h'k : (↑k : ℕ∞) < N
⊢ Summable (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) fun (n : α) ↦
    iteratedFDeriv 𝕜 k (f n) 0

Tactic:
have A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0 :=
      .of_norm_bounded (hv k h'k.le) fun n ↦ h'f k n 0 h'k.le
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
IH :
  ∀ (hk : (↑k : ℕ∞) ≤ N),
    Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : (↑(k + 1) : ℕ∞) ≤ N
h'k : (↑k : ℕ∞) < N
A :
  Summable (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) fun (n : α) ↦
    iteratedFDeriv 𝕜 k (f n) 0
succ :
  Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
    (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
      (fderiv 𝕜 fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x))
    fun (x : E) ↦
    ∑' (n : α),
      comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
        (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
                ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x
⊢ Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin (k + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (k + 1) fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦
    ∑' (n : α), iteratedFDeriv 𝕜 (k + 1) (f n) x

Tactic:
simp_rw [iteratedFDeriv_succ_eq_comp_left, IH h'k.le]

Premises used: LT.lt.le, iteratedFDeriv_succ_eq_comp_left
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N : WithTop ℕ∞) (f i)
hv : ∀ (k : ℕ), (↑k : ℕ∞) ≤ N → Summable (v k)
h'f :
  ∀ (k : ℕ) (i : α) (x : E),
    (↑k : ℕ∞) ≤ N →
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
        v k i
k : ℕ
IH :
  ∀ (hk : (↑k : ℕ∞) ≤ N),
    Eq (α := E → ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (iteratedFDeriv 𝕜 k fun (y : E) ↦ ∑' (n : α), f n y) fun (x : E) ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : (↑(k + 1) : ℕ∞) ≤ N
h'k : (↑k : ℕ∞) < N
A :
  Summable (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) fun (n : α) ↦
    iteratedFDeriv 𝕜 k (f n) 0
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
    (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
            (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
              ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
        (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
          ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
      (fun (x : E) ↦ ∑' (n : α), fderiv 𝕜 (fun (x : E) ↦ iteratedFDeriv 𝕜 k (f n) x) x) x)
    (∑' (n : α),
      comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
        (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
              (E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) ≃ₗᵢ[𝕜]
                ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (k + 1)) ↦ E) F) :
          (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin (k + 1)) ↦ E) F)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x)

Tactic:
(continuousMultilinearCurryLeftEquiv 𝕜
        (fun _ : Fin (k + 1) => E) F).symm.toContinuousLinearEquiv.map_tsum

Premises used: ContinuousLinearEquiv.map_tsum, LinearIsometryEquiv.symm, LinearIsometryEquiv.toContinuousLinearEquiv, continuousMultilinearCurryLeftEquiv