-- Mathlib/Algebra/Order/CauSeq/BigOperators.lean
lemma of_abv_le (n : ℕ) (hm : ∀ m, n ≤ m → abv (f m) ≤ a m) :
    IsCauSeq abs (fun n ↦ ∑ i ∈ range n, a i) → IsCauSeq abv fun n ↦ ∑ i ∈ range n, f i

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ n ⊔ i
hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n => ∑ i ∈ range n, a i) (n ⊔ i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (n ⊔ i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (n ⊔ i), a k|
⊢ abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (n ⊔ i)) < ε

Tactic:
have := add_lt_add hi₁ hi₂

Result:
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ n ⊔ i
hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n => ∑ i ∈ range n, a i) (n ⊔ i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (n ⊔ i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (n ⊔ i), a k|
this :
  |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| +
      |(fun n => ∑ i ∈ range n, a i) (n ⊔ i) - (fun n => ∑ i ∈ range n, a i) i| <
    ε / 2 + ε / 2
⊢ abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (n ⊔ i)) < ε

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ n ⊔ i
hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n => ∑ i ∈ range n, a i) (n ⊔ i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (n ⊔ i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (n ⊔ i), a k|
this :
  |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| +
      |(fun n => ∑ i ∈ range n, a i) (n ⊔ i) - (fun n => ∑ i ∈ range n, a i) i| <
    ε / 2 + ε / 2
⊢ abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (n ⊔ i)) < ε

Tactic:
rw [abs_sub_comm (∑ k ∈ range (max n i), a k), add_halves ε] at this

Result:
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ n ⊔ i
hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
hi₂ : |(fun n => ∑ i ∈ range n, a i) (n ⊔ i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
sub_le :
  |∑ k ∈ range j, a k - ∑ k ∈ range (n ⊔ i), a k| ≤
    |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (n ⊔ i), a k|
this :
  |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| +
      |(fun n => ∑ i ∈ range n, a i) i - ∑ k ∈ range (n ⊔ i), a k| <
    ε
⊢ abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (n ⊔ i)) < ε

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i j : ℕ
ji : j ≥ n ⊔ i
k : ℕ
hk : j = k + n ⊔ i
⊢ abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (n ⊔ i)) ≤
    ∑ k ∈ range j, a k - ∑ k ∈ range (n ⊔ i), a k

Tactic:
rw [hk]

Result:
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i j : ℕ
ji : j ≥ n ⊔ i
k : ℕ
hk : j = k + n ⊔ i
⊢ abv ((fun n => ∑ i ∈ range n, f i) (k + n ⊔ i) - (fun n => ∑ i ∈ range n, f i) (n ⊔ i)) ≤
    ∑ k ∈ range (k + n ⊔ i), a k - ∑ k ∈ range (n ⊔ i), a k

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) i) < ε

Tactic:
obtain ⟨i, hi⟩ := hg (ε / 2) (div_pos ε0 (by norm_num))

Result:
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2
⊢ ∃ i, ∀ j ≥ i, abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) i) < ε

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i j : ℕ
ji : j ≥ n ⊔ i
k : ℕ
hk : j = k + n ⊔ i
⊢ abv ((fun n => ∑ i ∈ range n, f i) (k + n ⊔ i) - (fun n => ∑ i ∈ range n, f i) (n ⊔ i)) ≤
    ∑ k ∈ range (k + n ⊔ i), a k - ∑ k ∈ range (n ⊔ i), a k

Tactic:
dsimp only

Result:
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i j : ℕ
ji : j ≥ n ⊔ i
k : ℕ
hk : j = k + n ⊔ i
⊢ abv (∑ i ∈ range (k + n ⊔ i), f i - ∑ i ∈ range (n ⊔ i), f i) ≤
    ∑ k ∈ range (k + n ⊔ i), a k - ∑ k ∈ range (n ⊔ i), a k

Proof state:
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k' : ℕ
hi :
  abv (∑ i ∈ range (k' + n ⊔ i), f i - ∑ i ∈ range (n ⊔ i), f i) ≤
    ∑ k ∈ range (k' + n ⊔ i), a k - ∑ k ∈ range (n ⊔ i), a k
⊢ abv (f (k' + n ⊔ i) + ∑ x ∈ range (k' + n ⊔ i), f x - ∑ x ∈ range (n ⊔ i), f x) ≤
    a (k' + n ⊔ i) + ∑ x ∈ range (k' + n ⊔ i), a x - ∑ x ∈ range (n ⊔ i), a x

Tactic:
simp only [add_assoc, sub_eq_add_neg]

Result:
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i k' : ℕ
hi :
  abv (∑ i ∈ range (k' + n ⊔ i), f i - ∑ i ∈ range (n ⊔ i), f i) ≤
    ∑ k ∈ range (k' + n ⊔ i), a k - ∑ k ∈ range (n ⊔ i), a k
⊢ abv (f (k' + n ⊔ i) + (∑ x ∈ range (k' + n ⊔ i), f x + -∑ x ∈ range (n ⊔ i), f x)) ≤
    a (k' + n ⊔ i) + (∑ x ∈ range (k' + n ⊔ i), a x + -∑ x ∈ range (n ⊔ i), a x)