∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ},
  (∀ s ∈ lb, Filter.Tendsto f (la ×ˢ Filter.principal sᶜ) lc) →
    Filter.Tendsto f (⊤ ×ˢ lb) lc → Filter.Tendsto f (la.coprod lb) lc