awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ε : ℝ
ε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) < ε
have simp : ∀ (ε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) < ε
Tactic: simp only [gt_iff_lt,
    eventually_atTop, ge_iff_le, Finset.le_eq_subset] at *
Cleared hypotheses: εpos, this
-- 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
ε : ℝ
ε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) < ε
have obtain : ∀ (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) < ε
Tactic: obtain ⟨t, ht⟩ := this
Cleared hypotheses: this
-- 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
ε : ℝ
ε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) < ε
have rw : ∀ (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) < ε
Tactic: rw [eventually_iff_exists_mem] at hfu
Cleared hypotheses: hfu, ε, εpos, t, ht
-- 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 : ∃ (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) < ε
have obtain : ∀ (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) < ε
Tactic: obtain ⟨N, hN, HN⟩ := hfu
Cleared hypotheses: hfu
-- 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 β
ε : ℝ
ε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) < ε
have refine : ∀ (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) < ε
Tactic: refine ⟨hN.toFinset ∪ t, fun n hn x hx => ?_⟩
-- 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 β
ε : ℝ
ε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
⊢ Summable (α := ℝ) fun (n : ι) ↦ ‖f n x‖
have apply : Summable.{0, u_4} (α := ℝ) (β := (↑(↑(Finite.toFinset (s := Nᶜ) hN) : Set ι)ᶜ : Type u_4))
  ((fun (n : ι) ↦ ‖f n x‖) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑(Finite.toFinset (s := Nᶜ) hN) : Set ι)ᶜ))
Tactic: apply Summable.add_compl (s := hN.toFinset) Summable.of_finite
-- 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 β
ε : ℝ
ε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
⊢ Summable.{0, u_4} (α := ℝ) (β := (↑(↑(Finite.toFinset (s := Nᶜ) hN) : Set ι)ᶜ : Type u_4))
    ((fun (n : ι) ↦ ‖f n x‖) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑(Finite.toFinset (s := Nᶜ) hN) : Set ι)ᶜ))
have apply : ∀ (b : { x : ι // x ∈ (↑(Finite.toFinset (s := Nᶜ) hN) : Set ι)ᶜ }),
  ‖f (↑b : ι) x‖ ≤ (u ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑(Finite.toFinset (s := Nᶜ) hN) : Set ι)ᶜ)) b
Tactic: apply Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) _ (hu.subtype _)
-- 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 β
ε : ℝ
ε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
⊢ ∀ (b : { x : ι // x ∈ (↑(Finite.toFinset (s := Nᶜ) hN) : Set ι)ᶜ }),
    ‖f (↑b : ι) x‖ ≤ (u ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑(Finite.toFinset (s := Nᶜ) hN) : Set ι)ᶜ)) b
have simp : ∀ (a : ι) (b : a ∉ Finite.toFinset (s := Nᶜ) hN), ‖f a x‖ ≤ u a
Tactic: simp only [comp_apply, Subtype.forall, Set.mem_compl_iff, Finset.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (hypothesis)
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 β
ε : ℝ
ε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) < ε
have A : Summable (α := ℝ) fun (n : ι) ↦ ‖f n x‖
Tactic: 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
-- 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 β
ε : ℝ
ε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) < ε
have rw : norm.{u_3} (E := F) (∑' (x_1 : { x : ι // x ∉ n }), f (↑x_1 : ι) x) < ε
Tactic: rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl n, add_sub_cancel_left]
-- 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 β
ε : ℝ
ε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‖
⊢ norm.{u_3} (E := F) (∑' (x_1 : { x : ι // x ∉ n }), f (↑x_1 : ι) x) < ε
have apply : norm.{u_3} (E := F) (∑' (x_1 : { x : ι // x ∉ n }), f (↑x_1 : ι) x) ≤ ∑' (a : { x : ι // x ∉ n }), u (↑a : ι)
Tactic: apply lt_of_le_of_lt _ (ht n (Finset.union_subset_right hn))
-- 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 β
ε : ℝ
ε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‖
⊢ norm.{u_3} (E := F) (∑' (x_1 : { x : ι // x ∉ n }), f (↑x_1 : ι) x) ≤ ∑' (a : { x : ι // x ∉ n }), u (↑a : ι)
have apply : LE.le (α := ℝ) (∑' (i : { x : ι // x ∉ n }), ‖f (↑i : ι) x‖) (∑' (a : { x : ι // x ∉ n }), u (↑a : ι))
Tactic: apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
-- 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 β
ε : ℝ
ε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‖
⊢ LE.le (α := ℝ) (∑' (i : { x : ι // x ∉ n }), ‖f (↑i : ι) x‖) (∑' (a : { x : ι // x ∉ n }), u (↑a : ι))
have apply : ∀ (i : { x : ι // x ∉ n }),
  ((fun (n : ι) ↦ ‖f n x‖) ∘ Subtype.val (p := fun (x : ι) ↦ x ∉ n)) i ≤ (u ∘ Subtype.val (p := fun (x : ι) ↦ x ∉ n)) i
Tactic: apply (A.subtype _).tsum_le_tsum _ (hu.subtype _)
-- 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 β
ε : ℝ
ε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‖
⊢ ∀ (i : { x : ι // x ∉ n }),
    ((fun (n : ι) ↦ ‖f n x‖) ∘ Subtype.val (p := fun (x : ι) ↦ x ∉ n)) i ≤
      (u ∘ Subtype.val (p := fun (x : ι) ↦ x ∉ n)) i
have simp : ∀ (a : ι) (b : a ∉ n), ‖f a x‖ ≤ u a
Tactic: simp only [comp_apply, Subtype.forall]
-- 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 β
ε : ℝ
ε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‖
⊢ ∀ (a : ι) (b : a ∉ n), ‖f a x‖ ≤ u a
have apply : ∀ (i : ι) (hi : i ∉ n), i ∈ N
Tactic: apply fun i hi => HN i ?_ x hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (hypothesis)
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 β
ε : ℝ
ε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‖
i : ι
hi : i ∉ n
⊢ i ∈ N
have this : i ∉ Finite.toFinset (s := Nᶜ) hN
Tactic: have : i ∉ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
-- 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
⊢ 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),
  ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, 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
-- 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) < ε
⊢ 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) (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) < ε
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
-- 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) < ε
⊢ 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 < ε)
  (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) < ε
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
-- 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) < ε
⊢ 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 : ι) < ε),
  ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, 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
-- 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) < ε
⊢ 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₄ : ∀ (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) < ε
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