f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ↑abs (↑f j - ↑f i) < ε
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ↑abs ((fun n => ↑(starRingEnd ℂ) (↑f n)) j - (fun n => ↑(starRingEnd ℂ) (↑f n)) i) < ε
rw [← RingHom.map_sub, abs_conj]
no goals
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ↑abs (↑f j - ↑f i) < ε
exact hi j hj