-- Mathlib/Analysis/NormedSpace/FunctionSeries.lean
theorem tendstoUniformlyOn_tsum_of_cofinite_eventually {ι : Type*} {f : ι → β → F} {u : ι → ℝ}
    (hu : Summable u) {s : Set β} (hfu : ∀ᶠ n in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n) :
    TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' n, f n x) atTop s

Proof state:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
i : ι
hi : i ∈ fun x => x ∉ n
this : i ∉ Finite.toFinset hN
⊢ i ∈ N

Tactic:
aesop

Result:
no goals

Proof state:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ n }), f (↑x_1) x‖ ≤ ∑' (a : { x // x ∉ n }), u ↑a

Tactic:
apply (norm_tsum_le_tsum_norm (A.subtype _)).trans

Result:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ∑' (i : ↑fun x => x ∈ n → False), ‖f (↑i) x‖ ≤ ∑' (a : { x // x ∉ n }), u ↑a

Proof state:
case intro
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
rw [eventually_iff_exists_mem] at hfu

Result:
case intro
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∃ v ∈ cofinite, ∀ 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, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Proof state:
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : ι), f n x) atTop s

Tactic:
classical
refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
have := (tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos
simp only [not_forall, Classical.not_imp, not_le, 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, ← sum_add_tsum_subtype_compl A.of_norm 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 tsum_le_tsum _ (A.subtype _) (hu.subtype _)
simp only [comp_apply, Subtype.forall, imp_false]
apply fun i hi => HN i ?_ x hx
have : ¬ i ∈ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
aesop

Result:
no goals

Proof state:
case intro.intro.intro
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
refine ⟨hN.toFinset ∪ t, fun n hn x hx => ?_⟩

Result:
case intro.intro.intro
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
⊢ dist (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε

Proof state:
case intro.intro.intro
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
⊢ dist (∑' (n : ι), f n x) (∑ n ∈ 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

Result:
case intro.intro.intro
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ dist (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε

Proof state:
case intro.intro.intro
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ dist (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε

Tactic:
rw [dist_eq_norm, ← sum_add_tsum_subtype_compl A.of_norm n, add_sub_cancel_left]

Result:
case intro.intro.intro
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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 : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n => ‖f n x‖
⊢ ‖∑' (x_1 : { x // x ∉ n }), f (↑x_1) x‖ < ε