no goals
𝓕 : Type ?u.111126
𝕜 : Type ?u.111129
α : Type u_1
ι : Type ?u.111135
κ : Type ?u.111138
E : Type u_2
F : Type ?u.111144
G : Type ?u.111147
inst✝⁴ : SeminormedGroup E
inst✝³ : SeminormedGroup F
inst✝² : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
u : α → E
⊢ CauchySeq u ↔ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m / u n‖ < ε
simp [Metric.cauchySeq_iff, dist_eq_norm_div]