α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) i) < ε
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
⊢ (∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m) →
    (IsCauSeq abs' fun n => ∑ i in range n, g i) → IsCauSeq abv fun n => ∑ i in range n, f i
intro hm hg ε ε0
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) i) < ε
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) i) < ε
cases' hg (ε / 2) (div_pos ε0 (by norm_num)) with i hi
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
⊢ ∀ (j : ℕ), j ≥ max n i → abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) i) < ε
exists max n i
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
⊢ ∀ (j : ℕ), j ≥ max n i → abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
intro j ji
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
have hi₁ := hi j (le_trans (le_max_right n i) ji)
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
have hi₂ := hi (max n i) (le_max_right n i)
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
have sub_le :=
  abs_sub_le (∑ k in range j, g k) (∑ k in range i, g k) (∑ k in range (max n i), g k)
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
this :
  abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) +
      abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) <
    ε / 2 + ε / 2
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
have := add_lt_add hi₁ hi₂
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
this :
  abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) +
      abs' ((fun n => ∑ i in range n, g i) i - ∑ k in range (max n i), g k) <
    ε
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
this :
  abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) +
      abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) <
    ε / 2 + ε / 2
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
rw [abs_sub_comm (∑ k in range (max n i), g k), add_halves ε] at this
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
this :
  abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) +
      abs' ((fun n => ∑ i in range n, g i) i - ∑ k in range (max n i), g k) <
    ε
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range j, g k - ∑ k in range (max n i), g k
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
this :
  abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) +
      abs' ((fun n => ∑ i in range n, g i) i - ∑ k in range (max n i), g k) <
    ε
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) < ε
refine' lt_of_le_of_lt (le_trans (le_trans _ (le_abs_self _)) sub_le) this
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
this :
  abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) +
      abs' ((fun n => ∑ i in range n, g i) i - ∑ k in range (max n i), g k) <
    ε
k : ℕ
hk : j - max n i = k
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range j, g k - ∑ k in range (max n i), g k
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
this :
  abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) +
      abs' ((fun n => ∑ i in range n, g i) i - ∑ k in range (max n i), g k) <
    ε
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range j, g k - ∑ k in range (max n i), g k
generalize hk : j - max n i = k
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j - max n i = k
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range j, g k - ∑ k in range (max n i), g k
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
j : ℕ
ji : j ≥ max n i
hi₁ : abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) < ε / 2
hi₂ : abs' ((fun n => ∑ i in range n, g i) (max n i) - (fun n => ∑ i in range n, g i) i) < ε / 2
sub_le :
  abs' (∑ k in range j, g k - ∑ k in range (max n i), g k) ≤
    abs' (∑ k in range j, g k - ∑ k in range i, g k) + abs' (∑ k in range i, g k - ∑ k in range (max n i), g k)
this :
  abs' ((fun n => ∑ i in range n, g i) j - (fun n => ∑ i in range n, g i) i) +
      abs' ((fun n => ∑ i in range n, g i) i - ∑ k in range (max n i), g k) <
    ε
k : ℕ
hk : j - max n i = k
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range j, g k - ∑ k in range (max n i), g k
clear this hi₂ hi₁ hi ε0 ε hg sub_le
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range j, g k - ∑ k in range (max n i), g k
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j - max n i = k
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range j, g k - ∑ k in range (max n i), g k
rw [tsub_eq_iff_eq_add_of_le ji] at hk
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv ((fun n => ∑ i in range n, f i) (k + max n i) - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range (k + max n i), g k - ∑ k in range (max n i), g k
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv ((fun n => ∑ i in range n, f i) j - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range j, g k - ∑ k in range (max n i), g k
rw [hk]
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv (∑ i in range (k + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k + max n i), g k - ∑ k in range (max n i), g k
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv ((fun n => ∑ i in range n, f i) (k + max n i) - (fun n => ∑ i in range n, f i) (max n i)) ≤
    ∑ k in range (k + max n i), g k - ∑ k in range (max n i), g k
dsimp only
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k : ℕ
⊢ abv (∑ i in range (k + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k + max n i), g k - ∑ k in range (max n i), g k
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i j : ℕ
ji : j ≥ max n i
k : ℕ
hk : j = k + max n i
⊢ abv (∑ i in range (k + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k + max n i), g k - ∑ k in range (max n i), g k
clear hk ji j
case intro.zero
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i : ℕ
⊢ abv (∑ i in range (Nat.zero + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (Nat.zero + max n i), g k - ∑ k in range (max n i), g k

case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k - ∑ k in range (max n i), g k
⊢ abv (∑ i in range (Nat.succ k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (Nat.succ k' + max n i), g k - ∑ k in range (max n i), g k
case intro
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k : ℕ
⊢ abv (∑ i in range (k + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k + max n i), g k - ∑ k in range (max n i), g k
induction' k with k' hi
no goals
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
hg : IsCauSeq abs' fun n => ∑ i in range n, g i
ε : α
ε0 : ε > 0
⊢ 0 < 2
norm_num
no goals
case intro.zero
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i : ℕ
⊢ abv (∑ i in range (Nat.zero + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (Nat.zero + max n i), g k - ∑ k in range (max n i), g k
simp [abv_zero abv]
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k - ∑ k in range (max n i), g k
⊢ abv (f (k' + max n i) + ∑ x in range (k' + max n i), f x - ∑ x in range (max n i), f x) ≤
    g (k' + max n i) + ∑ x in range (k' + max n i), g x - ∑ x in range (max n i), g x
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k - ∑ k in range (max n i), g k
⊢ abv (∑ i in range (Nat.succ k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (Nat.succ k' + max n i), g k - ∑ k in range (max n i), g k
simp only [Nat.succ_add, Nat.succ_eq_add_one, Finset.sum_range_succ_comm]
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k - ∑ k in range (max n i), g k
⊢ abv (f (k' + max n i) + (∑ x in range (k' + max n i), f x + -∑ x in range (max n i), f x)) ≤
    g (k' + max n i) + (∑ x in range (k' + max n i), g x + -∑ x in range (max n i), g x)
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k - ∑ k in range (max n i), g k
⊢ abv (f (k' + max n i) + ∑ x in range (k' + max n i), f x - ∑ x in range (max n i), f x) ≤
    g (k' + max n i) + ∑ x in range (k' + max n i), g x - ∑ x in range (max n i), g x
simp only [add_assoc, sub_eq_add_neg]
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k - ∑ k in range (max n i), g k
⊢ abv (f (k' + max n i)) + abv (∑ x in range (k' + max n i), f x + -∑ x in range (max n i), f x) ≤
    g (k' + max n i) + (∑ x in range (k' + max n i), g x + -∑ x in range (max n i), g x)
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k - ∑ k in range (max n i), g k
⊢ abv (f (k' + max n i) + (∑ x in range (k' + max n i), f x + -∑ x in range (max n i), f x)) ≤
    g (k' + max n i) + (∑ x in range (k' + max n i), g x + -∑ x in range (max n i), g x)
refine le_trans (abv_add _ _ _) ?_
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i + -∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k + -∑ k in range (max n i), g k
⊢ abv (f (k' + max n i)) + abv (∑ x in range (k' + max n i), f x + -∑ x in range (max n i), f x) ≤
    g (k' + max n i) + (∑ x in range (k' + max n i), g x + -∑ x in range (max n i), g x)
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i - ∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k - ∑ k in range (max n i), g k
⊢ abv (f (k' + max n i)) + abv (∑ x in range (k' + max n i), f x + -∑ x in range (max n i), f x) ≤
    g (k' + max n i) + (∑ x in range (k' + max n i), g x + -∑ x in range (max n i), g x)
simp only [sub_eq_add_neg] at hi
no goals
case intro.succ
α : Type u_1
β : Type u_2
inst✝² : Ring β
inst✝¹ : LinearOrderedField α
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ g m
i k' : ℕ
hi :
  abv (∑ i in range (k' + max n i), f i + -∑ i in range (max n i), f i) ≤
    ∑ k in range (k' + max n i), g k + -∑ k in range (max n i), g k
⊢ abv (f (k' + max n i)) + abv (∑ x in range (k' + max n i), f x + -∑ x in range (max n i), f x) ≤
    g (k' + max n i) + (∑ x in range (k' + max n i), g x + -∑ x in range (max n i), g x)
refine add_le_add (hm _ (le_add_of_nonneg_of_le (Nat.zero_le _) (le_max_left _ _))) hi