-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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
⊢ ContDiff.{u_3, u_4, u_5} 𝕜 (F := F) (↑N : WithTop ℕ∞) fun (x : E) ↦ ∑' (i : α), f i x
have 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
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