no goals
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
ij : j ≥ i
⊢ abs' ((fun n => (↑f n).im) j - (fun n => (↑f n).im) i) ≤ ↑abs (↑f j - ↑f i)
simpa using abs_im_le_abs (f j - f i)