-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
refine :
  ∀ (ε : ℝ) (εpos : ε > 0),
    ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
refine₁ :
  ∀ (ε : ℝ) (εpos : ε > 0) (this : ∀ᶠ (b : Finset ι) in atTop, ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
refine₂ :
  ∀ (ε : ℝ) (εpos : 0 < ε)
    (this : ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
refine₃ :
  ∀ (ε : ℝ) (εpos : 0 < ε) (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
refine₄ :
  ∀ (hfu : ∃ (v : Set ι), Membership.mem (γ := Filter ι) cofinite v ∧ ∀ y ∈ v, ∀ x ∈ s, ‖f y x‖ ≤ u y) (ε : ℝ)
    (εpos : 0 < ε) (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
refine₅ :
  ∀ (ε : ℝ) (εpos : 0 < ε) (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε)
    (N : Set ι) (hN : Membership.mem (γ := Filter ι) cofinite N) (HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
refine₆ :
  ∀ (ε : ℝ) (εpos : 0 < ε) (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε)
    (N : Set ι) (hN : Membership.mem (γ := Filter ι) cofinite N) (HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y) (n : Finset ι)
    (hn : Finite.toFinset (s := Nᶜ) hN ∪ t ⊆ n) (x : β) (hx : x ∈ s),
    dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
⊢ TendstoUniformlyOn.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : ι), f n x) atTop s
have refine₇ : ∀ (ε : ℝ) (εpos : 0 < ε) (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε)
  (N : Set ι) (hN : Membership.mem (γ := Filter ι) cofinite N) (HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y) (n : Finset ι)
  (hn : Finite.toFinset (s := Nᶜ) hN ∪ t ⊆ n) (x : β) (hx : x ∈ s) (A : Summable (α := ℝ) fun (n : ι) ↦ ‖f n x‖),
  dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
Tactic: classical
  refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
  have := (tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos
  simp only [gt_iff_lt,
    eventually_atTop, ge_iff_le, Finset.le_eq_subset] at *
  obtain ⟨t, ht⟩ := this
  rw [eventually_iff_exists_mem] at hfu
  obtain ⟨N, hN, HN⟩ := hfu
  refine ⟨hN.toFinset ∪ t, fun n hn x hx => ?_⟩
  have A : Summable fun n => ‖f n x‖ := by
    apply Summable.add_compl (s := hN.toFinset) Summable.of_finite
    apply Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) _ (hu.subtype _)
    simp only [comp_apply, Subtype.forall, Set.mem_compl_iff, Finset.mem_coe]
    aesop
  rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl n, add_sub_cancel_left]
  apply lt_of_le_of_lt _ (ht n (Finset.union_subset_right hn))
  apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
  apply (A.subtype _).tsum_le_tsum _ (hu.subtype _)
  simp only [comp_apply, Subtype.forall]
  apply fun i hi => HN i ?_ x hx
  have : i ∉ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
  simp_all
Cleared hypotheses: hfu