no goals
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
X : Set (C(α, β) × C(α, β))
⊢ X ∈ compactConvergenceUniformity ↔ ∃ K V _hK _hV, {fg | ∀ (x : α), x ∈ K → (↑fg.fst x, ↑fg.snd x) ∈ V} ⊆ X
simp only [hasBasis_compactConvergenceUniformity_aux.mem_iff, exists_prop, Prod.exists,
  and_assoc]