-- 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
refine₁ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N), ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
refine₂ refine₃ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N),
    let 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), ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
refine₄ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N),
    let 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),
      let T := 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),
        ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
refine₅ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N),
    let 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),
      let T := 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),
        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)
refine₆ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N),
    let 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),
      let T := 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),
        ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
refine₇ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N),
    let 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),
      let T := 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)
        (h'u :
          ∀ (k : ℕ),
            LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞) →
              Summable (β := { i : α // i ∉ T }) (v k ∘ Subtype.val (p := fun (i : α) ↦ i ∉ T))),
        ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑m : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : { i : α // i ∉ T }), f (↑i : α) x
refine₈ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N),
    let 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),
      let T := 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)
        (h'u :
          ∀ (k : ℕ),
            LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞) →
              Summable (β := { i : α // i ∉ T }) (v k ∘ Subtype.val (p := fun (i : α) ↦ i ∉ T)))
        (k : ℕ) (i : { i : α // i ∉ T }) (x : E),
        LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞) →
          norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
              (iteratedFDeriv 𝕜 k (f (↑i : α)) x) ≤
            (v k ∘ Subtype.val (p := fun (i : α) ↦ i ∉ T)) i
refine₉ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N),
    let 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),
      let T := 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)
        (h'u :
          ∀ (k : ℕ),
            LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞) →
              Summable (β := { i : α // i ∉ T }) (v k ∘ Subtype.val (p := fun (i : α) ↦ i ∉ T)))
        (k : ℕ) (i : α) (hi : i ∉ T) (x : E) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞)),
        norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
            (iteratedFDeriv 𝕜 k (f (↑(Subtype.mk (p := fun (i : α) ↦ i ∉ T) i hi) : α)) x) ≤
          comp (α := { i : α // i ∉ T }) (v k) (Subtype.val (p := fun (i : α) ↦ i ∉ T))
            (Subtype.mk (p := fun (i : α) ↦ i ∉ T) i hi)
refine₁₀ :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) ≤ N),
    let 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),
      let T := 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)
        (h'u :
          ∀ (k : ℕ),
            LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞) →
              Summable (β := { i : α // i ∉ T }) (v k ∘ Subtype.val (p := fun (i : α) ↦ i ∉ T)))
        (k : ℕ) (i : α) (hi : i ∉ T) (x : E) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞))
        (hi_1 :
          ∀ x < m + 1,
            ∀ (x_1 : E),
              norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin x) ↦ E) F)
                  (iteratedFDeriv 𝕜 x (f i) x_1) ≤
                v x i),
        norm (E := ContinuousMultilinearMap.{u_3, 0, u_4, u_5} 𝕜 (fun (i : Fin k) ↦ E) F)
            (iteratedFDeriv 𝕜 k (f (↑(Subtype.mk (p := fun (i : α) ↦ i ∉ T) i hi) : α)) x) ≤
          comp (α := { i : α // i ∉ T }) (v k) (Subtype.val (p := fun (i : α) ↦ i ∉ T))
            (Subtype.mk (p := fun (i : α) ↦ i ∉ T) i hi)
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑N : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x

Tactic:
classical
    refine contDiff_iff_forall_nat_le.2 fun m hm => ?_
    let t : Set α :=
      { i : α | ¬∀ k : ℕ, k ∈ Finset.range (m + 1) → ∀ x, ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i }
    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
    let T : Finset α := ht.toFinset
    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
    rw [this]
    apply (ContDiff.sum fun i _ => (hf i).of_le (mod_cast hm)).add
    have h'u : ∀ k : ℕ, (k : ℕ∞) ≤ m → Summable (v k ∘ ((↑) : { i // i ∉ T } → α)) := fun k hk =>
      (hv k (hk.trans hm)).subtype _
    refine contDiff_tsum (fun i => (hf i).of_le (mod_cast hm)) h'u ?_
    rintro k ⟨i, hi⟩ x hk
    simp only [t, T, Finite.mem_toFinset, mem_setOf_eq, Finset.mem_range, not_forall, not_le,
      exists_prop, not_exists, not_and, not_lt] at hi
    exact hi k (Nat.lt_succ_iff.2 (WithTop.coe_le_coe.1 hk)) x

Premises used: not_le, Iff.mpr, contDiff_iff_forall_nat_le, Set.Finite.mem_toFinset, not_exists, ContDiff.sum, Set.mem_setOf_eq, Finset.mem_range, exists_prop, ContDiff.of_le, ContDiff.add, not_lt, not_and, Classical.not_forall