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
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:
exact (continuousMultilinearCurryLeftEquiv 𝕜
        (fun _ : Fin (k + 1) => E) F).symm.toContinuousLinearEquiv.map_tsum

Premises used: ContinuousLinearEquiv.map_tsum, LinearIsometryEquiv.symm, LinearIsometryEquiv.toContinuousLinearEquiv, continuousMultilinearCurryLeftEquiv
-- 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
n : α
x : E
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
      (fderiv 𝕜 (fun (x : E) ↦ iteratedFDeriv 𝕜 k (f n) x) x) ≤
    v (k + 1) n

Tactic:
simpa only [iteratedFDeriv_succ_eq_comp_left, LinearIsometryEquiv.norm_map, comp_apply]
        using h'f k.succ n x hk

Premises used: LinearIsometryEquiv.norm_map, Function.comp_apply, iteratedFDeriv_succ_eq_comp_left, Nat.succ
-- 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 : ℕ
hk : (↑k : ℕ∞) ≤ N
zero :
  ∀ (hk : (↑0 : ℕ∞) ≤ N),
    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
succ :
  ∀ (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),
    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
⊢ 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

Tactic:
induction k with
  | zero =>
    ext1 x
    simp_rw [iteratedFDeriv_zero_eq_comp]
    exact (continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv.map_tsum
  | succ k IH =>
    have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk
    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
    simp_rw [iteratedFDeriv_succ_eq_comp_left, IH h'k.le]
    rw [fderiv_tsum (hv _ hk) (fun n => (hf n).differentiable_iteratedFDeriv
        (mod_cast h'k)) _ A]
    · ext1 x
      exact (continuousMultilinearCurryLeftEquiv 𝕜
        (fun _ : Fin (k + 1) => E) F).symm.toContinuousLinearEquiv.map_tsum
    · intro n x
      simpa only [iteratedFDeriv_succ_eq_comp_left, LinearIsometryEquiv.norm_map, comp_apply]
        using h'f k.succ n x hk

Premises used: ContinuousLinearEquiv.map_tsum, LinearIsometryEquiv.symm, LinearIsometryEquiv.norm_map, continuousMultilinearCurryFin0, iteratedFDeriv_zero_eq_comp, Function.comp_apply, LinearIsometryEquiv.toContinuousLinearEquiv, continuousMultilinearCurryLeftEquiv, 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 : ℕ
hk : (↑k : ℕ∞) ≤ N
x : E
rw rw₁ :
  Eq (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 k (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F))
      x)
    (∑' (n : α), iteratedFDeriv 𝕜 k (f n) x)
⊢ Eq (α := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
    (iteratedFDeriv 𝕜 k (fun (y : E) ↦ ∑' (n : α), f n y) x) (∑' (n : α), iteratedFDeriv 𝕜 k (f n) x)

Tactic:
rw [iteratedFDeriv_tsum hf hv h'f hk]

Premises used: iteratedFDeriv_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
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
rw :
  (∀ (m : ℕ),
      (↑m : ℕ∞) ≤ N →
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
          iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x) ∧
    ∀ (m : ℕ),
      (↑m : ℕ∞) < N →
        Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
          iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑N : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x

Tactic:
rw [contDiff_iff_continuous_differentiable]

Premises used: contDiff_iff_continuous_differentiable
-- 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
left :
  ∀ (m : ℕ),
    (↑m : ℕ∞) ≤ N →
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
        iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x
right :
  ∀ (m : ℕ),
    (↑m : ℕ∞) < N →
      Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
        iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x
⊢ (∀ (m : ℕ),
      (↑m : ℕ∞) ≤ N →
        Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
          iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x) ∧
    ∀ (m : ℕ),
      (↑m : ℕ∞) < N →
        Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
          iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x

Tactic:
constructor
-- 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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
    (fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
      x

Tactic:
continuous_tsum ?_ (hv m hm) ?_

Premises used: continuous_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
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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
left : ∀ (i : α), Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (iteratedFDeriv 𝕜 m (f i))
left₁ :
  ∀ (n : α) (x : E),
    norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n) x) ≤
      v m n
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : E) ↦
    (fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
      x

Tactic:
refine continuous_tsum ?_ (hv m hm) ?_

Premises used: continuous_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
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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
i : α
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (iteratedFDeriv 𝕜 m (f i))

Tactic:
ContDiff.continuous_iteratedFDeriv (mod_cast hm) (hf i)

Premises used: ContDiff.continuous_iteratedFDeriv
-- 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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
i : α
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (iteratedFDeriv 𝕜 m (f i))

Tactic:
exact ContDiff.continuous_iteratedFDeriv (mod_cast hm) (hf i)

Premises used: ContDiff.continuous_iteratedFDeriv
-- 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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
n : α
x : E
⊢ norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n) x) ≤ v m n

Tactic:
h'f _ _ _ hm
-- 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
m : ℕ
hm : (↑m : ℕ∞) ≤ N
n : α
x : E
⊢ norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n) x) ≤ v m n

Tactic:
exact h'f _ _ _ hm
-- 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
m : ℕ
hm : (↑m : ℕ∞) < N
⊢ (↑(m + 1) : ℕ∞) ≤ N

Tactic:
simpa only [ENat.coe_add, ENat.coe_one] using Order.add_one_le_of_lt hm

Premises used: ENat.coe_one, Order.add_one_le_of_lt, ENat.coe_add
-- 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
m : ℕ
hm : (↑m : ℕ∞) < N
⊢ (↑(m + 1) : ℕ∞) ≤ N

Tactic:
have h'm : ((m + 1 : ℕ) : ℕ∞) ≤ N := by
      simpa only [ENat.coe_add, ENat.coe_one] using Order.add_one_le_of_lt hm
-- 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
m : ℕ
hm : (↑m : ℕ∞) < N
h'm : (↑(m + 1) : ℕ∞) ≤ N
right :
  Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
    (fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
      x
⊢ Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
    iteratedFDeriv 𝕜 m (fun (x : E) ↦ ∑' (i : α), f i x) x

Tactic:
rw [iteratedFDeriv_tsum hf hv h'f hm.le]

Premises used: iteratedFDeriv_tsum, LT.lt.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
m : ℕ
hm : (↑m : ℕ∞) < N
h'm : (↑(m + 1) : ℕ∞) ≤ N
⊢ ∀ (n : α) (x : E),
    HasFDerivAt (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n))
      (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x

Tactic:
have A n x : HasFDerivAt (iteratedFDeriv 𝕜 m (f n)) (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x :=
      (ContDiff.differentiable_iteratedFDeriv (mod_cast hm)
        (hf n)).differentiableAt.hasFDerivAt
-- 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
m : ℕ
hm : (↑m : ℕ∞) < N
h'm : (↑(m + 1) : ℕ∞) ≤ N
A :
  ∀ (n : α) (x : E),
    HasFDerivAt (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n))
      (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
⊢ Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
    (fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
      x

Tactic:
differentiable_tsum (hv _ h'm) A fun n x => ?_

Premises used: differentiable_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
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
m : ℕ
hm : (↑m : ℕ∞) < N
h'm : (↑(m + 1) : ℕ∞) ≤ N
A :
  ∀ (n : α) (x : E),
    HasFDerivAt (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n))
      (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
right :
  ∀ (n : α) (x : E),
    norm (E := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F)
        (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) ≤
      v (m + 1) n
⊢ Differentiable 𝕜 (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) fun (x : E) ↦
    (fun (x : E) ↦
        (∑' (n : α), iteratedFDeriv 𝕜 m (f n) x :
          ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F))
      x

Tactic:
refine differentiable_tsum (hv _ h'm) A fun n x => ?_

Premises used: differentiable_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
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
m : ℕ
hm : (↑m : ℕ∞) < N
h'm : (↑(m + 1) : ℕ∞) ≤ N
A :
  ∀ (n : α) (x : E),
    HasFDerivAt (F := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F) (iteratedFDeriv 𝕜 m (f n))
      (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) x
n : α
x : E
right :
  norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (x : Fin (m + 1)) ↦ E) F)
      (iteratedFDeriv 𝕜 (m + 1) (f n) x) ≤
    v (m + 1) n
⊢ norm (E := E →L[𝕜] ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin m) ↦ E) F)
      (fderiv 𝕜 (iteratedFDeriv 𝕜 m (f n)) x) ≤
    v (m + 1) n

Tactic:
rw [fderiv_iteratedFDeriv, comp_apply, LinearIsometryEquiv.norm_map]

Premises used: fderiv_iteratedFDeriv, LinearIsometryEquiv.norm_map, Function.comp_apply