no goals
α : Type u_1
β : Type u_2
γ : Type ?u.47951
ι : Sort ?u.47954
f✝ : Filter α
f : α × α → β
x : Filter α
y : Filter β
⊢ Tendsto f (x ×ˢ x) y ↔ ∀ (W : Set β), W ∈ y → ∃ U, U ∈ x ∧ ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W
simp only [tendsto_def, mem_prod_same_iff, prod_sub_preimage_iff, exists_prop, iff_self_iff]