∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ}
  {g : β → γ},
  Filter.Tendsto f F Filter.atBot →
    Filter.Tendsto g G Filter.atBot → Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atBot