-- Mathlib/Analysis/Normed/Group/InfiniteSum.lean
theorem cauchySeq_finset_of_norm_bounded_eventually {f : ι → E} {g : ι → ℝ} (hg : Summable g)
    (h : ∀ᶠ i in cofinite, ‖f i‖ ≤ g i) : CauchySeq fun s => ∑ i ∈ s, f i

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
⊢ ∀ i ∈ t, ‖f i‖ ≤ g i

Tactic:
intro i hi

Result:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
i : ι
hi : i ∈ t
⊢ ‖f i‖ ≤ g i

Proof state:
case intro
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
refine ⟨s ∪ h.toFinset, fun t ht => ?_⟩

Result:
case intro
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
⊢ ‖∑ i ∈ t, f i‖ < ε

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
i : ι
hi : i ∈ t
⊢ ‖f i‖ ≤ g i

Tactic:
simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
  Classical.not_not] at ht

Result:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
i : ι
hi : i ∈ t
ht : ∀ ⦃a : ι⦄, a ∈ t → a ∉ s ∧ a ∈ {x | ‖f x‖ ≤ g x}
⊢ ‖f i‖ ≤ g i

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
⊢ CauchySeq fun s => ∑ i ∈ s, f i

Tactic:
refine cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => ?_

Result:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
rcases summable_iff_vanishing_norm.1 hg ε hε with ⟨s, hs⟩

Result:
case intro
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Proof state:
case intro
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
this : ∀ i ∈ t, ‖f i‖ ≤ g i
⊢ ‖∑ i ∈ t, f i‖ < ε

Tactic:
calc
  ‖∑ i ∈ t, f i‖ ≤ ∑ i ∈ t, g i := norm_sum_le_of_le _ this
  _ ≤ ‖∑ i ∈ t, g i‖ := le_abs_self _
  _ < ε := hs _ (ht.mono_right le_sup_left)

Result:
no goals

Proof state:
case intro
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
classical
refine ⟨s ∪ h.toFinset, fun t ht => ?_⟩
have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
  intro i hi
  simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
    Classical.not_not] at ht
  exact (ht hi).2
calc
  ‖∑ i ∈ t, f i‖ ≤ ∑ i ∈ t, g i := norm_sum_le_of_le _ this
  _ ≤ ‖∑ i ∈ t, g i‖ := le_abs_self _
  _ < ε := hs _ (ht.mono_right le_sup_left)

Result:
no goals

Proof state:
case intro
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
⊢ ‖∑ i ∈ t, f i‖ < ε

Tactic:
have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
  intro i hi
  simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
    Classical.not_not] at ht
  exact (ht hi).2

Result:
case intro
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
this : ∀ i ∈ t, ‖f i‖ ≤ g i
⊢ ‖∑ i ∈ t, f i‖ < ε

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
i : ι
hi : i ∈ t
ht : ∀ ⦃a : ι⦄, a ∈ t → a ∉ s ∧ a ∈ {x | ‖f x‖ ≤ g x}
⊢ ‖f i‖ ≤ g i

Tactic:
exact (ht hi).2

Result:
no goals