no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.51513
ι : Sort ?u.51516
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α × β → γ
x : Filter α
y : Filter β
z : Filter γ
⊢ Tendsto f (x ×ˢ y) z ↔
    ∀ (W : Set γ), W ∈ z → ∃ U, U ∈ x ∧ ∃ V, V ∈ y ∧ ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop, iff_self_iff]