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
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
⊢ 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

Tactic:
h'f _ _ _ h'm
-- 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
⊢ 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

Tactic:
exact h'f _ _ _ h'm
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑N : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x

Tactic:
contDiff_iff_forall_nat_le.2 fun m hm => ?_

Premises used: Iff.mpr, contDiff_iff_forall_nat_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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i
refine :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N), ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑N : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x

Tactic:
refine contDiff_iff_forall_nat_le.2 fun m hm => ?_

Premises used: Iff.mpr, contDiff_iff_forall_nat_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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          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 :
  ∀ i ∈ Finset.range (m + 1),
    ∀ᶠ (x : α) in cofinite,
      ∀ (x_1 : E),
        norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin i) ↦ E) F)
            (iteratedFDeriv 𝕜 i (f x) x_1) ≤
          v i x
⊢ ∀ᶠ (i : α) in cofinite,
    ∀ k ∈ Finset.range (m + 1),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F) (iteratedFDeriv 𝕜 k (f i) x) ≤
          v k i

Tactic:
rw [eventually_all_finset]

Premises used: Filter.eventually_all_finset
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
i : ℕ
hi : i ∈ Finset.range (m + 1)
a : (↑i : ℕ∞) ≤ N
⊢ ∀ᶠ (x : α) in cofinite,
    ∀ (x_1 : E),
      norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin i) ↦ E) F) (iteratedFDeriv 𝕜 i (f x) x_1) ≤
        v i x

Tactic:
apply h'f
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m

Tactic:
simp only [Finset.mem_range_succ_iff] at hi

Premises used: Finset.mem_range_succ_iff
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
i : ℕ
hi : i ≤ m
⊢ (↑i : ℕ∞) ≤ N

Tactic:
(WithTop.coe_le_coe.2 hi).trans hm

Premises used: Iff.mpr, LE.le.trans, WithTop.coe_le_coe
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
i : ℕ
hi : i ≤ m
⊢ (↑i : ℕ∞) ≤ N

Tactic:
exact (WithTop.coe_le_coe.2 hi).trans hm

Premises used: Iff.mpr, LE.le.trans, WithTop.coe_le_coe
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
⊢ t.Finite

Tactic:
have ht : Set.Finite t :=
      haveI A :
        ∀ᶠ i in (Filter.cofinite : Filter α),
          ∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x : E, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i := by
        rw [eventually_all_finset]
        intro i hi
        apply h'f
        simp only [Finset.mem_range_succ_iff] at hi
        exact (WithTop.coe_le_coe.2 hi).trans hm
      eventually_cofinite.2 A
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
h :
  ∀ (x : E),
    ∑' (i : α), f i x =
      HAdd.hAdd (α := (x : E) → F) (β := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x)
        (fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x) x
⊢ (fun (x : E) ↦ ∑' (i : α), f i x) =
    HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
x : E
⊢ ∑' (i : α), f i x =
    HAdd.hAdd (α := (x : E) → F) (β := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x)
      (fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x) x

Tactic:
(Summable.sum_add_tsum_subtype_compl ?_ T).symm

Premises used: Summable.sum_add_tsum_subtype_compl, Eq.symm
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
x : E
h : Summable.{u_5, u_1} (α := F) fun (i : α) ↦ f i x
⊢ ∑' (i : α), f i x =
    HAdd.hAdd (α := (x : E) → F) (β := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x)
      (fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x) x

Tactic:
refine (Summable.sum_add_tsum_subtype_compl ?_ T).symm

Premises used: Summable.sum_add_tsum_subtype_compl, Eq.symm
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
x : E
⊢ Summable.{u_5, u_1} (α := F) fun (i : α) ↦ f i x

Tactic:
.of_norm_bounded_eventually (hv 0 zero_le) ?_

Premises used: zero_le, Summable.of_norm_bounded_eventually, 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
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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
x : E
h : ∀ᶠ (i : α) in cofinite, ‖f i x‖ ≤ v 0 i
⊢ Summable.{u_5, u_1} (α := F) fun (i : α) ↦ f i x

Tactic:
refine .of_norm_bounded_eventually (hv 0 zero_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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
x : E
h :
  ∀ (i : α)
    (hi :
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 (f i) x) ≤
          v 0 i),
    ‖f i x‖ ≤ v 0 i
⊢ ∀ᶠ (i : α) in cofinite, ‖f i x‖ ≤ v 0 i

Tactic:
filter_upwards [h'f 0 zero_le] with i hi

Premises used: zero_le, 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
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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
x : E
i : α
hi :
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv 𝕜 0 (f i) x) ≤
      v 0 i
⊢ ‖f i x‖ ≤ v 0 i

Tactic:
simpa only [norm_iteratedFDeriv_zero] using hi x

Premises used: norm_iteratedFDeriv_zero
-- 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
⊢ (fun (x : E) ↦ ∑' (i : α), f i x) =
    HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x

Tactic:
have : (fun x => ∑' i, f i x) = (fun x => ∑ i ∈ T, f i x) +
        fun x => ∑' i : { i // i ∉ T }, f i x := by
      ext1 x
      refine (Summable.sum_add_tsum_subtype_compl ?_ T).symm
      refine .of_norm_bounded_eventually (hv 0 zero_le) ?_
      filter_upwards [h'f 0 zero_le] with i hi
      simpa only [norm_iteratedFDeriv_zero] using hi 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 : ℕ),
    (↑k : ℕ∞) ≤ N →
      ∀ᶠ (i : α) in cofinite,
        ∀ (x : E),
          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
t : Set α :=
  {i : α |
    ¬∀ k ∈ Finset.range (m + 1),
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f i) x) ≤
            v k i}
ht : t.Finite
T : Finset α := ht.toFinset (s := t)
this :
  (fun (x : E) ↦ ∑' (i : α), f i x) =
    HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
rw :
  ContDiff 𝕜 (↑m : WithTop ℕ∞)
    (HAdd.hAdd (α := (x : E) → F) (fun (x : E) ↦ ∑ i ∈ T, f i x) fun (x : E) ↦
      ∑' (i : { i : α // i ∉ T }), f (↑i : α) x)
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x

Tactic:
rw [this]