α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑(f - g) j) < ε / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
⊢ abv (↑f k - ↑g j) < ε
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑(f - g) j) < ε / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
jk : k ≥ j
⊢ abv (↑f k - ↑g j) < ε
let ⟨h₁, h₂⟩ := H _ ij
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑(f - g) j) < ε / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
this : abv (↑f j - ↑g j + (↑f k - ↑f j)) < ε / 2 + ε / 2
⊢ abv (↑f k - ↑g j) < ε
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑(f - g) j) < ε / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
⊢ abv (↑f k - ↑g j) < ε
have := lt_of_le_of_lt (abv_add abv (f j - g j) _) (add_lt_add h₁ (h₂ _ jk))
no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
h : f ≈ g
ε : α
ε0 : 0 < ε
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑(f - g) j) < ε / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
jk : k ≥ j
h₁ : abv (↑(f - g) j) < ε / 2
h₂ : ∀ (k : ℕ), k ≥ j → abv (↑f k - ↑f j) < ε / 2
this : abv (↑f j - ↑g j + (↑f k - ↑f j)) < ε / 2 + ε / 2
⊢ abv (↑f k - ↑g j) < ε
rwa [sub_add_sub_cancel', add_halves] at this