case h.e'_5
𝓕 : Type ?u.138811
𝕜 : Type ?u.138814
α : Type ?u.138817
ι : Type ?u.138820
κ : Type ?u.138823
E : Type u_1
F : Type ?u.138829
G : Type ?u.138832
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ (fun ε => {p | ‖p.fst / p.snd‖ < ε}) = fun ε => {p | dist p.fst p.snd < ε}
𝓕 : Type ?u.138811
𝕜 : Type ?u.138814
α : Type ?u.138817
ι : Type ?u.138820
κ : Type ?u.138823
E : Type u_1
F : Type ?u.138829
G : Type ?u.138832
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ HasBasis (𝓤 E) (fun ε => 0 < ε) fun ε => {p | ‖p.fst / p.snd‖ < ε}
convert Metric.uniformity_basis_dist (α := E) using 1
no goals
case h.e'_5
𝓕 : Type ?u.138811
𝕜 : Type ?u.138814
α : Type ?u.138817
ι : Type ?u.138820
κ : Type ?u.138823
E : Type u_1
F : Type ?u.138829
G : Type ?u.138832
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ (fun ε => {p | ‖p.fst / p.snd‖ < ε}) = fun ε => {p | dist p.fst p.snd < ε}
simp [dist_eq_norm_div]