have h1 : x ≠ 0 := by contrapose! hx; simp only [hx, mem_ball_self, hη]
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')