no goals
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type ?u.61803
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type ?u.61824
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × G)
hU : U ∈ nhds 1
V W : OpenSubgroup G
h : ↑V ×ˢ ↑W ⊆ U
⊢ ↑(V ⊓ W) ×ˢ ↑(V ⊓ W) ⊆ U
refine' Set.Subset.trans (Set.prod_mono _ _) ‹_› <;> simp