awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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
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) < ε
⊢ ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
refine ⟨hN.toFinset ∪ t, fun n hn x hx => ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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
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 ι)ᶜ))
⊢ Summable (α := ℝ) fun (n : ι) ↦ ‖f n x‖

Tactic:
apply Summable.add_compl (s := hN.toFinset) Summable.of_finite

Premises used: Summable.of_finite, Summable.add_compl
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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
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
⊢ 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.of_nonneg_of_le (fun _ ↦ norm_nonneg _) _ (hu.subtype _)

Premises used: Summable.subtype, Summable.of_nonneg_of_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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
simp : ∀ (a : ι) (b : a ∉ Finite.toFinset (s := Nᶜ) hN), ‖f a x‖ ≤ u a
⊢ ∀ (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:
simp only [comp_apply, Subtype.forall, Set.mem_compl_iff, Finset.mem_coe]

Premises used: Subtype.forall, Function.comp_apply, Finset.mem_coe, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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 : ι) (b : a ∉ Finite.toFinset (s := Nᶜ) hN), ‖f a x‖ ≤ u a

Tactic:
aesop
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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‖

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
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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‖
rw : norm.{u_3} (E := F) (∑' (x_1 : { x : ι // x ∉ n }), f (↑x_1 : ι) x) < ε
⊢ dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε

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

Premises used: Summable.sum_add_tsum_subtype_compl, dist_eq_norm, add_sub_cancel_left, Summable.of_norm
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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‖
apply : norm.{u_3} (E := F) (∑' (x_1 : { x : ι // x ∉ n }), f (↑x_1 : ι) x) ≤ ∑' (a : { x : ι // x ∉ n }), u (↑a : ι)
⊢ norm.{u_3} (E := F) (∑' (x_1 : { x : ι // x ∉ n }), f (↑x_1 : ι) x) < ε

Tactic:
apply lt_of_le_of_lt _ (ht n (Finset.union_subset_right hn))

Premises used: lt_of_le_of_lt, Finset.union_subset_right
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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‖
apply : LE.le (α := ℝ) (∑' (i : { x : ι // x ∉ n }), ‖f (↑i : ι) x‖) (∑' (a : { x : ι // x ∉ n }), u (↑a : ι))
⊢ norm.{u_3} (E := F) (∑' (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

Premises used: Summable.subtype, norm_tsum_le_tsum_norm, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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‖
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
⊢ LE.le (α := ℝ) (∑' (i : { x : ι // x ∉ n }), ‖f (↑i : ι) x‖) (∑' (a : { x : ι // x ∉ n }), u (↑a : ι))

Tactic:
apply (A.subtype _).tsum_le_tsum _ (hu.subtype _)

Premises used: Summable.subtype, Summable.tsum_le_tsum
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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‖
simp : ∀ (a : ι) (b : a ∉ n), ‖f a x‖ ≤ u a
⊢ ∀ (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:
simp only [comp_apply, Subtype.forall]

Premises used: Subtype.forall, Function.comp_apply
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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‖
apply : ∀ (i : ι) (hi : i ∉ n), i ∈ N
⊢ ∀ (a : ι) (b : a ∉ n), ‖f a x‖ ≤ u a

Tactic:
apply fun i hi => HN i ?_ x hx
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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 ∉ Finite.toFinset (s := Nᶜ) hN

Tactic:
have : i ∉ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
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
this : i ∉ Finite.toFinset (s := Nᶜ) hN
⊢ i ∈ N

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_4
F : Type u_5
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
f : ℕ → α → F
u : ℕ → ℝ
hu : Summable u
s : Set α
hfu : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn.{u_4, u_5, 0} (β := F) (fun (N : ℕ) (x : α) ↦ ∑ n ∈ Finset.range N, f n x)
    (fun (x : α) ↦ ∑' (n : ℕ), f n x) atTop s

Tactic:
fun v hv ↦ tendsto_finset_range.eventually <|
    tendstoUniformlyOn_tsum_of_cofinite_eventually hu (Nat.cofinite_eq_atTop ▸ hfu) v hv

Premises used: Set.Mem, TendstoUniformlyOn, Filter.tendsto_finset_range, tendstoUniformlyOn_tsum_of_cofinite_eventually, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
rw :
  TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (t : Finset α) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop univ
⊢ TendstoUniformly.{u_2, u_3, u_1} (β := F) (fun (t : Finset α) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop

Tactic:
rw [← tendstoUniformlyOn_univ]

Premises used: tendstoUniformlyOn_univ
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (t : Finset α) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop univ

Tactic:
tendstoUniformlyOn_tsum hu fun n x _ => hfu n x

Premises used: tendstoUniformlyOn_tsum
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (t : Finset α) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop univ

Tactic:
exact tendstoUniformlyOn_tsum hu fun n x _ => hfu n x

Premises used: tendstoUniformlyOn_tsum
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
f : ℕ → β → F
u : ℕ → ℝ
hu : Summable u
hfu : ∀ (n : ℕ) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformly.{u_2, u_3, 0} (β := F) (fun (N : ℕ) (x : β) ↦ ∑ n ∈ Finset.range N, f n x)
    (fun (x : β) ↦ ∑' (n : ℕ), f n x) atTop

Tactic:
fun v hv => tendsto_finset_range.eventually (tendstoUniformly_tsum hu hfu v hv)

Premises used: Set.Mem, Filter.tendsto_finset_range, TendstoUniformly, Filter.Tendsto.eventually, tendstoUniformly_tsum
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
rw :
  TendstoUniformlyOn.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : ι), f n x) atTop univ
⊢ TendstoUniformly.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : ι), f n x) atTop

Tactic:
rw [← tendstoUniformlyOn_univ]

Premises used: tendstoUniformlyOn_univ
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
apply : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), Membership.mem (γ := Set β) univ x → ‖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 univ

Tactic:
apply tendstoUniformlyOn_tsum_of_cofinite_eventually hu

Premises used: tendstoUniformlyOn_tsum_of_cofinite_eventually
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ ∀ᶠ (n : ι) in cofinite, ∀ (x : β), Membership.mem (γ := Set β) univ x → ‖f n x‖ ≤ u n

Tactic:
simpa using hfu
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑' (n : α), f n x) s

Tactic:
(tendstoUniformlyOn_tsum hu hfu).continuousOn (Frequently.of_forall ?_)

Premises used: Filter.Frequently.of_forall, tendstoUniformlyOn_tsum, TendstoUniformlyOn.continuousOn
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
refine : ∀ (x : Finset α), ContinuousOn.{u_2, u_3} (Y := F) (fun (x_1 : β) ↦ ∑ n ∈ x, f n x_1) s
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑' (n : α), f n x) s

Tactic:
refine (tendstoUniformlyOn_tsum hu hfu).continuousOn (Frequently.of_forall ?_)

Premises used: Filter.Frequently.of_forall, tendstoUniformlyOn_tsum, TendstoUniformlyOn.continuousOn
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
t : Finset α
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑ n ∈ t, f n x) s

Tactic:
continuousOn_finsetSum _ fun i _ => hf i

Premises used: continuousOn_finsetSum
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
t : Finset α
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑ n ∈ t, f n x) s

Tactic:
exact continuousOn_finsetSum _ fun i _ => hf i

Premises used: continuousOn_finsetSum
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
refine refine₁ : ∀ (t : Finset α), ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑ n ∈ t, f n x) s
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑' (n : α), f n x) s

Tactic:
classical
    refine (tendstoUniformlyOn_tsum hu hfu).continuousOn (Frequently.of_forall ?_)
    intro t
    exact continuousOn_finsetSum _ fun i _ => hf i

Premises used: Filter.Frequently.of_forall, tendstoUniformlyOn_tsum, continuousOn_finsetSum, TendstoUniformlyOn.continuousOn
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
hf : ∀ (i : α), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
simp_rw :
  ∀ (hf : ∀ (i : α), ContinuousOn (f i) univ), ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑' (n : α), f n x) univ
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : β) ↦ ∑' (n : α), f n x

Tactic:
simp_rw [← continuousOn_univ] at hf ⊢

Premises used: continuousOn_univ
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
hf : ∀ (i : α), ContinuousOn (f i) univ
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑' (n : α), f n x) univ

Tactic:
continuousOn_tsum hf hu fun n x _ => hfu n x

Premises used: continuousOn_tsum
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
hf : ∀ (i : α), ContinuousOn (f i) univ
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑' (n : α), f n x) univ

Tactic:
exact continuousOn_tsum hf hu fun n x _ => hfu n x

Premises used: continuousOn_tsum
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : Completion G
⊢ Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) x : Completion H)
    (Completion.map (⇑f : (a : G) → H) x : Completion H)

Tactic:
rfl

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion, rfl, ite
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
⊢ Eq (α := (a : Completion G) → Completion H) (⇑f.completion : (a : Completion G) → Completion H)
    (Completion.map (⇑f : (a : G) → H))

Tactic:
rfl

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion, rfl, ite
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
g : G
⊢ Eq.{u_2 + 1} (α := Completion H)
    ((f.completion : (a : Completion G) → Completion H) (↑g : Completion G) : Completion H)
    ((↑((f : (a : G) → H) g) : Completion H) : Completion H)

Tactic:
Completion.map_coe f.uniformContinuous _

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', UniformSpace.Completion.map_coe, NormedAddGroupHom.uniformContinuous, Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion, ite
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
g : G
⊢ Eq.{u_2 + 1} (α := Completion H) (Completion.map (⇑f : (a : G) → H) (↑g : Completion G) : Completion H)
    ((↑((f : (a : G) → H) g) : Completion H) : Completion H)

Tactic:
f.completion_coe g

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', NormedAddGroupHom.completion_coe, Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion, ite
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H :
  ∀ (x : Completion G),
    Eq (α := Completion G) ((completion (id G) : (a : Completion G) → Completion G) x : Completion G)
      ((id (Completion G) : (a : Completion G) → Completion G) x : Completion G)
⊢ Eq (α := NormedAddGroupHom (Completion G) (Completion G)) (completion (id G)) (id (Completion G))

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
x : Completion G
H : _root_.id x = (id (Completion G) : (a : Completion G) → Completion G) x
⊢ Eq (α := Completion G) ((completion (id G) : (a : Completion G) → Completion G) x : Completion G)
    ((id (Completion G) : (a : Completion G) → Completion G) x : Completion G)

Tactic:
rw [NormedAddGroupHom.completion_def, NormedAddGroupHom.coe_id, Completion.map_id]

Premises used: NormedAddGroupHom.completion_def, NormedAddGroupHom.coe_id, UniformSpace.Completion.map_id
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
x : Completion G
⊢ _root_.id x = (id (Completion G) : (a : Completion G) → Completion G) x

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
K : Type u_3
inst_2 : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
H₁ :
  ∀ (x : Completion G),
    Eq.{u_3 + 1} (α := Completion K)
      ((g.completion.comp f.completion : (a : Completion G) → Completion K) x : Completion K)
      (((g.comp f).completion : (a : Completion G) → Completion K) x : Completion K)
⊢ g.completion.comp f.completion = (g.comp f).completion

Tactic:
ext x