no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_2
inst✝¹ : UniformSpace α
ι' : Sort u_1
inst✝ : UniformSpace β
p : ι → Prop
s : ι → Set (α × α)
ha : HasBasis (𝓤 α) p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : HasBasis (𝓤 β) q t
f : α → β
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ (x : α × α), x ∈ s ia → (f x.fst, f x.snd) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i
simp only [Prod.forall]