no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬LimZero f
ε : α
ε0 : ε > 0
K : α
K0 : K > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → K ≤ abv (↑f j)
j : ℕ
ij : j ≥ i
⊢ abv (↑(inv f hf * f - 1) j) < ε
simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0