obtain ⟨ε, hε, hu⟩ := mem_uniformity_dist.mp hu
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu : u ∈ 𝓤 𝕜
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)