case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (f i - ↑g i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
⊢ abv (f j - f i) < ε
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
⊢ abv (f j - f i) < ε
cases' hi _ le_rfl with h₁ h₂
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
⊢ abv (f j - f i) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (f i - ↑g i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
⊢ abv (f j - f i) < ε
rw [abv_sub abv] at h₁
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
this : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2
⊢ abv (f j - f i) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
⊢ abv (f j - f i) < ε
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi _ ij).1 h₁)
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
this✝ : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2
this : abv (f j - ↑g j + (↑g i - f i) + (↑g j - ↑g i)) < ε / 2 / 2 + ε / 2 / 2 + ε / 2
⊢ abv (f j - f i) < ε
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
this : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2
⊢ abv (f j - f i) < ε
have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add this (h₂ _ ij))
no goals
case intro
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
g : CauSeq β abv
h : ∀ (ε : α), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ (k : ℕ), k ≥ j → abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ (k : ℕ), k ≥ i → abv (↑g k - ↑g i) < ε / 2
this✝ : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2
this : abv (f j - ↑g j + (↑g i - f i) + (↑g j - ↑g i)) < ε / 2 / 2 + ε / 2 / 2 + ε / 2
⊢ abv (f j - f i) < ε
rwa [add_halves, add_halves, add_right_comm, sub_add_sub_cancel, sub_add_sub_cancel] at this